Theorem: comp_assoc (FormalisingMathematics2024/Solutions/Section07subgroupsAndHomomorphisms/Sheet2.lean)

State before:
G H : Type
inst✝³ : Group G
inst✝² : Group H
φ : G →* H
a : G
K : Type
inst✝¹ : Group K
ψ : H →* K
L : Type
inst✝ : Group L
ρ : K →* L
⊢ MonoidHom.comp (MonoidHom.comp ρ ψ) φ = MonoidHom.comp ρ (MonoidHom.comp ψ φ)
Tactic:
rfl
State after:
no goals