Theorem: id_comp (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 H) φ = φ
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 H) φ) 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 H) φ) x = φ x
Tactic:
rfl
State after:
no goals