Theorem: Matrix.comp₃ (Logic/Vorspiel/Vorspiel.lean)

State before:
n : ℕ
α : Type u
δ✝ : Type u_1
f : α → δ✝
a₁ a₂ a₃ : α
⊢ f ∘ ![a₁, a₂, a₃] = ![f a₁, f a₂, f a₃]
Tactic:
simp[comp_vecCons'']
State after:
no goals