[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
f : ι → G
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem : ∀ (x : ι), x ∈ s → f x ∈ K x
heq1 : Finset.noncommProd s f comm = 1
⊢ ∀ (i : ι), i ∈ s → f i = 1
[PROOFSTEP]
classical
revert heq1
induction' s using Finset.induction_on with i s hnmem ih
· simp
· have hcomm := comm.mono (Finset.coe_subset.2 <| Finset.subset_insert _ _)
  simp only [Finset.forall_mem_insert] at hmem 
  have hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ (s : Set ι), K i :=
    by
    refine' Subgroup.noncommProd_mem _ _ _
    intro x hx
    have : K x ≤ ⨆ i ∈ (s : Set ι), K i := le_iSup₂ (f := fun i _ => K i) x hx
    exact this (hmem.2 x hx)
  intro heq1
  rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ hnmem] at heq1 
  have hnmem' : i ∉ (s : Set ι) := by simpa
  obtain ⟨heq1i : f i = 1, heq1S : s.noncommProd f _ = 1⟩ :=
    Subgroup.disjoint_iff_mul_eq_one.mp (hind.disjoint_biSup hnmem') hmem.1 hmem_bsupr heq1
  intro i h
  simp only [Finset.mem_insert] at h 
  rcases h with (rfl | h)
  · exact heq1i
  · refine' ih hcomm hmem.2 heq1S _ h
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
f : ι → G
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem : ∀ (x : ι), x ∈ s → f x ∈ K x
heq1 : Finset.noncommProd s f comm = 1
⊢ ∀ (i : ι), i ∈ s → f i = 1
[PROOFSTEP]
revert heq1
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
f : ι → G
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem : ∀ (x : ι), x ∈ s → f x ∈ K x
⊢ Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
[PROOFSTEP]
induction' s using Finset.induction_on with i s hnmem ih
[GOAL]
case empty
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s → f x ∈ K x
comm : Set.Pairwise ↑∅ fun a b => Commute (f a) (f b)
hmem : ∀ (x : ι), x ∈ ∅ → f x ∈ K x
⊢ Finset.noncommProd ∅ f comm = 1 → ∀ (i : ι), i ∈ ∅ → f i = 1
[PROOFSTEP]
simp
[GOAL]
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hmem : ∀ (x : ι), x ∈ insert i s → f x ∈ K x
⊢ Finset.noncommProd (insert i s) f comm = 1 → ∀ (i_1 : ι), i_1 ∈ insert i s → f i_1 = 1
[PROOFSTEP]
have hcomm := comm.mono (Finset.coe_subset.2 <| Finset.subset_insert _ _)
[GOAL]
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hmem : ∀ (x : ι), x ∈ insert i s → f x ∈ K x
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
⊢ Finset.noncommProd (insert i s) f comm = 1 → ∀ (i_1 : ι), i_1 ∈ insert i s → f i_1 = 1
[PROOFSTEP]
simp only [Finset.forall_mem_insert] at hmem 
[GOAL]
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
⊢ Finset.noncommProd (insert i s) f comm = 1 → ∀ (i_1 : ι), i_1 ∈ insert i s → f i_1 = 1
[PROOFSTEP]
have hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ (s : Set ι), K i :=
  by
  refine' Subgroup.noncommProd_mem _ _ _
  intro x hx
  have : K x ≤ ⨆ i ∈ (s : Set ι), K i := le_iSup₂ (f := fun i _ => K i) x hx
  exact this (hmem.2 x hx)
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
⊢ Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
[PROOFSTEP]
refine' Subgroup.noncommProd_mem _ _ _
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
⊢ ∀ (c : ι), c ∈ s → f c ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
[PROOFSTEP]
intro x hx
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
x : ι
hx : x ∈ s
⊢ f x ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
[PROOFSTEP]
have : K x ≤ ⨆ i ∈ (s : Set ι), K i := le_iSup₂ (f := fun i _ => K i) x hx
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
x : ι
hx : x ∈ s
this : K x ≤ ⨆ (i : ι) (_ : i ∈ ↑s), K i
⊢ f x ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
[PROOFSTEP]
exact this (hmem.2 x hx)
[GOAL]
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
⊢ Finset.noncommProd (insert i s) f comm = 1 → ∀ (i_1 : ι), i_1 ∈ insert i s → f i_1 = 1
[PROOFSTEP]
intro heq1
[GOAL]
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
heq1 : Finset.noncommProd (insert i s) f comm = 1
⊢ ∀ (i_1 : ι), i_1 ∈ insert i s → f i_1 = 1
[PROOFSTEP]
rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ hnmem] at heq1 
[GOAL]
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
heq1 : f i * Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) = 1
⊢ ∀ (i_1 : ι), i_1 ∈ insert i s → f i_1 = 1
[PROOFSTEP]
have hnmem' : i ∉ (s : Set ι) := by simpa
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
heq1 : f i * Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) = 1
⊢ ¬i ∈ ↑s
[PROOFSTEP]
simpa
[GOAL]
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
heq1 : f i * Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) = 1
hnmem' : ¬i ∈ ↑s
⊢ ∀ (i_1 : ι), i_1 ∈ insert i s → f i_1 = 1
[PROOFSTEP]
obtain ⟨heq1i : f i = 1, heq1S : s.noncommProd f _ = 1⟩ :=
  Subgroup.disjoint_iff_mul_eq_one.mp (hind.disjoint_biSup hnmem') hmem.1 hmem_bsupr heq1
[GOAL]
case insert.intro
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i : ι
s : Finset ι
hnmem : ¬i ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
heq1 : f i * Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) = 1
hnmem' : ¬i ∈ ↑s
heq1i : f i = 1
heq1S : Finset.noncommProd s f hcomm = 1
⊢ ∀ (i_1 : ι), i_1 ∈ insert i s → f i_1 = 1
[PROOFSTEP]
intro i h
[GOAL]
case insert.intro
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i✝ : ι
s : Finset ι
hnmem : ¬i✝ ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i✝ s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i✝ ∈ K i✝ ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
heq1 : f i✝ * Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) = 1
hnmem' : ¬i✝ ∈ ↑s
heq1i : f i✝ = 1
heq1S : Finset.noncommProd s f hcomm = 1
i : ι
h : i ∈ insert i✝ s
⊢ f i = 1
[PROOFSTEP]
simp only [Finset.mem_insert] at h 
[GOAL]
case insert.intro
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i✝ : ι
s : Finset ι
hnmem : ¬i✝ ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i✝ s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i✝ ∈ K i✝ ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
heq1 : f i✝ * Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) = 1
hnmem' : ¬i✝ ∈ ↑s
heq1i : f i✝ = 1
heq1S : Finset.noncommProd s f hcomm = 1
i : ι
h : i = i✝ ∨ i ∈ s
⊢ f i = 1
[PROOFSTEP]
rcases h with (rfl | h)
[GOAL]
case insert.intro.inl
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
s : Finset ι
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
heq1S : Finset.noncommProd s f hcomm = 1
i : ι
hnmem : ¬i ∈ s
comm : Set.Pairwise ↑(insert i s) fun a b => Commute (f a) (f b)
hmem : f i ∈ K i ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
heq1 : f i * Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) = 1
hnmem' : ¬i ∈ ↑s
heq1i : f i = 1
⊢ f i = 1
[PROOFSTEP]
exact heq1i
[GOAL]
case insert.intro.inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
s✝ : Finset ι
f : ι → G
comm✝ : Set.Pairwise ↑s✝ fun a b => Commute (f a) (f b)
K : ι → Subgroup G
hind : CompleteLattice.Independent K
hmem✝ : ∀ (x : ι), x ∈ s✝ → f x ∈ K x
i✝ : ι
s : Finset ι
hnmem : ¬i✝ ∈ s
ih :
  ∀ (comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)),
    (∀ (x : ι), x ∈ s → f x ∈ K x) → Finset.noncommProd s f comm = 1 → ∀ (i : ι), i ∈ s → f i = 1
