no goals
M : Type u_1
N : Type ?u.160395
P : Type ?u.160398
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M
A : Type ?u.160419
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
⊢ (∀ (x : M), x ∈ S ↔ x ∈ ⊥) ↔ ∀ (x : M), x ∈ S → x = 1
simp (config := { contextual := true }) [iff_def, S.one_mem]