toArray/keysArray lemmas

Author: datokrat

src/Init/Data/Array/Basic.lean

@@ -147,6 +147,9 @@ end List
 
 namespace Array
 
+@[simp, grind =] theorem getElem!_toList [Inhabited α] {xs : Array α} {i : Nat} : xs.toList[i]! = xs[i]! := by
+  rw [List.getElem!_toArray]
+
 theorem size_eq_length_toList {xs : Array α} : xs.size = xs.toList.length := rfl
 
 /-! ### Externs -/

src/Init/Data/List/Lemmas.lean

@@ -937,6 +937,12 @@ theorem getElem_zero_eq_head {l : List α} (h : 0 < l.length) :
   | nil => simp at h
   | cons _ _ => simp
 
+theorem head!_eq_getElem! [Inhabited α] {l : List α} : head! l = l[0]! := by
+  cases l <;> rfl
+
+theorem headD_eq_getD {l : List α} {fallback} : headD l fallback = l.getD 0 fallback := by
+  cases l <;> rfl
+
 theorem head_eq_iff_head?_eq_some {xs : List α} (h) : xs.head h = a ↔ xs.head? = some a := by
   cases xs with
   | nil => simp at h

src/Std/Data/DTreeMap/Internal/Lemmas.lean

@@ -661,7 +661,7 @@ theorem minKey?_eq_minEntry?_map_fst {l : Impl α β} : l.minKey? = l.minEntry?.
 theorem minKey_eq_minEntry_fst {l : Impl α β} {he} : l.minKey he = (l.minEntry he).fst := by
   induction l, he using minKey.induct_unfolding <;> simp only [minEntry] <;> trivial
 
-theorem minKey!_eq_get!_minKey? [Inhabited α] {l : Impl α β} :
+theorem minKey!_eq_getElem!_minKey? [Inhabited α] {l : Impl α β} :
     l.minKey! = l.minKey?.get! := by
   induction l using minKey!.induct_unfolding <;> simp only [minKey?] <;> trivial
 

src/Std/Data/DTreeMap/Internal/Model.lean

@@ -2296,7 +2296,7 @@ theorem minKey_eq_minKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l :
 theorem minKey!_eq_minKey! [Ord α] [TransOrd α] [Inhabited α] [BEq α] [LawfulBEqOrd α]
     {l : Impl α β} (hlo : l.Ordered) :
     l.minKey! = List.minKey! l.toListModel := by
-  simp [Impl.minKey!_eq_get!_minKey?, List.minKey!_eq_get!_minKey?, minKey?_eq_minKey? hlo]
+  simp [Impl.minKey!_eq_getElem!_minKey?, List.minKey!_eq_get!_minKey?, minKey?_eq_minKey? hlo]
 
 theorem minKeyD_eq_minKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : Impl α β}
     (hlo : l.Ordered) {fallback} :