no goals
G : Type ?u.318819
G' : Type ?u.318822
inst✝⁵ : Group G
inst✝⁴ : Group G'
A : Type ?u.318831
inst✝³ : AddGroup A
H✝ K : Subgroup G
k : Set G
N : Type ?u.318852
inst✝² : Group N
P : Type ?u.318858
inst✝¹ : Group P
η : Type u_2
f : η → Type u_1
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
x : (i : η) → f i
⊢ x ∈ pi ∅ H ↔ x ∈ ⊤
simp [mem_pi]