Test leanprover-community/batteries#784

Mathlib/Data/List/OfFn.lean

@@ -36,23 +36,33 @@ namespace List
 
 #noalign list.length_of_fn_aux
 
+@[simp]
+theorem length_ofFn_go {n} (f : Fin n → α) (i : Nat) (h : i ≤ n) : length (ofFn.go f i h) = i := by
+  induction i <;> simp_all [ofFn.go]
+
 /-- The length of a list converted from a function is the size of the domain. -/
 @[simp]
 theorem length_ofFn {n} (f : Fin n → α) : length (ofFn f) = n := by
-  simp [ofFn]
+  simp [ofFn, length_ofFn_go]
 #align list.length_of_fn List.length_ofFn
 
 #noalign list.nth_of_fn_aux
 
+theorem get_ofFn_go {n} (f : Fin n → α) (i : Nat) (h : i ≤ n) (j) (hj) :
+    get (ofFn.go f i h) ⟨j, hj⟩ = f ⟨n + j - i, by simp at hj; omega⟩ := by
+  induction i, h using ofFn.go.induct f generalizing j
+  case case1 => simp at hj
+  case case2 ih =>
+  · cases j
+    · simp [ofFn.go]
+    · simp [ofFn.go, ih]
+      congr 2
+      omega
+
 -- Porting note (#10756): new theorem
 @[simp]
 theorem get_ofFn {n} (f : Fin n → α) (i) : get (ofFn f) i = f (Fin.cast (by simp) i) := by
-  have := Array.getElem_ofFn f i (by simpa using i.2)
-  cases' i with i hi
-  simp only [getElem, Array.get] at this
-  simp only [Fin.cast_mk]
-  rw [← this]
-  congr
+  cases i; simp [ofFn, get_ofFn_go]
 
 /-- The `n`th element of a list -/
 @[simp]
@@ -114,7 +124,7 @@ theorem ofFn_zero (f : Fin 0 → α) : ofFn f = [] :=
 theorem ofFn_succ {n} (f : Fin (succ n) → α) : ofFn f = f 0 :: ofFn fun i => f i.succ :=
   ext_get (by simp) (fun i hi₁ hi₂ => by
     cases i
-    · simp
+    · simp; rfl
     · simp)
 #align list.of_fn_succ List.ofFn_succ
 

lakefile.lean

@@ -21,7 +21,7 @@ package mathlib where
 meta if get_config? doc = some "on" then -- do not download and build doc-gen4 by default
 require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
 
-require batteries from git "https://github.com/leanprover-community/batteries" @ "main"
+require batteries from git "https://github.com/nomeata/std4" @ "joachim/List.ofFn-structural"
 require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
 require aesop from git "https://github.com/leanprover-community/aesop" @ "master"
 require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.36"