Theorem: Secion7Sheet2.comp_id (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 G) = φ
Tactic:
sorry
State after:
no goals