Theorem: Array.get_ofFn (GMLInit/Data/Array/Basic.lean)

State before:
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ (ofFn f).get i = f (⋯ ▸ i)
Tactic:
rw [get_eq_getElem, getElem_ofFn]
State after:
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ f ⟨↑i, ⋯⟩ = f (⋯ ▸ i)

State before:
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ f ⟨↑i, ⋯⟩ = f (⋯ ▸ i)
Tactic:
congr 1
State after:
case e_a
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ ⟨↑i, ⋯⟩ = ⋯ ▸ i

State before:
case e_a
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ ⟨↑i, ⋯⟩ = ⋯ ▸ i
Tactic:
ext
State after:
case e_a.h
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ ↑⟨↑i, ⋯⟩ = ↑(⋯ ▸ i)

State before:
case e_a.h
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ ↑⟨↑i, ⋯⟩ = ↑(⋯ ▸ i)
Tactic:
simp only
State after:
case e_a.h
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ ↑i = ↑(⋯ ▸ i)

State before:
case e_a.h
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ ↑i = ↑(⋯ ▸ i)
Tactic:
apply Fin.val_eq_val_of_heq (size_ofFn ..)
State after:
case e_a.h.a
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ i ≅ ⋯ ▸ i

State before:
case e_a.h.a
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ i ≅ ⋯ ▸ i
Tactic:
elim_casts
State after:
case e_a.h.a
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ i ≅ i

State before:
case e_a.h.a
n : Nat
α : Type u_1
f : Fin n → α
i : Fin (ofFn f).size
⊢ i ≅ i
Tactic:
rfl
State after:
no goals