G : Type u_2
inst✝ : Group G
ι : Type u_1
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
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
revert heq1
case empty
G : Type u_2
inst✝ : Group G
ι : Type u_1
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

case insert
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
induction' s using Finset.induction_on with i s hnmem ih
no goals
case empty
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
simp
case insert
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
case insert
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
have hcomm := comm.mono (Finset.coe_subset.2 <| Finset.subset_insert _ _)
case insert
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
case insert
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
simp only [Finset.forall_mem_insert] at hmem
case insert
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
case insert
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
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)
case insert
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
case insert
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
intro heq1
case insert
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
case insert
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ hnmem] at heq1
case insert
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
case insert
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
have hnmem' : i ∉ (s : Set ι) := by simpa
case insert.intro
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
case insert
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
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
case insert.intro
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
case insert.intro
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
intro i h
case insert.intro
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
case insert.intro
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
simp only [Finset.mem_insert] at h
case insert.intro.inl
G : Type u_2
inst✝ : Group G
ι : Type u_1
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

case insert.intro.inr
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
case insert.intro
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
rcases h with (rfl | h)
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
refine' Subgroup.noncommProd_mem _ _ _
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
intro x hx
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
have : K x ≤ ⨆ i ∈ (s : Set ι), K i := le_iSup₂ (f := fun i _ => K i) x hx
no goals
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
exact this (hmem.2 x hx)
no goals
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
simpa
no goals
case insert.intro.inl
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
exact heq1i
no goals
case insert.intro.inr
G : Type u_2
inst✝ : Group G
ι : Type u_1
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
refine' ih hcomm hmem.2 heq1S _ h