Theorem: comp_id (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
⊢ MonoidHom.comp φ (MonoidHom.id G) = φ
Tactic:
ext x
State after:
case h
G H : Type
inst✝² : Group G
inst✝¹ : Group H
φ : G →* H
a : G
K : Type
inst✝ : Group K
ψ : H →* K
x : G
⊢ (MonoidHom.comp φ (MonoidHom.id G)) x = φ x

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