no goals
G : Type u_2
G' : Type ?u.226690
inst✝³ : Group G
inst✝² : Group G'
A : Type ?u.226699
inst✝¹ : AddGroup A
H K : Subgroup G
k : Set G
ι : Sort u_1
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : Directed (fun x x_1 => x ≤ x_1) S
x : G
⊢ x ∈ ↑(⨆ (i : ι), S i) ↔ x ∈ ⋃ (i : ι), ↑(S i)
simp [mem_iSup_of_directed hS]