case empty
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I → Pi.mulSingle i (x✝ i) ∈ H
x : (i : η) → f i
h1 : ∀ (i : η), ¬i ∈ ∅ → x i = 1
h2 : ∀ (i : η), i ∈ ∅ → Pi.mulSingle i (x i) ∈ H
⊢ x ∈ H

case insert
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
⊢ x ∈ H
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Finset η
H : Subgroup ((i : η) → f i)
x : (i : η) → f i
h1 : ∀ (i : η), ¬i ∈ I → x i = 1
h2 : ∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H
⊢ x ∈ H
induction' I using Finset.induction_on with i I hnmem ih generalizing x
case h.e'_4
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I → Pi.mulSingle i (x✝ i) ∈ H
x : (i : η) → f i
h1 : ∀ (i : η), ¬i ∈ ∅ → x i = 1
h2 : ∀ (i : η), i ∈ ∅ → Pi.mulSingle i (x i) ∈ H
⊢ x = 1
case empty
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I → Pi.mulSingle i (x✝ i) ∈ H
x : (i : η) → f i
h1 : ∀ (i : η), ¬i ∈ ∅ → x i = 1
h2 : ∀ (i : η), i ∈ ∅ → Pi.mulSingle i (x i) ∈ H
⊢ x ∈ H
convert one_mem H
case h.e'_4.h
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I → Pi.mulSingle i (x✝ i) ∈ H
x : (i : η) → f i
h1 : ∀ (i : η), ¬i ∈ ∅ → x i = 1
h2 : ∀ (i : η), i ∈ ∅ → Pi.mulSingle i (x i) ∈ H
i : η
⊢ x i = OfNat.ofNat 1 i
case h.e'_4
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I → Pi.mulSingle i (x✝ i) ∈ H
x : (i : η) → f i
h1 : ∀ (i : η), ¬i ∈ ∅ → x i = 1
h2 : ∀ (i : η), i ∈ ∅ → Pi.mulSingle i (x i) ∈ H
⊢ x = 1
ext i
no goals
case h.e'_4.h
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I → Pi.mulSingle i (x✝ i) ∈ H
x : (i : η) → f i
h1 : ∀ (i : η), ¬i ∈ ∅ → x i = 1
h2 : ∀ (i : η), i ∈ ∅ → Pi.mulSingle i (x i) ∈ H
i : η
⊢ x i = OfNat.ofNat 1 i
exact h1 i (Finset.not_mem_empty i)
case insert
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
this : x = Function.update x i 1 * Pi.mulSingle i (x i)
⊢ Function.update x i 1 * Pi.mulSingle i (x i) ∈ H
case insert
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
this : x = Function.update x i 1 * Pi.mulSingle i (x i)
⊢ x ∈ H
rw [this]
case insert
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
⊢ Function.update x i 1 * Pi.mulSingle i (x i) ∈ H
case insert
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
this : x = Function.update x i 1 * Pi.mulSingle i (x i)
⊢ Function.update x i 1 * Pi.mulSingle i (x i) ∈ H
clear this
case insert.a
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
⊢ Function.update x i 1 ∈ H

case insert.a
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
⊢ Pi.mulSingle i (x i) ∈ H
case insert
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
⊢ Function.update x i 1 * Pi.mulSingle i (x i) ∈ H
apply mul_mem
case h
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
⊢ x j = (Function.update x i 1 * Pi.mulSingle i (x i)) j
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
⊢ x = Function.update x i 1 * Pi.mulSingle i (x i)
ext j
case pos
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
heq : j = i
⊢ x j = (Function.update x i 1 * Pi.mulSingle i (x i)) j

case neg
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
heq : ¬j = i
⊢ x j = (Function.update x i 1 * Pi.mulSingle i (x i)) j
case h
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
⊢ x j = (Function.update x i 1 * Pi.mulSingle i (x i)) j
by_cases heq : j = i
case pos
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
I : Finset η
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
j : η
hnmem : ¬j ∈ I
h1 : ∀ (i : η), ¬i ∈ insert j I → x i = 1
h2 : ∀ (i : η), i ∈ insert j I → Pi.mulSingle i (x i) ∈ H
⊢ x j = (Function.update x j 1 * Pi.mulSingle j (x j)) j
case pos
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
heq : j = i
⊢ x j = (Function.update x i 1 * Pi.mulSingle i (x i)) j
subst heq
no goals
case pos
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
I : Finset η
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
j : η
hnmem : ¬j ∈ I
h1 : ∀ (i : η), ¬i ∈ insert j I → x i = 1
h2 : ∀ (i : η), i ∈ insert j I → Pi.mulSingle i (x i) ∈ H
⊢ x j = (Function.update x j 1 * Pi.mulSingle j (x j)) j
simp
no goals
case neg
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
heq : ¬j = i
⊢ x j = (Function.update x i 1 * Pi.mulSingle i (x i)) j
simp [heq]
case insert.a.h1
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
⊢ ∀ (i_1 : η), ¬i_1 ∈ I → Function.update x i 1 i_1 = 1

