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

State before:
α : Type u_1
β : Type u_2
γ : Type ?u.77130
δ : Type ?u.77133
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F G H K : α ⥤ β
η₁ : NatTrans H K
η₂ : NatTrans G H
η₃ : NatTrans F G
⊢ comp (comp η₁ η₂) η₃ = comp η₁ (comp η₂ η₃)
Tactic:
ext
State after:
case app.h
α : Type u_1
β : Type u_2
γ : Type ?u.77130
δ : Type ?u.77133
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F G H K : α ⥤ β
η₁ : NatTrans H K
η₂ : NatTrans G H
η₃ : NatTrans F G
x✝ : α
⊢ app (comp (comp η₁ η₂) η₃) x✝ = app (comp η₁ (comp η₂ η₃)) x✝

State before:
case app.h
α : Type u_1
β : Type u_2
γ : Type ?u.77130
δ : Type ?u.77133
A B C D : α
inst✝³ : Category α
inst✝² : Category β
inst✝¹ : Category γ
inst✝ : Category δ
F G H K : α ⥤ β
η₁ : NatTrans H K
η₂ : NatTrans G H
η₃ : NatTrans F G
x✝ : α
⊢ app (comp (comp η₁ η₂) η₃) x✝ = app (comp η₁ (comp η₂ η₃)) x✝
Tactic:
simp
State after:
no goals