Theorem: Vector.ofFn_vecCons (Logic/Vorspiel/Vorspiel.lean)

State before:
α : Type u_1
n : ℕ
a : α
v : Fin n → α
⊢ ofFn (a :> v) = a ::ᵥ ofFn v
Tactic:
ext i
State after:
case x
α : Type u_1
n : ℕ
a : α
v : Fin n → α
i : Fin n.succ
⊢ (ofFn (a :> v)).get i = (a ::ᵥ ofFn v).get i

State before:
case x
α : Type u_1
n : ℕ
a : α
v : Fin n → α
i : Fin n.succ
⊢ (ofFn (a :> v)).get i = (a ::ᵥ ofFn v).get i
Tactic:
cases i using Fin.cases <;> simp
State after:
no goals