comm : Set.Pairwise ↑(insert i✝ s) fun a b => Commute (f a) (f b)
hcomm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
hmem : f i✝ ∈ K i✝ ∧ ∀ (x : ι), x ∈ s → f x ∈ K x
hmem_bsupr : Finset.noncommProd s f hcomm ∈ ⨆ (i : ι) (_ : i ∈ ↑s), K i
heq1 : f i✝ * Finset.noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) = 1
hnmem' : ¬i✝ ∈ ↑s
heq1i : f i✝ = 1
heq1S : Finset.noncommProd s f hcomm = 1
i : ι
h : i ∈ s
⊢ f i = 1
[PROOFSTEP]
refine' ih hcomm hmem.2 heq1S _ h
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ (fun f =>
        Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (f i))
          (_ :
            ∀ (i : ι), i ∈ ↑Finset.univ → ∀ (j : ι), j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (f i)) (↑(ϕ j) (f j))))
      1 =
    1
[PROOFSTEP]
apply (Finset.noncommProd_eq_pow_card _ _ _ _ _).trans (one_pow _)
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ ∀ (x : ι), x ∈ Finset.univ → ↑(ϕ x) (OfNat.ofNat 1 x) = 1
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ f g : (i : ι) → N i
⊢ OneHom.toFun
      {
        toFun := fun f =>
          Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (f i))
            (_ :
              ∀ (i : ι),
                i ∈ ↑Finset.univ → ∀ (j : ι), j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (f i)) (↑(ϕ j) (f j))),
        map_one' :=
          (_ :
            Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (OfNat.ofNat 1 i))
                (_ :
                  ∀ (i : ι),
                    i ∈ ↑Finset.univ →
                      ∀ (j : ι),
                        j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (OfNat.ofNat 1 i)) (↑(ϕ j) (OfNat.ofNat 1 j))) =
              1) }
      (f * g) =
    OneHom.toFun
        {
          toFun := fun f =>
            Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (f i))
              (_ :
                ∀ (i : ι),
                  i ∈ ↑Finset.univ → ∀ (j : ι), j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (f i)) (↑(ϕ j) (f j))),
          map_one' :=
            (_ :
              Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (OfNat.ofNat 1 i))
                  (_ :
                    ∀ (i : ι),
                      i ∈ ↑Finset.univ →
                        ∀ (j : ι),
                          j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (OfNat.ofNat 1 i)) (↑(ϕ j) (OfNat.ofNat 1 j))) =
                1) }
        f *
      OneHom.toFun
        {
          toFun := fun f =>
            Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (f i))
              (_ :
                ∀ (i : ι),
                  i ∈ ↑Finset.univ → ∀ (j : ι), j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (f i)) (↑(ϕ j) (f j))),
          map_one' :=
            (_ :
              Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (OfNat.ofNat 1 i))
                  (_ :
                    ∀ (i : ι),
                      i ∈ ↑Finset.univ →
                        ∀ (j : ι),
                          j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (OfNat.ofNat 1 i)) (↑(ϕ j) (OfNat.ofNat 1 j))) =
                1) }
        g
