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

State before:
n : ℕ
α : Type u
β : Type u_1
f : α → β
v : Fin (n + 1) → α
⊢ vecHead (f ∘ v) = f (vecHead v)
Tactic:
simp[vecHead]
State after:
no goals