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

State before:
n : ℕ
α : Type u
β : Type u_1
f : α → β
a : α
s : Fin n → α
i : Fin n.succ
⊢ f ((s <: a) (last n)) = (f ∘ s <: f a) (last n)
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 ((s <: a) i.castSucc) = (f ∘ s <: f a) i.castSucc
Tactic:
simp
State after:
no goals