Theorem: Tutorial.comp_app (Solution/Advanced/Category/Lecture1.lean)

State before:
C : Type u
inst✝ : Category C
a b c d e : C
X Y Z : Type
f : Hom X Y
g : Hom Y Z
x : X
⊢ (f ≫ g) x = g (f x)
Tactic:
rfl
State after:
no goals