Theorem: Qq.compVecCons (Logic/Vorspiel/Meta.lean)

State before:
α : Type u
β : Type v
f : α → β
n : ℕ
a : α
as : Fin n → α
b : β
bs : Fin n → β
hb : f a = b
hbs : f ∘ as = bs
⊢ f ∘ (a :> as) = b :> bs
Tactic:
simp[Function.comp, Matrix.comp_vecCons, hb, ←hbs]
State after:
no goals