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

State before:
n : ℕ
α : Type u
δ✝ : Type u_1
f : α → δ✝
⊢ f ∘ ![] = ![]
Tactic:
simp[Matrix.empty_eq]
State after:
no goals