no goals
M : Type u_1
A : Type ?u.40177
B : Type ?u.40180
inst✝ : MulOneClass M
S : Set (Submonoid M)
Sne : Set.Nonempty S
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ (s : Submonoid M) (_ : s ∈ S), ↑s
simp [mem_sSup_of_directedOn Sne hS]