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

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