Theorem: Secion7Sheet2.id_comp (FormalisingMathematics2024/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
⊢ MonoidHom.comp (MonoidHom.id H) φ = φ
Tactic:
sorry
State after:
no goals