feat: injectivity lemmas for getElem(?) on List and Option

src/Init/Data/List/Pairwise.lean

@@ -304,26 +304,43 @@ grind_pattern Nodup.sublist => l₁ <+ l₂, Nodup l₂
 theorem Sublist.nodup : l₁ <+ l₂ → Nodup l₂ → Nodup l₁ :=
   Nodup.sublist
 
-theorem getElem?_inj {xs : List α}
-    (h₀ : i < xs.length) (h₁ : Nodup xs) (h₂ : xs[i]? = xs[j]?) : i = j := by
-  induction xs generalizing i j with
-  | nil => cases h₀
-  | cons x xs ih =>
-    match i, j with
-    | 0, 0 => rfl
-    | i+1, j+1 =>
-      cases h₁ with
-      | cons ha h₁ =>
-        simp only [getElem?_cons_succ] at h₂
-        exact congrArg (· + 1) (ih (Nat.lt_of_succ_lt_succ h₀) h₁ h₂)
-    | i+1, 0 => ?_
-    | 0, j+1 => ?_
-    all_goals
-      simp only [getElem?_cons_zero, getElem?_cons_succ] at h₂
-      cases h₁; rename_i h' h
-      have := h x ?_ rfl; cases this
-      rw [mem_iff_getElem?]
-    exact ⟨_, h₂⟩; exact ⟨_ , h₂.symm⟩
+theorem getElem?_inj {l : List α} (h₀ : i < l.length) (h₁ : List.Nodup l) :
+    l[i]? = l[j]? ↔ i = j :=
+  ⟨by
+    intro h₂
+    induction l generalizing i j with
+    | nil => cases h₀
+    | cons x xs ih =>
+      match i, j with
+      | 0, 0 => rfl
+      | i+1, j+1 =>
+        cases h₁ with
+        | cons ha h₁ =>
+          simp only [getElem?_cons_succ] at h₂
+          exact congrArg (· + 1) (ih (Nat.lt_of_succ_lt_succ h₀) h₁ h₂)
+      | i+1, 0 => ?_
+      | 0, j+1 => ?_
+      all_goals
+        simp only [getElem?_cons_zero, getElem?_cons_succ] at h₂
+        cases h₁; rename_i h' h
+        have := h x ?_ rfl; cases this
+        rw [mem_iff_getElem?]
+      exact ⟨_, h₂⟩; exact ⟨_ , h₂.symm⟩
+      , by simp +contextual⟩
+
+theorem getElem_inj {xs : List α}
+    {h₀ : i < xs.length} {h₁ : j < xs.length} (h : Nodup xs) : xs[i] = xs[j] ↔ i = j := by
+  simpa only [List.getElem_eq_getElem?_get, Option.get_inj] using getElem?_inj h₀ h
+
+theorem getD_inj {xs : List α}
+    (h₀ : i < xs.length) (h₁ : j < xs.length) (h₂ : Nodup xs) :
+    xs.getD i fallback = xs.getD j fallback ↔ i = j := by
+  simp only [List.getD_eq_getElem?_getD]
+  rw [Option.getD_inj, getElem?_inj] <;> simpa
+
+theorem getElem!_inj [Inhabited α] {xs : List α}
+    (h₀ : i < xs.length) (h₁ : j < xs.length) (h₂ : Nodup xs) : xs[i]! = xs[j]! ↔ i = j := by
+  simpa only [getElem!_eq_getElem?_getD, ← getD_eq_getElem?_getD] using getD_inj h₀ h₁ h₂
 
 @[simp, grind =] theorem nodup_replicate {n : Nat} {a : α} :
     (replicate n a).Nodup ↔ n ≤ 1 := by simp [Nodup]

src/Init/Data/Option/Lemmas.lean

@@ -82,6 +82,15 @@ theorem get_inj {o1 o2 : Option α} {h1} {h2} :
   match o1, o2, h1, h2 with
   | some a, some b, _, _ => simp only [Option.get_some, Option.some.injEq]
 
+theorem getD_inj {o₁ o₂ : Option α} (h₁ : o₁.isSome) (h₂ : o₂.isSome) {fallback} :
+    o₁.getD fallback = o₂.getD fallback ↔ o₁ = o₂ := by
+  match o₁, o₂, h₁, h₂ with
+  | some a, some b, _, _ => simp only [Option.getD_some, Option.some.injEq]
+
+theorem get!_inj [Inhabited α] {o₁ o₂ : Option α} (h₁ : o₁.isSome) (h₂ : o₂.isSome) :
+    o₁.get! = o₂.get! ↔ o₁ = o₂ := by
+  simpa [get!_eq_getD] using getD_inj h₁ h₂
+
 theorem mem_unique {o : Option α} {a b : α} (ha : a ∈ o) (hb : b ∈ o) : a = b :=
   some.inj <| ha ▸ hb