no goals
ι : Sort u_2
M : Type u_1
A : Type ?u.1446
B : Type ?u.1449
inst✝ : Mul M
S : ι → Subsemigroup M
hS : Directed (fun x x_1 => x ≤ x_1) S
x : M
⊢ x ∈ ↑(⨆ (i : ι), S i) ↔ x ∈ ⋃ (i : ι), ↑(S i)
simp [mem_iSup_of_directed hS]