no goals
M : Type u_2
A : Type ?u.34491
B : Type ?u.34494
inst✝¹ : MulOneClass M
ι : Sort u_1
inst✝ : Nonempty ι
S : ι → Submonoid 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]