Theorem: Vector.of_Fn'_get (Saturn/Vector.lean)

State before:
α : Type
n : ℕ
⊢ ∀ (seq : FinSeq n α) (k : Fin n), get (ofFn' seq) k = seq ↑k (_ : ↑k < n)
Tactic:
intro seq ⟨k, kw⟩
State after:
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n
⊢ get (ofFn' seq) { val := k, isLt := kw } = seq ↑{ val := k, isLt := kw } (_ : ↑{ val := k, isLt := kw } < n)

State before:
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n
⊢ get (ofFn' seq) { val := k, isLt := kw } = seq ↑{ val := k, isLt := kw } (_ : ↑{ val := k, isLt := kw } < n)
Tactic:
let lem := congrFun (Vector.of_Fn'_get' seq) k
State after:
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n
lem : get' (ofFn' seq) k = seq k := congrFun (of_Fn'_get' seq) k
⊢ get (ofFn' seq) { val := k, isLt := kw } = seq ↑{ val := k, isLt := kw } (_ : ↑{ val := k, isLt := kw } < n)

State before:
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n
lem : get' (ofFn' seq) k = seq k := congrFun (of_Fn'_get' seq) k
⊢ get (ofFn' seq) { val := k, isLt := kw } = seq ↑{ val := k, isLt := kw } (_ : ↑{ val := k, isLt := kw } < n)
Tactic:
let lem' := (congrFun lem kw)
State after:
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n
lem : get' (ofFn' seq) k = seq k := congrFun (of_Fn'_get' seq) k
lem' : get' (ofFn' seq) k kw = seq k kw := congrFun lem kw
⊢ get (ofFn' seq) { val := k, isLt := kw } = seq ↑{ val := k, isLt := kw } (_ : ↑{ val := k, isLt := kw } < n)

State before:
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n
lem : get' (ofFn' seq) k = seq k := congrFun (of_Fn'_get' seq) k
lem' : get' (ofFn' seq) k kw = seq k kw := congrFun lem kw
⊢ get (ofFn' seq) { val := k, isLt := kw } = seq ↑{ val := k, isLt := kw } (_ : ↑{ val := k, isLt := kw } < n)
Tactic:
exact lem'
State after:
no goals