no goals
G : Type ?u.316307
G' : Type ?u.316310
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.316319
inst✝³ : AddGroup A
H K : Subgroup G
k : Set G
N : Type ?u.316340
inst✝² : Group N
P : Type ?u.316346
inst✝¹ : Group P
η : Type u_1
f : η → Type u_2
inst✝ : (i : η) → Group (f i)
I : Set η
x : (i : η) → f i
⊢ (x ∈ pi I fun i => ⊤) ↔ x ∈ ⊤
simp [mem_pi]