[PROOFSTEP]
classical
simp only
convert @Finset.noncommProd_mul_distrib _ _ _ _ (fun i => ϕ i (f i)) (fun i => ϕ i (g i)) _ _ _
· exact map_mul _ _ _
· rintro i - j - h
  exact hcomm h _ _
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ f g : (i : ι) → N i
⊢ OneHom.toFun
      {
        toFun := fun f =>
          Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (f i))
            (_ :
              ∀ (i : ι),
                i ∈ ↑Finset.univ → ∀ (j : ι), j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (f i)) (↑(ϕ j) (f j))),
        map_one' :=
          (_ :
            Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (OfNat.ofNat 1 i))
                (_ :
                  ∀ (i : ι),
                    i ∈ ↑Finset.univ →
                      ∀ (j : ι),
                        j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (OfNat.ofNat 1 i)) (↑(ϕ j) (OfNat.ofNat 1 j))) =
              1) }
      (f * g) =
    OneHom.toFun
        {
          toFun := fun f =>
            Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (f i))
              (_ :
                ∀ (i : ι),
                  i ∈ ↑Finset.univ → ∀ (j : ι), j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (f i)) (↑(ϕ j) (f j))),
          map_one' :=
            (_ :
              Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (OfNat.ofNat 1 i))
                  (_ :
                    ∀ (i : ι),
                      i ∈ ↑Finset.univ →
                        ∀ (j : ι),
                          j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (OfNat.ofNat 1 i)) (↑(ϕ j) (OfNat.ofNat 1 j))) =
                1) }
        f *
      OneHom.toFun
        {
          toFun := fun f =>
            Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (f i))
              (_ :
                ∀ (i : ι),
                  i ∈ ↑Finset.univ → ∀ (j : ι), j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (f i)) (↑(ϕ j) (f j))),
          map_one' :=
            (_ :
              Finset.noncommProd Finset.univ (fun i => ↑(ϕ i) (OfNat.ofNat 1 i))
                  (_ :
                    ∀ (i : ι),
                      i ∈ ↑Finset.univ →
                        ∀ (j : ι),
                          j ∈ ↑Finset.univ → i ≠ j → Commute (↑(ϕ i) (OfNat.ofNat 1 i)) (↑(ϕ j) (OfNat.ofNat 1 j))) =
                1) }
        g
[PROOFSTEP]
simp only
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ f g : (i : ι) → N i
⊢ Finset.noncommProd Finset.univ (fun x => ↑(ϕ x) ((f * g) x))
      (_ :
        ∀ (x : ι),
          x ∈ ↑Finset.univ →
            ∀ (y : ι), y ∈ ↑Finset.univ → x ≠ y → (fun a b => Commute (↑(ϕ a) ((f * g) a)) (↑(ϕ b) ((f * g) b))) x y) =
    Finset.noncommProd Finset.univ (fun x => ↑(ϕ x) (f x))
        (_ :
          ∀ (x : ι),
            x ∈ ↑Finset.univ →
              ∀ (y : ι), y ∈ ↑Finset.univ → x ≠ y → (fun a b => Commute (↑(ϕ a) (f a)) (↑(ϕ b) (f b))) x y) *
      Finset.noncommProd Finset.univ (fun x => ↑(ϕ x) (g x))
        (_ :
          ∀ (x : ι),
            x ∈ ↑Finset.univ →
              ∀ (y : ι), y ∈ ↑Finset.univ → x ≠ y → (fun a b => Commute (↑(ϕ a) (g a)) (↑(ϕ b) (g b))) x y)
