-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_ofFn_go (f : Fin n → α) (i) {acc k}
    (hki : k < n) (hin : i ≤ n) (hi : i = acc.size)
    (hacc : ∀ j, ∀ hj : j < acc.size, acc[j] = f ⟨j, Nat.lt_of_lt_of_le hj (hi ▸ hin)⟩) :
    haveI : acc.size + (n - acc.size) = n := Nat.add_sub_cancel' (hi ▸ hin)
    (ofFn.go f i acc)[k]'(by simp [*]) = f ⟨k, hki⟩

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
acc : Array α
k : Nat
hki : k < n
hin✝ : i ≤ n
hi : i = acc.size
hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩
hin : i < n
⊢ (if h : i < n then ofFn.go f (i + 1) (acc.push (f ⟨i, h⟩)) else acc)[k] = f ⟨k, hki⟩

Tactic:
have : 1 + (n - (i + 1)) = n - i :=
  Nat.sub_sub .. ▸ Nat.add_sub_cancel' (Nat.le_sub_of_add_le (Nat.add_comm .. ▸ hin))

Result:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
acc : Array α
k : Nat
hki : k < n
hin✝ : i ≤ n
hi : i = acc.size
hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩
hin : i < n
this : 1 + (n - (i + 1)) = n - i
⊢ (if h : i < n then ofFn.go f (i + 1) (acc.push (f ⟨i, h⟩)) else acc)[k] = f ⟨k, hki⟩

Proof state:
case hacc
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
acc : Array α
k : Nat
hki : k < n
hin✝ : i ≤ n
hi : i = acc.size
hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩
hin : i < n
this : 1 + (n - (i + 1)) = n - i
j : Nat
hj : j < (acc.push (f ⟨i, hin⟩)).size
⊢ (acc.push (f ⟨i, hin⟩))[j] = f ⟨j, ⋯⟩

Tactic:
cases (Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ (by simpa using hj)) with
| inl hj => simp [getElem_push, hj, hacc j hj]
| inr hj => simp [getElem_push, *]

Result:
no goals

Proof state:
n : Nat
α : Type ?u.455551
f : Fin n → α
i : Nat
acc : Array α
k : Nat
hki : k < n
hin : i ≤ n
hi : i = acc.size
hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩
this : acc.size + (n - acc.size) = n
⊢ k < (ofFn.go f i acc).size

Tactic:
simp [*]

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
acc : Array α
k : Nat
hki : k < n
hin✝ : i ≤ n
hi : i = acc.size
hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩
hin : ¬i < n
⊢ (if h : i < n then ofFn.go f (i + 1) (acc.push (f ⟨i, h⟩)) else acc)[k] = f ⟨k, hki⟩

Tactic:
simp [hin, hacc k (Nat.lt_of_lt_of_le hki (Nat.le_of_not_lt (hi ▸ hin)))]

Result:
no goals

Proof state:
case hacc.inr
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
acc : Array α
k : Nat
hki : k < n
hin✝ : i ≤ n
hi : i = acc.size
hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩
hin : i < n
this : 1 + (n - (i + 1)) = n - i
j : Nat
hj✝ : j < (acc.push (f ⟨i, hin⟩)).size
hj : j = acc.size
⊢ (acc.push (f ⟨i, hin⟩))[j] = f ⟨j, ⋯⟩

Tactic:
simp [getElem_push, *]

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
acc : Array α
k : Nat
hki : k < n
hin✝ : i ≤ n
hi : i = acc.size
hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩
hin : i < n
this : 1 + (n - (i + 1)) = n - i
j : Nat
hj : j < (acc.push (f ⟨i, hin⟩)).size
⊢ ?m.457251 < Nat.succ ?m.457252

Tactic:
simpa using hj

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
acc : Array α
k : Nat
hki : k < n
hin : i ≤ n
hi : i = acc.size
hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩
⊢ (ofFn.go f i acc)[k] = f ⟨k, hki⟩

