case h
M : Type u_1
N : Type u_2
P : Type ?u.140375
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.140396
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type ?u.140420
mc : MonoidHomClass F M N
x✝ : M
⊢ x✝ ∈ mker 1 ↔ x✝ ∈ ⊤
M : Type u_1
N : Type u_2
P : Type ?u.140375
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.140396
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type ?u.140420
mc : MonoidHomClass F M N
⊢ mker 1 = ⊤
ext
no goals
case h
M : Type u_1
N : Type u_2
P : Type ?u.140375
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.140396
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type ?u.140420
mc : MonoidHomClass F M N
x✝ : M
⊢ x✝ ∈ mker 1 ↔ x✝ ∈ ⊤
simp [mem_mker]