[PROOFSTEP]
convert @Finset.noncommProd_mul_distrib _ _ _ _ (fun i => ϕ i (f i)) (fun i => ϕ i (g i)) _ _ _
[GOAL]
case h.e'_2.h₂
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ f g : (i : ι) → N i
x✝ : ι
a✝ : x✝ ∈ Finset.univ
⊢ ↑(ϕ x✝) ((f * g) x✝) = ((fun i => ↑(ϕ i) (f i)) * fun i => ↑(ϕ i) (g i)) x✝
[PROOFSTEP]
exact map_mul _ _ _
[GOAL]
case convert_4
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ f g : (i : ι) → N i
⊢ Set.Pairwise ↑Finset.univ fun x y => Commute ((fun i => ↑(ϕ i) (g i)) x) ((fun i => ↑(ϕ i) (f i)) y)
[PROOFSTEP]
rintro i - j - h
[GOAL]
case convert_4
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ f g : (i : ι) → N i
i j : ι
h : i ≠ j
⊢ Commute ((fun i => ↑(ϕ i) (g i)) i) ((fun i => ↑(ϕ i) (f i)) j)
[PROOFSTEP]
exact hcomm h _ _
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ ↑(noncommPiCoprod ϕ hcomm) (Pi.mulSingle i y) = ↑(ϕ i) y
[PROOFSTEP]
change Finset.univ.noncommProd (fun j => ϕ j (Pi.mulSingle i y j)) (fun _ _ _ _ h => hcomm h _ _) = ϕ i y
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ Finset.noncommProd Finset.univ (fun j => ↑(ϕ j) (Pi.mulSingle i y j))
      (_ :
        ∀ (x : ι),
          x ∈ ↑Finset.univ →
            ∀ (x_2 : ι),
              x_2 ∈ ↑Finset.univ → x ≠ x_2 → Commute (↑(ϕ x) (Pi.mulSingle i y x)) (↑(ϕ x_2) (Pi.mulSingle i y x_2))) =
    ↑(ϕ i) y
[PROOFSTEP]
simp (config := { singlePass := true }) only [← Finset.insert_erase (Finset.mem_univ i)]
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ Finset.noncommProd (insert i (Finset.erase Finset.univ i)) (fun x => ↑(ϕ x) (Pi.mulSingle i y x))
      (_ :
        ∀ (x : ι),
          x ∈ ↑(insert i (Finset.erase Finset.univ i)) →
            ∀ (y_1 : ι),
              y_1 ∈ ↑(insert i (Finset.erase Finset.univ i)) →
                x ≠ y_1 → (fun a b => Commute (↑(ϕ a) (Pi.mulSingle i y a)) (↑(ϕ b) (Pi.mulSingle i y b))) x y_1) =
    ↑(ϕ i) y
[PROOFSTEP]
rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ (Finset.not_mem_erase i _)]
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ ↑(ϕ i) (Pi.mulSingle i y i) *
      Finset.noncommProd (Finset.erase Finset.univ i) (fun x => ↑(ϕ x) (Pi.mulSingle i y x))
        (_ :
          Set.Pairwise ↑(Finset.erase Finset.univ i) fun a b =>
            Commute (↑(ϕ a) (Pi.mulSingle i y a)) (↑(ϕ b) (Pi.mulSingle i y b))) =
    ↑(ϕ i) y
[PROOFSTEP]
rw [Pi.mulSingle_eq_same]
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ ↑(ϕ i) y *
      Finset.noncommProd (Finset.erase Finset.univ i) (fun x => ↑(ϕ x) (Pi.mulSingle i y x))
        (_ :
          Set.Pairwise ↑(Finset.erase Finset.univ i) fun a b =>
            Commute (↑(ϕ a) (Pi.mulSingle i y a)) (↑(ϕ b) (Pi.mulSingle i y b))) =
    ↑(ϕ i) y
[PROOFSTEP]
rw [Finset.noncommProd_eq_pow_card]
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ ↑(ϕ i) y * ?m ^ Finset.card (Finset.erase Finset.univ i) = ↑(ϕ i) y
[PROOFSTEP]
rw [one_pow]
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ ↑(ϕ i) y * 1 = ↑(ϕ i) y
[PROOFSTEP]
exact mul_one _
[GOAL]
case h
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ ∀ (x : ι), x ∈ Finset.erase Finset.univ i → ↑(ϕ x) (Pi.mulSingle i y x) = 1
[PROOFSTEP]
intro j hj
[GOAL]
case h
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
j : ι
hj : j ∈ Finset.erase Finset.univ i
⊢ ↑(ϕ j) (Pi.mulSingle i y j) = 1
[PROOFSTEP]
simp only [Finset.mem_erase] at hj 
[GOAL]
case h
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
j : ι
hj : j ≠ i ∧ j ∈ Finset.univ
⊢ ↑(ϕ j) (Pi.mulSingle i y j) = 1
[PROOFSTEP]
simp [hj]
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ✝ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ✝ i) x) (↑(ϕ✝ j) y)
f g : (i : ι) → N i
ϕ : { ϕ // Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y) }
⊢ (fun f =>
        { val := fun i => comp f (single N i),
          property :=
            (_ : ∀ (i j : ι), i ≠ j → ∀ (x : N i) (y : N j), Commute (↑f (Pi.mulSingle i x)) (↑f (Pi.mulSingle j y))) })
      ((fun ϕ => noncommPiCoprod ↑ϕ (_ : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(↑ϕ i) x) (↑(↑ϕ j) y)))
        ϕ) =
    ϕ