Tactic:
unfold ofFn.go

Result:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
acc : Array α
k : Nat
hki : k < n
hin : i ≤ n
hi : i = acc.size
hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩
⊢ (if h : i < n then ofFn.go f (i + 1) (acc.push (f ⟨i, h⟩)) else acc)[k] = f ⟨k, hki⟩

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
acc : Array α
k : Nat
hki : k < n
hin✝ : i ≤ n
hi : i = acc.size
hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩
hin : i < n
this : 1 + (n - (i + 1)) = n - i
⊢ (if h : i < n then ofFn.go f (i + 1) (acc.push (f ⟨i, h⟩)) else acc)[k] = f ⟨k, hki⟩

Tactic:
simp only [dif_pos hin]

Result:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
acc : Array α
k : Nat
hki : k < n
hin✝ : i ≤ n
hi : i = acc.size
hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩
hin : i < n
this : 1 + (n - (i + 1)) = n - i
⊢ (ofFn.go f (i + 1) (acc.push (f ⟨i, hin⟩)))[k] = f ⟨k, hki⟩

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
acc : Array α
k : Nat
hki : k < n
hin✝ : i ≤ n
hi : i = acc.size
hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩
hin : i < n
this : 1 + (n - (i + 1)) = n - i
⊢ (ofFn.go f (i + 1) (acc.push (f ⟨i, hin⟩)))[k] = f ⟨k, hki⟩

Tactic:
rw [getElem_ofFn_go f (i+1) _ hin (by simp [*]) (fun j hj => ?hacc)]

Result:
case hacc
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
acc : Array α
k : Nat
hki : k < n
hin✝ : i ≤ n
hi : i = acc.size
hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩
hin : i < n
this : 1 + (n - (i + 1)) = n - i
j : Nat
hj : j < (acc.push (f ⟨i, hin⟩)).size
⊢ (acc.push (f ⟨i, hin⟩))[j] = f ⟨j, ⋯⟩

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
acc : Array α
k : Nat
hki : k < n
hin : i ≤ n
hi : i = acc.size
hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩
⊢ (if h : i < n then ofFn.go f (i + 1) (acc.push (f ⟨i, h⟩)) else acc)[k] = f ⟨k, hki⟩

Tactic:
if hin : i < n then
  have : 1 + (n - (i + 1)) = n - i :=
    Nat.sub_sub .. ▸ Nat.add_sub_cancel' (Nat.le_sub_of_add_le (Nat.add_comm .. ▸ hin))
  simp only [dif_pos hin]
  rw [getElem_ofFn_go f (i+1) _ hin (by simp [*]) (fun j hj => ?hacc)]
  cases (Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ (by simpa using hj)) with
  | inl hj => simp [getElem_push, hj, hacc j hj]
  | inr hj => simp [getElem_push, *]
else
  simp [hin, hacc k (Nat.lt_of_lt_of_le hki (Nat.le_of_not_lt (hi ▸ hin)))]

Result:
no goals

Proof state:
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
acc : Array α
k : Nat
hki : k < n
hin✝ : i ≤ n
hi : i = acc.size
hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩
hin : i < n
this : 1 + (n - (i + 1)) = n - i
⊢ i + 1 = (acc.push (f ⟨i, hin⟩)).size

Tactic:
simp [*]

Result:
no goals

Proof state:
case hacc.inl
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
acc : Array α
k : Nat
hki : k < n
hin✝ : i ≤ n
hi : i = acc.size
hacc : ∀ (j : Nat) (hj : j < acc.size), acc[j] = f ⟨j, ⋯⟩
hin : i < n
this : 1 + (n - (i + 1)) = n - i
j : Nat
hj✝ : j < (acc.push (f ⟨i, hin⟩)).size
hj : j < acc.size
⊢ (acc.push (f ⟨i, hin⟩))[j] = f ⟨j, ⋯⟩

Tactic:
simp [getElem_push, hj, hacc j hj]

Result:
no goals