feat(Data/List/GetD): golf and add lemmas for get and getElem?

Author: SnirBroshi

Mathlib/Data/List/GetD.lean

@@ -30,46 +30,48 @@ variable (d : α)
 theorem getD_eq_getElem {n : ℕ} (hn : n < l.length) : l.getD n d = l[n] := by
   grind
 
-theorem getD_map {n : ℕ} (f : α → β) : (map f l).getD n (f d) = f (l.getD n d) := by simp
+theorem getD_eq_getElem? (l : List α) (d : α) (i : Fin l.length) :
+    l.getD i d = l[i]?.get (by simp) := by
+  simp
+
+theorem getD_eq_get (l : List α) (d : α) (i : Fin l.length) : l.getD i d = l.get i := by
+  simp
+
+theorem getD_map {n : ℕ} (f : α → β) : (map f l).getD n (f d) = f (l.getD n d) := by
+  simp
 
 theorem getD_eq_default {n : ℕ} (hn : l.length ≤ n) : l.getD n d = d := by
   grind
 
 theorem getD_reverse {l : List α} (i) (h : i < length l) :
     getD l.reverse i = getD l (l.length - 1 - i) := by
-  funext a
-  rwa [List.getD_eq_getElem?_getD, List.getElem?_reverse, ← List.getD_eq_getElem?_getD]
+  grind
 
 /-- An empty list can always be decidably checked for the presence of an element.
 Not an instance because it would clash with `DecidableEq α`. -/
-def decidableGetDNilNe (a : α) : DecidablePred fun i : ℕ => getD ([] : List α) i a ≠ a :=
+def decidableGetDNilNe (a : α) : DecidablePred fun i : ℕ => getD nil i a ≠ a :=
   fun _ => isFalse fun H => H getD_nil
 
 @[simp]
-theorem getElem?_getD_singleton_default_eq (n : ℕ) : [d][n]?.getD d = d := by cases n <;> simp
+theorem getElem?_getD_singleton_default_eq (n : ℕ) : [d][n]?.getD d = d := by
+  grind
 
 @[simp]
 theorem getElem?_getD_replicate_default_eq (r n : ℕ) : (replicate r d)[n]?.getD d = d := by
   grind
 
-theorem getD_replicate {y i n} (h : i < n) :
-    getD (replicate n x) i y = x := by
-  rw [getD_eq_getElem, getElem_replicate]
-  rwa [length_replicate]
+theorem getD_replicate {y i n} (h : i < n) : getD (replicate n x) i y = x := by
+  grind
 
 theorem getD_append (l l' : List α) (d : α) (n : ℕ) (h : n < l.length) :
     (l ++ l').getD n d = l.getD n d := by
-  rw [getD_eq_getElem _ _ (Nat.lt_of_lt_of_le h (length_append ▸ Nat.le_add_right _ _)),
-    getElem_append_left h, getD_eq_getElem]
+  grind
 
 theorem getD_append_right (l l' : List α) (d : α) (n : ℕ) (h : l.length ≤ n) :
     (l ++ l').getD n d = l'.getD (n - l.length) d := by
   grind
 
-theorem getD_eq_getD_getElem? (n : ℕ) : l.getD n d = l[n]?.getD d := by
-  cases Nat.lt_or_ge n l.length with
-  | inl h => rw [getD_eq_getElem _ _ h, getElem?_eq_getElem h, Option.getD_some]
-  | inr h => rw [getD_eq_default _ _ h, getElem?_eq_none_iff.mpr h, Option.getD_none]
+theorem getD_eq_getD_getElem? (n : ℕ) : l.getD n d = l[n]?.getD d := rfl
 
 end getD
 
@@ -106,7 +108,7 @@ theorem getI_append_right (l l' : List α) (n : ℕ) (h : l.length ≤ n) :
   getD_append_right _ _ _ _ h
 
 theorem getI_eq_iget_getElem? (n : ℕ) : l.getI n = l[n]?.iget := by
-  rw [← getD_default_eq_getI, getD_eq_getD_getElem?, Option.getD_default_eq_iget]
+  simp [← getD_default_eq_getI, Option.getD_default_eq_iget]
 
 theorem getI_zero_eq_headI : l.getI 0 = l.headI := by cases l <;> rfl