case intro
G : Type ?u.35743
inst✝⁴ : Group G
A : Type ?u.35749
inst✝³ : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝² : (i : η) → Group (f i)
inst✝¹ : Finite η
inst✝ : DecidableEq η
H : Subgroup ((i : η) → f i)
x : (i : η) → f i
h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H
val✝ : Fintype η
⊢ x ∈ H
G : Type ?u.35743
inst✝⁴ : Group G
A : Type ?u.35749
inst✝³ : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝² : (i : η) → Group (f i)
inst✝¹ : Finite η
inst✝ : DecidableEq η
H : Subgroup ((i : η) → f i)
x : (i : η) → f i
h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H
⊢ x ∈ H
cases nonempty_fintype η
no goals
case intro
G : Type ?u.35743
inst✝⁴ : Group G
A : Type ?u.35749
inst✝³ : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝² : (i : η) → Group (f i)
inst✝¹ : Finite η
inst✝ : DecidableEq η
H : Subgroup ((i : η) → f i)
x : (i : η) → f i
h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H
val✝ : Fintype η
⊢ x ∈ H
exact pi_mem_of_mulSingle_mem_aux Finset.univ x (by simp) fun i _ => h i
no goals
G : Type ?u.35743
inst✝⁴ : Group G
A : Type ?u.35749
inst✝³ : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝² : (i : η) → Group (f i)
inst✝¹ : Finite η
inst✝ : DecidableEq η
H : Subgroup ((i : η) → f i)
x : (i : η) → f i
h : ∀ (i : η), Pi.mulSingle i (x i) ∈ H
val✝ : Fintype η
⊢ ∀ (i : η), ¬i ∈ Finset.univ → x i = 1
simp