no goals
ι : Sort ?u.4507
M : Type u_1
A : Type ?u.4513
B : Type ?u.4516
inst✝ : Mul M
S : Set (Subsemigroup M)
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ (s : Subsemigroup M) (_ : s ∈ S), ↑s
simp [mem_sSup_of_directed_on hS]