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

State before:
α : Type
n : ℕ
⊢ ∀ (seq : FinSeq n α), get' (ofFn' seq) = seq
Tactic:
intro seq
State after:
α : Type
n : ℕ
seq : FinSeq n α
⊢ get' (ofFn' seq) = seq

State before:
α : Type
n : ℕ
seq : FinSeq n α
⊢ get' (ofFn' seq) = seq
Tactic:
apply funext
State after:
case h
α : Type
n : ℕ
seq : FinSeq n α
⊢ ∀ (x : ℕ), get' (ofFn' seq) x = seq x

State before:
case h
α : Type
n : ℕ
seq : FinSeq n α
⊢ ∀ (x : ℕ), get' (ofFn' seq) x = seq x
Tactic:
intro k
State after:
case h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
⊢ get' (ofFn' seq) k = seq k

State before:
case h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
⊢ get' (ofFn' seq) k = seq k
Tactic:
apply funext
State after:
case h.h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
⊢ ∀ (x : k < n), get' (ofFn' seq) k x = seq k x

State before:
case h.h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
⊢ ∀ (x : k < n), get' (ofFn' seq) k x = seq k x
Tactic:
intro kw
State after:
case h.h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n
⊢ get' (ofFn' seq) k kw = seq k kw

State before:
case h.h
α : Type
n : ℕ
seq : FinSeq n α
k : ℕ
kw : k < n
⊢ get' (ofFn' seq) k kw = seq k kw
Tactic:
simp [Vector.get', Vector.ofFn']
State after:
no goals