no goals
M : Type u_1
N : Type ?u.166126
P : Type ?u.166129
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S✝ : Submonoid M
A : Type ?u.166150
inst✝ : SetLike A M
hA : SubmonoidClass A M
S' : A
S : Submonoid M
⊢ S = ⊥ ∨ Nontrivial { x // x ∈ S }
simp only [eq_bot_iff_forall, nontrivial_iff_exists_ne_one, ← not_forall, ← not_imp, Classical.em]