case h
G : Type u_2
G' : Type ?u.511685
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.511694
inst✝⁴ : AddGroup A
N : Type ?u.511700
P : Type ?u.511703
inst✝³ : Group N
inst✝² : Group P
K : Subgroup G
M✝ : Type ?u.511720
inst✝¹ : MulOneClass M✝
M : Type u_1
inst✝ : Monoid M
f : G →* M
x : G
⊢ x ∈ ker (toHomUnits f) ↔ x ∈ ker f
G : Type u_2
G' : Type ?u.511685
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.511694
inst✝⁴ : AddGroup A
N : Type ?u.511700
P : Type ?u.511703
inst✝³ : Group N
inst✝² : Group P
K : Subgroup G
M✝ : Type ?u.511720
inst✝¹ : MulOneClass M✝
M : Type u_1
inst✝ : Monoid M
f : G →* M
⊢ ker (toHomUnits f) = ker f
ext x
no goals
case h
G : Type u_2
G' : Type ?u.511685
inst✝⁶ : Group G
inst✝⁵ : Group G'
A : Type ?u.511694
inst✝⁴ : AddGroup A
N : Type ?u.511700
P : Type ?u.511703
inst✝³ : Group N
inst✝² : Group P
K : Subgroup G
M✝ : Type ?u.511720
inst✝¹ : MulOneClass M✝
M : Type u_1
inst✝ : Monoid M
f : G →* M
x : G
⊢ x ∈ ker (toHomUnits f) ↔ x ∈ ker f
simp [mem_ker, Units.ext_iff]