[GOAL]
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H K : Subgroup G
⊢ ∀ (x : { x // x ∈ ⊥ }), x ∈ {1}
[PROOFSTEP]
rintro ⟨x, ⟨hx⟩⟩
[GOAL]
case mk.refl
G : Type u_1
inst✝¹ : Group G
A : Type u_2
inst✝ : AddGroup A
H K : Subgroup G
⊢ { val := 1, property := (_ : 1 = 1) } ∈ {1}
[PROOFSTEP]
exact Finset.mem_singleton_self _
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
H K : Subgroup G
inst✝ : Fintype G
⊢ Fintype.card { x // x ∈ ⊤ } = Fintype.card G
[PROOFSTEP]
rw [Fintype.card_eq]
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
H K : Subgroup G
inst✝ : Fintype G
⊢ Nonempty ({ x // x ∈ ⊤ } ≃ G)
[PROOFSTEP]
exact Nonempty.intro Subgroup.topEquiv.toEquiv
[GOAL]
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
H K : Subgroup G
inst✝¹ : Fintype { x // x ∈ H }
inst✝ : Fintype G
h : Fintype.card { x // x ∈ H } = Fintype.card G
⊢ H = ⊤
[PROOFSTEP]
letI : Fintype (H : Set G) := ‹Fintype H›
[GOAL]
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
H K : Subgroup G
inst✝¹ : Fintype { x // x ∈ H }
inst✝ : Fintype G
h : Fintype.card { x // x ∈ H } = Fintype.card G
this : Fintype ↑↑H := inst✝¹
⊢ H = ⊤
[PROOFSTEP]
rw [SetLike.ext'_iff, coe_top, ← Finset.coe_univ, ← (H : Set G).coe_toFinset, Finset.coe_inj, ←
  Finset.card_eq_iff_eq_univ, ← h, Set.toFinset_card]
[GOAL]
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
H K : Subgroup G
inst✝¹ : Fintype { x // x ∈ H }
inst✝ : Fintype G
h : Fintype.card { x // x ∈ H } = Fintype.card G
this : Fintype ↑↑H := inst✝¹
⊢ Fintype.card ↑↑H = Fintype.card { x // x ∈ H }
[PROOFSTEP]
congr
[GOAL]
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
H K : Subgroup G
inst✝¹ : Fintype { x // x ∈ H }
inst✝ : Fintype G
h : H = ⊤
⊢ Fintype.card { x // x ∈ H } = Fintype.card G
[PROOFSTEP]
simpa only [h] using card_top
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
H K : Subgroup G
inst✝ : Fintype { x // x ∈ H }
h : Fintype.card { x // x ∈ H } ≤ 1
x : G
hx : x ∈ H
⊢ x = 1
[PROOFSTEP]
simpa [Subtype.ext_iff] using Fintype.card_le_one_iff.1 h ⟨x, hx⟩ 1
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
H K : Subgroup G
inst✝ : Fintype { x // x ∈ H }
h : H = ⊥
⊢ Fintype.card { x // x ∈ H } ≤ 1
[PROOFSTEP]
simp [h]
[GOAL]
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
induction' I using Finset.induction_on with i I hnmem ih generalizing x
[GOAL]
case empty
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
convert one_mem H
[GOAL]
case h.e'_4
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
ext i
[GOAL]
case h.e'_4.h
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
exact h1 i (Finset.not_mem_empty i)
[GOAL]
case insert
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
have : x = Function.update x i 1 * Pi.mulSingle i (x i) :=
  by
  ext j
  by_cases heq : j = i
  · subst heq
    simp
  · simp [heq]
[GOAL]
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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)
[PROOFSTEP]
ext j
[GOAL]
case h
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
by_cases heq : j = i
[GOAL]
case pos
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
subst heq
[GOAL]
case pos
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
simp
[GOAL]
case neg
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
simp [heq]
[GOAL]
case insert
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
rw [this]
[GOAL]
case insert
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
clear this
[GOAL]
case insert
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
apply mul_mem
[GOAL]
case insert.a
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
apply ih
[GOAL]
case insert.a.h1
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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_1 : η), ¬i_1 ∈ I → Function.update x i 1 i_1 = 1
[PROOFSTEP]
clear ih
[GOAL]
case insert.a.h2
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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_1 : η), i_1 ∈ I → Pi.mulSingle i_1 (Function.update x i 1 i_1) ∈ H
[PROOFSTEP]
clear ih
[GOAL]
case insert.a.h1
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
intro j hj
[GOAL]
case insert.a.h1
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
by_cases heq : j = i
[GOAL]
case pos
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
subst heq
[GOAL]
case pos
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
simp
[GOAL]
case neg
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
simp [heq]
[GOAL]
case neg
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
apply h1 j
[GOAL]
case neg
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
simpa [heq] using hj
[GOAL]
case insert.a.h2
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
intro j hj
[GOAL]
case insert.a.h2
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
have : j ≠ i := by
  rintro rfl
  contradiction
[GOAL]
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
rintro rfl
[GOAL]
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
contradiction
[GOAL]
case insert.a.h2
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
simp [this]
[GOAL]
case insert.a.h2
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
exact h2 _ (Finset.mem_insert_of_mem hj)
[GOAL]
case insert.a
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
apply h2
[GOAL]
case insert.a.a
G : Type u_1
inst✝³ : Group G
A : Type u_2
inst✝² : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
inst✝⁴ : Group G
A : Type u_2
inst✝³ : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
cases nonempty_fintype η
[GOAL]
case intro
G : Type u_1
inst✝⁴ : Group G
A : Type u_2
inst✝³ : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
exact pi_mem_of_mulSingle_mem_aux Finset.univ x (by simp) fun i _ => h i
[GOAL]
G : Type u_1
inst✝⁴ : Group G
A : Type u_2
inst✝³ : AddGroup A
η : Type u_3
f : η → Type u_4
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
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
inst✝⁴ : Group G
A : Type u_2
inst✝³ : AddGroup A
η : Type u_3
f : η → Type u_4
inst✝² : (i : η) → Group (f i)
inst✝¹ : DecidableEq η
inst✝ : Finite η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ pi univ H ≤ J ↔ ∀ (i : η), map (MonoidHom.single f i) (H i) ≤ J
[PROOFSTEP]
constructor
[GOAL]
case mp
G : Type u_1
inst✝⁴ : Group G
A : Type u_2
inst✝³ : AddGroup A
η : Type u_3
f : η → Type u_4
inst✝² : (i : η) → Group (f i)
inst✝¹ : DecidableEq η
inst✝ : Finite η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ pi univ H ≤ J → ∀ (i : η), map (MonoidHom.single f i) (H i) ≤ J
[PROOFSTEP]
rintro h i _ ⟨x, hx, rfl⟩
[GOAL]
case mp.intro.intro
G : Type u_1
inst✝⁴ : Group G
A : Type u_2
inst✝³ : AddGroup A
η : Type u_3
f : η → Type u_4
inst✝² : (i : η) → Group (f i)
inst✝¹ : DecidableEq η
inst✝ : Finite η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
h : pi univ H ≤ J
i : η
x : f i
hx : x ∈ ↑(H i)
⊢ ↑(MonoidHom.single f i) x ∈ J
[PROOFSTEP]
apply h
[GOAL]
case mp.intro.intro.a
G : Type u_1
inst✝⁴ : Group G
A : Type u_2
inst✝³ : AddGroup A
η : Type u_3
f : η → Type u_4
inst✝² : (i : η) → Group (f i)
inst✝¹ : DecidableEq η
inst✝ : Finite η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
h : pi univ H ≤ J
i : η
x : f i
hx : x ∈ ↑(H i)
⊢ ↑(MonoidHom.single f i) x ∈ pi univ H
[PROOFSTEP]
simpa using hx
[GOAL]
case mpr
G : Type u_1
inst✝⁴ : Group G
A : Type u_2
inst✝³ : AddGroup A
η : Type u_3
f : η → Type u_4
inst✝² : (i : η) → Group (f i)
inst✝¹ : DecidableEq η
inst✝ : Finite η
H : (i : η) → Subgroup (f i)
J : Subgroup ((i : η) → f i)
⊢ (∀ (i : η), map (MonoidHom.single f i) (H i) ≤ J) → pi univ H ≤ J
[PROOFSTEP]
exact fun h x hx => pi_mem_of_mulSingle_mem x fun i => h i (mem_map_of_mem _ (hx i trivial))
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ (n : G), n ∈ S → x * n * x⁻¹ ∈ S
⊢ x ∈ setNormalizer S
[PROOFSTEP]
haveI := Classical.propDecidable
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ (n : G), n ∈ S → x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
⊢ x ∈ setNormalizer S
[PROOFSTEP]
cases nonempty_fintype S
[GOAL]
case intro
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ (n : G), n ∈ S → x * n * x⁻¹ ∈ S
this : (a : Prop) → Decidable a
val✝ : Fintype ↑S
⊢ x ∈ setNormalizer S
[PROOFSTEP]
haveI := Set.fintypeImage S fun n => x * n * x⁻¹
[GOAL]
case intro
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ (n : G), n ∈ S → x * n * x⁻¹ ∈ S
this✝ : (a : Prop) → Decidable a
val✝ : Fintype ↑S
this : Fintype ↑((fun n => x * n * x⁻¹) '' S)
⊢ x ∈ setNormalizer S
[PROOFSTEP]
exact fun n =>
  ⟨h n, fun h₁ =>
    have heq : (fun n => x * n * x⁻¹) '' S = S :=
      Set.eq_of_subset_of_card_le (fun n ⟨y, hy⟩ => hy.2 ▸ h y hy.1)
        (by rw [Set.card_image_of_injective S conj_injective])
    have : x * n * x⁻¹ ∈ (fun n => x * n * x⁻¹) '' S := heq.symm ▸ h₁
    let ⟨y, hy⟩ := this
    conj_injective hy.2 ▸ hy.1⟩
[GOAL]
G : Type u_1
inst✝² : Group G
A : Type u_2
inst✝¹ : AddGroup A
S : Set G
inst✝ : Finite ↑S
x : G
h : ∀ (n : G), n ∈ S → x * n * x⁻¹ ∈ S
this✝ : (a : Prop) → Decidable a
val✝ : Fintype ↑S
this : Fintype ↑((fun n => x * n * x⁻¹) '' S)
n : G
h₁ : x * n * x⁻¹ ∈ S
⊢ Fintype.card ↑S ≤ Fintype.card ↑((fun n => x * n * x⁻¹) '' S)
[PROOFSTEP]
rw [Set.card_image_of_injective S conj_injective]
