no goals
G : Type u_2
G' : Type ?u.188426
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.188435
inst✝ : AddGroup A
H K : Subgroup G
ι : Sort u_1
S : ι → Subgroup G
x : G
⊢ (x ∈ ⨅ (i : ι), S i) ↔ ∀ (i : ι), x ∈ S i
simp only [iInf, mem_sInf, Set.forall_range_iff]