no goals
R : Type u
S✝ : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
inst✝² : NonUnitalNonAssocSemiring S✝
inst✝¹ : NonUnitalNonAssocSemiring T
F : Type ?u.280898
inst✝ : NonUnitalRingHomClass F R S✝
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : Directed (fun x x_1 => x ≤ x_1) S
x : R
⊢ x ∈ ↑(⨆ (i : ι), S i) ↔ x ∈ ⋃ (i : ι), ↑(S i)
simp [mem_iSup_of_directed hS]