[PROOFSTEP]
ext
[GOAL]
case a.h.h
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ✝ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ✝ i) x) (↑(ϕ✝ j) y)
f g : (i : ι) → N i
ϕ : { ϕ // Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y) }
x✝¹ : ι
x✝ : N x✝¹
⊢ ↑(↑((fun f =>
                { val := fun i => comp f (single N i),
                  property :=
                    (_ :
                      ∀ (i j : ι),
                        i ≠ j → ∀ (x : N i) (y : N j), Commute (↑f (Pi.mulSingle i x)) (↑f (Pi.mulSingle j y))) })
              ((fun ϕ =>
                  noncommPiCoprod ↑ϕ (_ : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(↑ϕ i) x) (↑(↑ϕ j) y)))
                ϕ))
          x✝¹)
      x✝ =
    ↑(↑ϕ x✝¹) x✝
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → N i
f : ((i : ι) → N i) →* M
i : ι
x : N i
⊢ ↑((fun ϕ => noncommPiCoprod ↑ϕ (_ : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(↑ϕ i) x) (↑(↑ϕ j) y)))
          ((fun f =>
              { val := fun i => comp f (single N i),
                property :=
                  (_ :
                    ∀ (i j : ι),
                      i ≠ j → ∀ (x : N i) (y : N j), Commute (↑f (Pi.mulSingle i x)) (↑f (Pi.mulSingle j y))) })
            f))
      (Pi.mulSingle i x) =
    ↑f (Pi.mulSingle i x)
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ mrange (noncommPiCoprod ϕ hcomm) = ⨆ (i : ι), mrange (ϕ i)
[PROOFSTEP]
classical
apply le_antisymm
· rintro x ⟨f, rfl⟩
  refine Submonoid.noncommProd_mem _ _ _ (fun _ _ _ _ h => hcomm h _ _) (fun i _ => ?_)
  apply Submonoid.mem_sSup_of_mem
  · use i
  simp
· refine' iSup_le _
  rintro i x ⟨y, rfl⟩
  refine' ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩
[GOAL]
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ mrange (noncommPiCoprod ϕ hcomm) = ⨆ (i : ι), mrange (ϕ i)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ mrange (noncommPiCoprod ϕ hcomm) ≤ ⨆ (i : ι), mrange (ϕ i)
[PROOFSTEP]
rintro x ⟨f, rfl⟩
[GOAL]
case a.intro
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → N i
⊢ ↑(noncommPiCoprod ϕ hcomm) f ∈ ⨆ (i : ι), mrange (ϕ i)
[PROOFSTEP]
refine Submonoid.noncommProd_mem _ _ _ (fun _ _ _ _ h => hcomm h _ _) (fun i _ => ?_)
[GOAL]
case a.intro
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → N i
i : ι
x✝ : i ∈ Finset.univ
⊢ ↑(ϕ i) (f i) ∈ ⨆ (i : ι), mrange (ϕ i)
[PROOFSTEP]
apply Submonoid.mem_sSup_of_mem
[GOAL]
case a.intro.hs
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → N i
i : ι
x✝ : i ∈ Finset.univ
⊢ ?a.intro.s✝ ∈ Set.range fun i => mrange (ϕ i)
[PROOFSTEP]
use i
[GOAL]
case a.intro.a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → N i
i : ι
x✝ : i ∈ Finset.univ
⊢ ↑(ϕ i) (f i) ∈ (fun i => mrange (ϕ i)) i
[PROOFSTEP]
simp
[GOAL]
case a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ ⨆ (i : ι), mrange (ϕ i) ≤ mrange (noncommPiCoprod ϕ hcomm)
[PROOFSTEP]
refine' iSup_le _
[GOAL]
case a
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
⊢ ∀ (i : ι), mrange (ϕ i) ≤ mrange (noncommPiCoprod ϕ hcomm)
[PROOFSTEP]
rintro i x ⟨y, rfl⟩
[GOAL]
case a.intro
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
hdec : DecidableEq ι
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → N i
i : ι
y : N i
⊢ ↑(ϕ i) y ∈ mrange (noncommPiCoprod ϕ hcomm)
[PROOFSTEP]
refine' ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
⊢ range (noncommPiCoprod ϕ hcomm) = ⨆ (i : ι), range (ϕ i)
[PROOFSTEP]
classical
apply le_antisymm
· rintro x ⟨f, rfl⟩
  refine Subgroup.noncommProd_mem _ (fun _ _ _ _ h => hcomm _ _ h _ _) ?_
  intro i _hi
  apply Subgroup.mem_sSup_of_mem
  · use i
  simp
· refine' iSup_le _
  rintro i x ⟨y, rfl⟩
  refine' ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
