-- Mathlib/GroupTheory/NoncommPiCoprod.lean
theorem eq_one_of_noncommProd_eq_one_of_iSupIndep {ι : Type*} (s : Finset ι) (f : ι → G) (comm)
    (K : ι → Subgroup G) (hind : iSupIndep K) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1) : ∀ i ∈ s, f i = 1

Proof state:
case insert.intro
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i✝ : ι
s : Finset ι
hnmem : i✝ ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
comm : (↑(insert i✝ s)).Pairwise (Function.onFun Commute f)
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem : f i✝ ∈ K i✝ ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ ↑s, K i
heq1 : f i✝ * s.noncommProd f ⋯ = 1
hnmem' : i✝ ∉ ↑s
heq1i : f i✝ = 1
heq1S : s.noncommProd f hcomm = 1
i : ι
h : i = i✝ ∨ i ∈ s
⊢ f i = 1

Tactic:
rcases h with (rfl | h)

Result:
case insert.intro.inl
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
s : Finset ι
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ ↑s, K i
heq1S : s.noncommProd f hcomm = 1
i : ι
hnmem : i ∉ s
comm : (↑(insert i s)).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
heq1 : f i * s.noncommProd f ⋯ = 1
hnmem' : i ∉ ↑s
heq1i : f i = 1
⊢ f i = 1

case insert.intro.inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i✝ : ι
s : Finset ι
hnmem : i✝ ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
comm : (↑(insert i✝ s)).Pairwise (Function.onFun Commute f)
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem : f i✝ ∈ K i✝ ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ ↑s, K i
heq1 : f i✝ * s.noncommProd f ⋯ = 1
hnmem' : i✝ ∉ ↑s
heq1i : f i✝ = 1
heq1S : s.noncommProd f hcomm = 1
i : ι
h : i ∈ s
⊢ f i = 1

Proof state:
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnmem : i ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
comm : (↑(insert i s)).Pairwise (Function.onFun Commute f)
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ ↑s, K i
⊢ (insert i s).noncommProd f comm = 1 → ∀ i_1 ∈ insert i s, f i_1 = 1

Tactic:
intro heq1

Result:
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnmem : i ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
comm : (↑(insert i s)).Pairwise (Function.onFun Commute f)
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ ↑s, K i
heq1 : (insert i s).noncommProd f comm = 1
⊢ ∀ i_1 ∈ insert i s, f i_1 = 1

Proof state:
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnmem : i ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
comm : (↑(insert i s)).Pairwise (Function.onFun Commute f)
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ ↑s, K i
heq1 : (insert i s).noncommProd f comm = 1
⊢ ∀ i_1 ∈ insert i s, f i_1 = 1

Tactic:
rw [Finset.noncommProd_insert_of_not_mem _ _ _ _ hnmem] at heq1

Result:
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnmem : i ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
comm : (↑(insert i s)).Pairwise (Function.onFun Commute f)
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ ↑s, K i
heq1 : f i * s.noncommProd f ⋯ = 1
⊢ ∀ i_1 ∈ insert i s, f i_1 = 1

Proof state:
case insert.intro.inl
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
s : Finset ι
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ ↑s, K i
heq1S : s.noncommProd f hcomm = 1
i : ι
hnmem : i ∉ s
comm : (↑(insert i s)).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
heq1 : f i * s.noncommProd f ⋯ = 1
hnmem' : i ∉ ↑s
heq1i : f i = 1
⊢ f i = 1

Tactic:
exact heq1i

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnmem : i ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
comm : (↑(insert i s)).Pairwise (Function.onFun Commute f)
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ ↑s, K i
heq1 : f i * s.noncommProd f ⋯ = 1
⊢ i ∉ ↑s

Tactic:
simpa

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
f : ι → G
comm : (↑s).Pairwise (Function.onFun Commute f)
K : ι → Subgroup G
hind : iSupIndep K
hmem : ∀ x ∈ s, f x ∈ K x
⊢ s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1

Tactic:
induction' s using Finset.induction_on with i s hnmem ih

Result:
case empty
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
comm : (↑∅).Pairwise (Function.onFun Commute f)
hmem : ∀ x ∈ ∅, f x ∈ K x
⊢ ∅.noncommProd f comm = 1 → ∀ i ∈ ∅, f i = 1

case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnmem : i ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
comm : (↑(insert i s)).Pairwise (Function.onFun Commute f)
hmem : ∀ x ∈ insert i s, f x ∈ K x
⊢ (insert i s).noncommProd f comm = 1 → ∀ i_1 ∈ insert i s, f i_1 = 1

Proof state:
case insert
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnmem : i ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
comm : (↑(insert i s)).Pairwise (Function.onFun Commute f)
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ ↑s, K i
heq1 : f i * s.noncommProd f ⋯ = 1
hnmem' : i ∉ ↑s
⊢ ∀ i_1 ∈ insert i s, f i_1 = 1

Tactic:
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

Result:
case insert.intro
G : Type u_1
inst✝ : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnmem : i ∉ s
ih :
  ∀ (comm : (↑s).Pairwise (Function.onFun Commute f)),
    (∀ x ∈ s, f x ∈ K x) → s.noncommProd f comm = 1 → ∀ i ∈ s, f i = 1
comm : (↑(insert i s)).Pairwise (Function.onFun Commute f)
hcomm : (↑s).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : s.noncommProd f hcomm ∈ ⨆ i ∈ ↑s, K i
heq1 : f i * s.noncommProd f ⋯ = 1
hnmem' : i ∉ ↑s
heq1i : f i = 1
heq1S : s.noncommProd f hcomm = 1
⊢ ∀ i_1 ∈ insert i s, f i_1 = 1