Theorem: Vector.get'_of_Fn' (Saturn/Vector.lean)

State before:
α : Type
n : ℕ
f : (k : ℕ) → k < n → α
k : ℕ
kw : k < n
⊢ get' (ofFn' f) k kw = f k kw
Tactic:
let lem := Vector.of_Fn'_get' f
State after:
α : Type
n : ℕ
f : (k : ℕ) → k < n → α
k : ℕ
kw : k < n
lem : get' (ofFn' f) = f := of_Fn'_get' f
⊢ get' (ofFn' f) k kw = f k kw

State before:
α : Type
n : ℕ
f : (k : ℕ) → k < n → α
k : ℕ
kw : k < n
lem : get' (ofFn' f) = f := of_Fn'_get' f
⊢ get' (ofFn' f) k kw = f k kw
Tactic:
let lem' := congrFun lem k
State after:
α : Type
n : ℕ
f : (k : ℕ) → k < n → α
k : ℕ
kw : k < n
lem : get' (ofFn' f) = f := of_Fn'_get' f
lem' : get' (ofFn' f) k = f k := congrFun lem k
⊢ get' (ofFn' f) k kw = f k kw

State before:
α : Type
n : ℕ
f : (k : ℕ) → k < n → α
k : ℕ
kw : k < n
lem : get' (ofFn' f) = f := of_Fn'_get' f
lem' : get' (ofFn' f) k = f k := congrFun lem k
⊢ get' (ofFn' f) k kw = f k kw
Tactic:
apply congrFun lem'
State after:
no goals