case h
M : Type u_1
N : Type u_2
P : Type ?u.143655
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.143676
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type ?u.143700
mc : MonoidHomClass F M N
x : M
⊢ x ∈ mker (inl M N) ↔ x ∈ ⊥
M : Type u_1
N : Type u_2
P : Type ?u.143655
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.143676
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type ?u.143700
mc : MonoidHomClass F M N
⊢ mker (inl M N) = ⊥
ext x
no goals
case h
M : Type u_1
N : Type u_2
P : Type ?u.143655
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.143676
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
F : Type ?u.143700
mc : MonoidHomClass F M N
x : M
⊢ x ∈ mker (inl M N) ↔ x ∈ ⊥
simp [mem_mker]