-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/OfFn.lean
theorem getElem_ofFn (f : Fin n → α) (i : Nat) (h : i < (ofFn f).length) :
    (ofFn f)[i] = f ⟨i, by simp_all⟩

Proof state:
α : Type u_1
n : Nat
ih : ∀ (f : Fin n → α) (i : Nat) (h : i < (ofFn f).length), (Fin.foldr n (fun x1 x2 => f x1 :: x2) [])[i] = f ⟨i, ⋯⟩
f : Fin (n + 1) → α
i✝ i : Nat
h : i + 1 < (ofFn f).length
⊢ (f 0 :: Fin.foldr n (fun i x2 => f i.succ :: x2) [])[i + 1] = f ⟨i + 1, ⋯⟩

Tactic:
apply ih

Result:
case h
α : Type u_1
n : Nat
ih : ∀ (f : Fin n → α) (i : Nat) (h : i < (ofFn f).length), (Fin.foldr n (fun x1 x2 => f x1 :: x2) [])[i] = f ⟨i, ⋯⟩
f : Fin (n + 1) → α
i✝ i : Nat
h : i + 1 < (ofFn f).length
⊢ i < (ofFn fun x1 => f x1.succ).length

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < (ofFn f).length
⊢ (ofFn f)[i] = f ⟨i, ⋯⟩

Tactic:
simp only [ofFn]

Result:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < (ofFn f).length
⊢ (Fin.foldr n (fun x1 x2 => f x1 :: x2) [])[i] = f ⟨i, ⋯⟩

Proof state:
case h
α : Type u_1
n : Nat
ih : ∀ (f : Fin n → α) (i : Nat) (h : i < (ofFn f).length), (Fin.foldr n (fun x1 x2 => f x1 :: x2) [])[i] = f ⟨i, ⋯⟩
f : Fin (n + 1) → α
i✝ i : Nat
h : i + 1 < (ofFn f).length
⊢ i < (ofFn fun x1 => f x1.succ).length

Tactic:
simp_all

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < (ofFn f).length
⊢ (Fin.foldr n (fun x1 x2 => f x1 :: x2) [])[i] = f ⟨i, ⋯⟩

Tactic:
induction n generalizing i with
| zero => simp at h
| succ n ih =>
  match i with
  | 0 => simp [Fin.foldr_succ]
  | i+1 =>
    simp only [Fin.foldr_succ]
    apply ih
    simp_all

Result:
no goals

Proof state:
n : Nat
α : Type ?u.412
f : Fin n → α
i : Nat
h : i < (ofFn f).length
⊢ i < n

Tactic:
simp_all

Result:
no goals

Proof state:
case succ
α : Type u_1
n : Nat
ih : ∀ (f : Fin n → α) (i : Nat) (h : i < (ofFn f).length), (Fin.foldr n (fun x1 x2 => f x1 :: x2) [])[i] = f ⟨i, ⋯⟩
f : Fin (n + 1) → α
i : Nat
h : i < (ofFn f).length
⊢ (Fin.foldr (n + 1) (fun x1 x2 => f x1 :: x2) [])[i] = f ⟨i, ⋯⟩

Tactic:
match i with
| 0 => simp [Fin.foldr_succ]
| i+1 =>
  simp only [Fin.foldr_succ]
  apply ih
  simp_all

Result:
no goals

Proof state:
α : Type u_1
n : Nat
ih : ∀ (f : Fin n → α) (i : Nat) (h : i < (ofFn f).length), (Fin.foldr n (fun x1 x2 => f x1 :: x2) [])[i] = f ⟨i, ⋯⟩
f : Fin (n + 1) → α
i : Nat
h : 0 < (ofFn f).length
⊢ (Fin.foldr (n + 1) (fun x1 x2 => f x1 :: x2) [])[0] = f ⟨0, ⋯⟩

Tactic:
simp [Fin.foldr_succ]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
ih : ∀ (f : Fin n → α) (i : Nat) (h : i < (ofFn f).length), (Fin.foldr n (fun x1 x2 => f x1 :: x2) [])[i] = f ⟨i, ⋯⟩
f : Fin (n + 1) → α
i✝ i : Nat
h : i + 1 < (ofFn f).length
⊢ (Fin.foldr (n + 1) (fun x1 x2 => f x1 :: x2) [])[i + 1] = f ⟨i + 1, ⋯⟩

Tactic:
simp only [Fin.foldr_succ]

Result:
α : Type u_1
n : Nat
ih : ∀ (f : Fin n → α) (i : Nat) (h : i < (ofFn f).length), (Fin.foldr n (fun x1 x2 => f x1 :: x2) [])[i] = f ⟨i, ⋯⟩
f : Fin (n + 1) → α
i✝ i : Nat
h : i + 1 < (ofFn f).length
⊢ (f 0 :: Fin.foldr n (fun i x2 => f i.succ :: x2) [])[i + 1] = f ⟨i + 1, ⋯⟩

Proof state:
case zero
α : Type u_1
f : Fin 0 → α
i : Nat
h : i < (ofFn f).length
⊢ (Fin.foldr 0 (fun x1 x2 => f x1 :: x2) [])[i] = f ⟨i, ⋯⟩

Tactic:
simp at h

Result:
no goals