⊢ range (noncommPiCoprod ϕ hcomm) = ⨆ (i : ι), range (ϕ i)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
⊢ range (noncommPiCoprod ϕ hcomm) ≤ ⨆ (i : ι), range (ϕ i)
[PROOFSTEP]
rintro x ⟨f, rfl⟩
[GOAL]
case a.intro
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → H i
⊢ ↑(noncommPiCoprod ϕ hcomm) f ∈ ⨆ (i : ι), range (ϕ i)
[PROOFSTEP]
refine Subgroup.noncommProd_mem _ (fun _ _ _ _ h => hcomm _ _ h _ _) ?_
[GOAL]
case a.intro
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → H i
⊢ ∀ (c : ι), c ∈ Finset.univ → ↑(ϕ c) (f c) ∈ ⨆ (i : ι), range (ϕ i)
[PROOFSTEP]
intro i _hi
[GOAL]
case a.intro
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → H i
i : ι
_hi : i ∈ Finset.univ
⊢ ↑(ϕ i) (f i) ∈ ⨆ (i : ι), range (ϕ i)
[PROOFSTEP]
apply Subgroup.mem_sSup_of_mem
[GOAL]
case a.intro.hs
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → H i
i : ι
_hi : i ∈ Finset.univ
⊢ ?a.intro.s✝ ∈ Set.range fun i => range (ϕ i)
[PROOFSTEP]
use i
[GOAL]
case a.intro.a
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g f : (i : ι) → H i
i : ι
_hi : i ∈ Finset.univ
⊢ ↑(ϕ i) (f i) ∈ (fun i => range (ϕ i)) i
[PROOFSTEP]
simp
[GOAL]
case a
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
⊢ ⨆ (i : ι), range (ϕ i) ≤ range (noncommPiCoprod ϕ hcomm)
[PROOFSTEP]
refine' iSup_le _
[GOAL]
case a
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
⊢ ∀ (i : ι), range (ϕ i) ≤ range (noncommPiCoprod ϕ hcomm)
[PROOFSTEP]
rintro i x ⟨y, rfl⟩
[GOAL]
case a.intro
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
i : ι
y : H i
⊢ ↑(ϕ i) y ∈ range (noncommPiCoprod ϕ hcomm)
[PROOFSTEP]
refine' ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩
[GOAL]
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
⊢ Function.Injective ↑(noncommPiCoprod ϕ hcomm)
[PROOFSTEP]
classical
apply (MonoidHom.ker_eq_bot_iff _).mp
apply eq_bot_iff.mpr
intro f heq1
have : ∀ i, i ∈ Finset.univ → ϕ i (f i) = 1 :=
  Subgroup.eq_one_of_noncommProd_eq_one_of_independent _ _ (fun _ _ _ _ h => hcomm _ _ h _ _) _ hind (by simp) heq1
ext i
apply hinj
simp [this i (Finset.mem_univ i)]
[GOAL]
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
⊢ Function.Injective ↑(noncommPiCoprod ϕ hcomm)
[PROOFSTEP]
apply (MonoidHom.ker_eq_bot_iff _).mp
[GOAL]
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
⊢ ker (noncommPiCoprod ϕ hcomm) = ⊥
[PROOFSTEP]
apply eq_bot_iff.mpr
[GOAL]
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
⊢ ker (noncommPiCoprod ϕ hcomm) ≤ ⊥
[PROOFSTEP]
intro f heq1
[GOAL]
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
⊢ f ∈ ⊥
[PROOFSTEP]
have : ∀ i, i ∈ Finset.univ → ϕ i (f i) = 1 :=
  Subgroup.eq_one_of_noncommProd_eq_one_of_independent _ _ (fun _ _ _ _ h => hcomm _ _ h _ _) _ hind (by simp) heq1
