no goals
ι : Sort ?u.3746
M : Type u_1
A : Type ?u.3752
B : Type ?u.3755
inst✝ : Mul M
S : Set (Subsemigroup M)
hS : DirectedOn (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ sSup S ↔ ∃ s, s ∈ S ∧ x ∈ s
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, Subtype.coe_mk,
  exists_prop]