Theorem: Category.Functor.comp_assoc (CategoryTheory/Basic.lean)

State before:
α : Type u_7
β : Type u_5
γ : Type u_1
δ : Type u_2
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
H : γ ⥤ δ
G : β ⥤ γ
F : α ⥤ β
⊢ (H ◌ G) ◌ F = H ◌ G ◌ F
Tactic:
aesop
State after:
no goals