[GOAL]
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
⊢ ∀ (x : ι), x ∈ Finset.univ → ↑(ϕ x) (f x) ∈ range (ϕ x)
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
this : ∀ (i : ι), i ∈ Finset.univ → ↑(ϕ i) (f i) = 1
⊢ f ∈ ⊥
[PROOFSTEP]
ext i
[GOAL]
case h
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
this : ∀ (i : ι), i ∈ Finset.univ → ↑(ϕ i) (f i) = 1
i : ι
⊢ f i = OfNat.ofNat 1 i
[PROOFSTEP]
apply hinj
[GOAL]
case h.a
G : Type u_1
inst✝¹ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝ : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
hind : CompleteLattice.Independent fun i => range (ϕ i)
hinj : ∀ (i : ι), Function.Injective ↑(ϕ i)
f : (i : ι) → H i
heq1 : f ∈ ker (noncommPiCoprod ϕ hcomm)
this : ∀ (i : ι), i ∈ Finset.univ → ↑(ϕ i) (f i) = 1
i : ι
⊢ ↑(ϕ i) (f i) = ↑(ϕ i) (OfNat.ofNat 1 i)
[PROOFSTEP]
simp [this i (Finset.mem_univ i)]
[GOAL]
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
⊢ CompleteLattice.Independent fun i => range (ϕ i)
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
⊢ CompleteLattice.Independent fun i => range (ϕ i)
[PROOFSTEP]
classical
rintro i
rw [disjoint_iff_inf_le]
rintro f ⟨hxi, hxp⟩
dsimp at hxi hxp 
rw [iSup_subtype', ← noncommPiCoprod_range] at hxp 
rotate_left
· intro _ _ hj
  apply hcomm
  exact hj ∘ Subtype.ext
cases' hxp with g hgf
cases' hxi with g' hg'f
have hxi : orderOf f ∣ Fintype.card (H i) := by
  rw [← hg'f]
  exact (orderOf_map_dvd _ _).trans orderOf_dvd_card_univ
have hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H j) :=
  by
  rw [← hgf, ← Fintype.card_pi]
  exact (orderOf_map_dvd _ _).trans orderOf_dvd_card_univ
change f = 1
rw [← pow_one f, ← orderOf_dvd_iff_pow_eq_one]
  -- porting note: ouch, had to replace an ugly `convert`
obtain ⟨c, hc⟩ := Nat.dvd_gcd hxp hxi
use c
rw [← hc]
symm
rw [← Nat.coprime_iff_gcd_eq_one]
apply Nat.coprime_prod_left
intro j _
apply hcoprime
exact j.2
[GOAL]
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
⊢ CompleteLattice.Independent fun i => range (ϕ i)
[PROOFSTEP]
rintro i
[GOAL]
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
⊢ Disjoint ((fun i => range (ϕ i)) i) (⨆ (j : ι) (_ : j ≠ i), (fun i => range (ϕ i)) j)
[PROOFSTEP]
rw [disjoint_iff_inf_le]
[GOAL]
case intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
⊢ (fun i => range (ϕ i)) i ⊓ ⨆ (j : ι) (_ : j ≠ i), (fun i => range (ϕ i)) j ≤ ⊥
[PROOFSTEP]
rintro f ⟨hxi, hxp⟩
[GOAL]
case intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ ↑((fun i => range (ϕ i)) i).toSubmonoid
hxp : f ∈ ↑(⨆ (j : ι) (_ : j ≠ i), (fun i => range (ϕ i)) j).toSubmonoid
⊢ f ∈ ⊥
[PROOFSTEP]
dsimp at hxi hxp 
[GOAL]
case intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (j : ι) (_ : ¬j = i), range (ϕ j))
⊢ f ∈ ⊥
[PROOFSTEP]
rw [iSup_subtype', ← noncommPiCoprod_range] at hxp 
[GOAL]
case intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
hxp : f ∈ ↑(range (noncommPiCoprod (fun x => ϕ ↑x) ?intro.intro.hcomm))
⊢ f ∈ ⊥
case intro.intro.hcomm
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
⊢ ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)
[PROOFSTEP]
rotate_left
[GOAL]
case intro.intro.hcomm
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
⊢ ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)
[PROOFSTEP]
intro _ _ hj
[GOAL]
case intro.intro.hcomm
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
i✝ j✝ : { j // ¬j = i }
hj : i✝ ≠ j✝
⊢ ∀ (x : H ↑i✝) (y : H ↑j✝), Commute (↑(ϕ ↑i✝) x) (↑(ϕ ↑j✝) y)
[PROOFSTEP]
apply hcomm
[GOAL]
case intro.intro.hcomm.a
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
i✝ j✝ : { j // ¬j = i }
hj : i✝ ≠ j✝
⊢ ↑i✝ ≠ ↑j✝
[PROOFSTEP]
exact hj ∘ Subtype.ext
[GOAL]
case intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
hxp :
  f ∈
    ↑(range
        (noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y))))
