Theorem: List.get_ofFn (LeanSAT/Reflect/BoolExpr/Nat.lean)

State before:
k : Nat
α : Type ?u.7201
f : Fin k → α
i : Fin (ofFn f).length
⊢ (ofFn f).length = k
Tactic:
simp
State after:
no goals

State before:
k : Nat
α : Type u_1
f : Fin k → α
i : Fin (ofFn f).length
⊢ (ofFn f).get i = f (Fin.cast ⋯ i)
Tactic:
rcases i with ⟨i, hi⟩
State after:
case mk
k : Nat
α : Type u_1
f : Fin k → α
i : Nat
hi : i < (ofFn f).length
⊢ (ofFn f).get ⟨i, hi⟩ = f (Fin.cast ⋯ ⟨i, hi⟩)

State before:
case mk
k : Nat
α : Type u_1
f : Fin k → α
i : Nat
hi : i < (ofFn f).length
⊢ (ofFn f).get ⟨i, hi⟩ = f (Fin.cast ⋯ ⟨i, hi⟩)
Tactic:
simp [ofFn, get_ofFn_go]
State after:
no goals