Theorem: Matrix.comp_vecCons (Logic/Vorspiel/Vorspiel.lean)

State before:
n : ℕ
α : Type u
β : Type u_1
f : α → β
a : α
s : Fin n → α
i : Fin n.succ
⊢ f ((a :> s) 0) = (f a :> f ∘ s) 0
Tactic:
simp
State after:
no goals

State before:
n : ℕ
α : Type u
β : Type u_1
f : α → β
a : α
s : Fin n → α
i : Fin n.succ
⊢ ∀ (i : Fin n), f ((a :> s) i.succ) = (f a :> f ∘ s) i.succ
Tactic:
simp
State after:
no goals