⊢ f ∈ ⊥
[PROOFSTEP]
cases' hxp with g hgf
[GOAL]
case intro.intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxi : f ∈ Set.range ↑(ϕ i)
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
⊢ f ∈ ⊥
[PROOFSTEP]
cases' hxi with g' hg'f
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
⊢ f ∈ ⊥
[PROOFSTEP]
have hxi : orderOf f ∣ Fintype.card (H i) := by
  rw [← hg'f]
  exact (orderOf_map_dvd _ _).trans orderOf_dvd_card_univ
[GOAL]
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
⊢ orderOf f ∣ Fintype.card (H i)
[PROOFSTEP]
rw [← hg'f]
[GOAL]
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
⊢ orderOf (↑(ϕ i) g') ∣ Fintype.card (H i)
[PROOFSTEP]
exact (orderOf_map_dvd _ _).trans orderOf_dvd_card_univ
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
⊢ f ∈ ⊥
[PROOFSTEP]
have hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H j) :=
  by
  rw [← hgf, ← Fintype.card_pi]
  exact (orderOf_map_dvd _ _).trans orderOf_dvd_card_univ
[GOAL]
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
⊢ orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
[PROOFSTEP]
rw [← hgf, ← Fintype.card_pi]
[GOAL]
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
⊢ orderOf
      (↑(noncommPiCoprod (fun x => ϕ ↑x)
            (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
        g) ∣
    Fintype.card ((a : { j // j ≠ i }) → H ↑a)
[PROOFSTEP]
exact (orderOf_map_dvd _ _).trans orderOf_dvd_card_univ
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
⊢ f ∈ ⊥
[PROOFSTEP]
change f = 1
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
⊢ f = 1
[PROOFSTEP]
rw [← pow_one f, ← orderOf_dvd_iff_pow_eq_one]
  -- porting note: ouch, had to replace an ugly `convert`
[GOAL]
case intro.intro.intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
⊢ orderOf f ∣ 1
[PROOFSTEP]
obtain ⟨c, hc⟩ := Nat.dvd_gcd hxp hxi
[GOAL]
case intro.intro.intro.intro.intro
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ orderOf f ∣ 1
[PROOFSTEP]
use c
[GOAL]
case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ 1 = orderOf f * c
[PROOFSTEP]
rw [← hc]
[GOAL]
case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ 1 = Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i))
[PROOFSTEP]
symm
[GOAL]
case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = 1
[PROOFSTEP]
rw [← Nat.coprime_iff_gcd_eq_one]
[GOAL]
case h
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ Nat.coprime (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i))
[PROOFSTEP]
apply Nat.coprime_prod_left
[GOAL]
case h.a
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
⊢ ∀ (i_1 : { j // j ≠ i }), i_1 ∈ Finset.univ → Nat.coprime (Fintype.card (H ↑i_1)) (Fintype.card (H i))
[PROOFSTEP]
intro j _
[GOAL]
case h.a
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
j : { j // j ≠ i }
a✝ : j ∈ Finset.univ
⊢ Nat.coprime (Fintype.card (H ↑j)) (Fintype.card (H i))
[PROOFSTEP]
apply hcoprime
[GOAL]
case h.a.a
G : Type u_1
inst✝³ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Type u_3
inst✝² : (i : ι) → Group (H i)
ϕ : (i : ι) → H i →* G
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x : H i) (y : H j), Commute (↑(ϕ i) x) (↑(ϕ j) y)
f✝ g✝ : (i : ι) → H i
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype (H i)
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card (H i)) (Fintype.card (H j))
val✝ : Fintype ι
i : ι
f : G
hxp✝ : f ∈ ↑(⨆ (x : { j // ¬j = i }), range (ϕ ↑x))
g : (i_1 : { j // ¬j = i }) → H ↑i_1
hgf :
  ↑(noncommPiCoprod (fun x => ϕ ↑x)
          (_ : ∀ (i_1 j : { j // ¬j = i }), i_1 ≠ j → ∀ (x : H ↑i_1) (y : H ↑j), Commute (↑(ϕ ↑i_1) x) (↑(ϕ ↑j) y)))
      g =
    f
g' : H i
hg'f : ↑(ϕ i) g' = f
hxi : orderOf f ∣ Fintype.card (H i)
hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H ↑j)
c : ℕ
hc : Nat.gcd (∏ j : { j // j ≠ i }, Fintype.card (H ↑j)) (Fintype.card (H i)) = orderOf f * c
j : { j // j ≠ i }
a✝ : j ∈ Finset.univ
⊢ ↑j ≠ i
[PROOFSTEP]
exact j.2
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i j : ι
hne : i ≠ j
⊢ ∀ (x : { x // x ∈ H i }) (y : { x // x ∈ H j }), Commute (↑(Subgroup.subtype (H i)) x) (↑(Subgroup.subtype (H j)) y)
[PROOFSTEP]
rintro ⟨x, hx⟩ ⟨y, hy⟩
[GOAL]
case mk.mk
G : Type u_1
inst✝ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i j : ι
hne : i ≠ j
x : G
hx : x ∈ H i
y : G
hy : y ∈ H j
⊢ Commute (↑(Subgroup.subtype (H i)) { val := x, property := hx })
    (↑(Subgroup.subtype (H j)) { val := y, property := hy })
[PROOFSTEP]
exact hcomm i j hne x y hx hy
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i : ι
y : { x // x ∈ H i }
⊢ ↑(noncommPiCoprod hcomm) (Pi.mulSingle i y) = ↑y
[PROOFSTEP]
apply MonoidHom.noncommPiCoprod_mulSingle
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
⊢ MonoidHom.range (noncommPiCoprod hcomm) = ⨆ (i : ι), H i
[PROOFSTEP]
simp [noncommPiCoprod, MonoidHom.noncommPiCoprod_range]
[GOAL]
G : Type u_1
inst✝ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : CompleteLattice.Independent H
⊢ Function.Injective ↑(noncommPiCoprod hcomm)
[PROOFSTEP]
apply MonoidHom.injective_noncommPiCoprod_of_independent
[GOAL]
case hind
G : Type u_1
inst✝ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : CompleteLattice.Independent H
⊢ CompleteLattice.Independent fun i => MonoidHom.range (Subgroup.subtype ((fun i => H i) i))
[PROOFSTEP]
simpa using hind
[GOAL]
case hinj
G : Type u_1
inst✝ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : CompleteLattice.Independent H
⊢ ∀ (i : ι), Function.Injective ↑(Subgroup.subtype ((fun i => H i) i))
[PROOFSTEP]
intro i
[GOAL]
case hinj
G : Type u_1
inst✝ : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
hind : CompleteLattice.Independent H
i : ι
⊢ Function.Injective ↑(Subgroup.subtype ((fun i => H i) i))
[PROOFSTEP]
exact Subtype.coe_injective
[GOAL]
G : Type u_1
inst✝² : Group G
ι : Type u_2
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
inst✝¹ : Finite ι
inst✝ : (i : ι) → Fintype { x // x ∈ H i }
hcoprime : ∀ (i j : ι), i ≠ j → Nat.coprime (Fintype.card { x // x ∈ H i }) (Fintype.card { x // x ∈ H j })
⊢ CompleteLattice.Independent H
[PROOFSTEP]
simpa using
  MonoidHom.independent_range_of_coprime_order (fun i => (H i).subtype) (commute_subtype_of_commute hcomm) hcoprime
