case h
M : Type u_1
N : Type u_2
P : Type ?u.138500
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.138521
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type ?u.138545
mc : MonoidHomClass F M N
f : M →* N
x : M
⊢ x ∈ mker (mrangeRestrict f) ↔ x ∈ mker f
M : Type u_1
N : Type u_2
P : Type ?u.138500
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.138521
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type ?u.138545
mc : MonoidHomClass F M N
f : M →* N
⊢ mker (mrangeRestrict f) = mker f
ext x
case h
M : Type u_1
N : Type u_2
P : Type ?u.138500
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.138521
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type ?u.138545
mc : MonoidHomClass F M N
f : M →* N
x : M
⊢ { val := ↑f x, property := (_ : ∃ y, ↑f y = ↑f x) } = { val := 1, property := (_ : 1 ∈ mrange f) } ↔ ↑f x = 1
case h
M : Type u_1
N : Type u_2
P : Type ?u.138500
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.138521
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type ?u.138545
mc : MonoidHomClass F M N
f : M →* N
x : M
⊢ x ∈ mker (mrangeRestrict f) ↔ x ∈ mker f
change (⟨f x, _⟩ : mrange f) = ⟨1, _⟩ ↔ f x = 1
no goals
case h
M : Type u_1
N : Type u_2
P : Type ?u.138500
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.138521
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type ?u.138545
mc : MonoidHomClass F M N
f : M →* N
x : M
⊢ { val := ↑f x, property := (_ : ∃ y, ↑f y = ↑f x) } = { val := 1, property := (_ : 1 ∈ mrange f) } ↔ ↑f x = 1
simp