case insert.a.h2
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
⊢ ∀ (i_1 : η), i_1 ∈ I → Pi.mulSingle i_1 (Function.update x i 1 i_1) ∈ H
case insert.a
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
⊢ Function.update x i 1 ∈ H
apply ih <;> clear ih
case insert.a.h1
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : ¬j ∈ I
⊢ Function.update x i 1 j = 1
case insert.a.h1
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
⊢ ∀ (i_1 : η), ¬i_1 ∈ I → Function.update x i 1 i_1 = 1
intro j hj
case pos
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : ¬j ∈ I
heq : j = i
⊢ Function.update x i 1 j = 1

case neg
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : ¬j ∈ I
heq : ¬j = i
⊢ Function.update x i 1 j = 1
case insert.a.h1
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : ¬j ∈ I
⊢ Function.update x i 1 j = 1
by_cases heq : j = i
case pos
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
I : Finset η
x : (i : η) → f i
j : η
hj hnmem : ¬j ∈ I
h1 : ∀ (i : η), ¬i ∈ insert j I → x i = 1
h2 : ∀ (i : η), i ∈ insert j I → Pi.mulSingle i (x i) ∈ H
⊢ Function.update x j 1 j = 1
case pos
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : ¬j ∈ I
heq : j = i
⊢ Function.update x i 1 j = 1
subst heq
no goals
case pos
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
I : Finset η
x : (i : η) → f i
j : η
hj hnmem : ¬j ∈ I
h1 : ∀ (i : η), ¬i ∈ insert j I → x i = 1
h2 : ∀ (i : η), i ∈ insert j I → Pi.mulSingle i (x i) ∈ H
⊢ Function.update x j 1 j = 1
simp
case neg
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : ¬j ∈ I
heq : ¬j = i
⊢ x j = 1
case neg
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : ¬j ∈ I
heq : ¬j = i
⊢ Function.update x i 1 j = 1
simp [heq]
case neg
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : ¬j ∈ I
heq : ¬j = i
⊢ ¬j ∈ insert i I
case neg
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : ¬j ∈ I
heq : ¬j = i
⊢ x j = 1
apply h1 j
no goals
case neg
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : ¬j ∈ I
heq : ¬j = i
⊢ ¬j ∈ insert i I
simpa [heq] using hj
case insert.a.h2
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∈ I
⊢ Pi.mulSingle j (Function.update x i 1 j) ∈ H
case insert.a.h2
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
⊢ ∀ (i_1 : η), i_1 ∈ I → Pi.mulSingle i_1 (Function.update x i 1 i_1) ∈ H
intro j hj
case insert.a.h2
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∈ I
this : j ≠ i
⊢ Pi.mulSingle j (Function.update x i 1 j) ∈ H
case insert.a.h2
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∈ I
⊢ Pi.mulSingle j (Function.update x i 1 j) ∈ H
have : j ≠ i := by
  rintro rfl
  contradiction
case insert.a.h2
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∈ I
this : j ≠ i
⊢ Pi.mulSingle j (x j) ∈ H
case insert.a.h2
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∈ I
this : j ≠ i
⊢ Pi.mulSingle j (Function.update x i 1 j) ∈ H
simp [this]
no goals
case insert.a.h2
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∈ I
this : j ≠ i
⊢ Pi.mulSingle j (x j) ∈ H
exact h2 _ (Finset.mem_insert_of_mem hj)
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
I : Finset η
x : (i : η) → f i
j : η
hj : j ∈ I
hnmem : ¬j ∈ I
h1 : ∀ (i : η), ¬i ∈ insert j I → x i = 1
h2 : ∀ (i : η), i ∈ insert j I → Pi.mulSingle i (x i) ∈ H
⊢ False
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
j : η
hj : j ∈ I
⊢ j ≠ i
rintro rfl
no goals
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
I : Finset η
x : (i : η) → f i
j : η
hj : j ∈ I
hnmem : ¬j ∈ I
h1 : ∀ (i : η), ¬i ∈ insert j I → x i = 1
h2 : ∀ (i : η), i ∈ insert j I → Pi.mulSingle i (x i) ∈ H
⊢ False
contradiction
case insert.a.a
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
⊢ i ∈ insert i I
case insert.a
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
⊢ Pi.mulSingle i (x i) ∈ H
apply h2
no goals
case insert.a.a
G : Type ?u.19680
inst✝³ : Group G
A : Type ?u.19686
inst✝² : AddGroup A
η : Type u_1
f : η → Type u_2
inst✝¹ : (i : η) → Group (f i)
inst✝ : DecidableEq η
I✝ : Finset η
H : Subgroup ((i : η) → f i)
x✝ : (i : η) → f i
h1✝ : ∀ (i : η), ¬i ∈ I✝ → x✝ i = 1
h2✝ : ∀ (i : η), i ∈ I✝ → Pi.mulSingle i (x✝ i) ∈ H
i : η
I : Finset η
hnmem : ¬i ∈ I
ih : ∀ (x : (i : η) → f i), (∀ (i : η), ¬i ∈ I → x i = 1) → (∀ (i : η), i ∈ I → Pi.mulSingle i (x i) ∈ H) → x ∈ H
x : (i : η) → f i
h1 : ∀ (i_1 : η), ¬i_1 ∈ insert i I → x i_1 = 1
h2 : ∀ (i_1 : η), i_1 ∈ insert i I → Pi.mulSingle i_1 (x i_1) ∈ H
⊢ i ∈ insert i I
simp