awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.NoncommCoprod
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
a : M
⊢ Membership.mem.{u_6, u_6} (α := P) (γ := Subgroup P) ((f.noncommCoprod g comm).range (G := M × N))
    ((f : (a : M) → P) a : P)

Tactic:
exact ⟨(a, 1), by rw [noncommCoprod_apply, map_one, mul_one]⟩
-- Module: Mathlib.GroupTheory.NoncommCoprod
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
a : N
rw : HMul.hMul (α := P) (β := P) ((f : (a : M) → P) (1, a).1 : P) ((g : (a : N) → P) (1, a).2 : P) = (g : (a : N) → P) a
rw₁ : HMul.hMul (α := P) (β := P) (1 : P) ((g : (a : N) → P) (1, a).2 : P) = (g : (a : N) → P) a
rw₂ rw₃ : Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) (1, a).2 : P) ((g : (a : N) → P) a : P)
⊢ Eq.{u_6 + 1} (α := P) ((f.noncommCoprod g comm : (a : M × N) → P) (1, a) : P) ((g : (a : N) → P) a : P)

Tactic:
rw [noncommCoprod_apply, map_one, one_mul]

Premises used: MonoidHom.noncommCoprod_apply, map_one, one_mul
-- Module: Mathlib.GroupTheory.NoncommCoprod
Goal:
M : Type u_4
N : Type u_5
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute.{u_6} (S := P) ((f : (a : M) → P) m : P) ((g : (a : N) → P) n : P)
a : N
⊢ Membership.mem.{u_6, u_6} (α := P) (γ := Subgroup P) ((f.noncommCoprod g comm).range (G := M × N))
    ((g : (a : N) → P) a : P)

Tactic:
exact ⟨(1, a), by rw [noncommCoprod_apply, map_one, one_mul]⟩
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
f : ι → G
comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
K : ι → Subgroup G
hind : iSupIndep K
hmem : ∀ x ∈ s, f x ∈ K x
heq1 : s.noncommProd f comm = 1
revert : ∀ (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
⊢ ∀ i ∈ s, f i = 1

Tactic:
revert heq1
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
comm : (↑∅ : Set ι).Pairwise (Function.onFun Commute f)
hmem : ∀ (x : ι), Membership.mem (γ := Finset ι) ∅ x → f x ∈ K x
⊢ ∀ (heq1 : Finset.noncommProd ∅ f comm = 1) (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i = 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
comm : (↑(insert i s) : Set ι).Pairwise (Function.onFun Commute f)
hmem : ∀ x ∈ insert i s, f x ∈ K x
⊢ (↑s : Set ι).Pairwise (Function.onFun Commute f)

Tactic:
have hcomm := comm.mono (Finset.coe_subset.2 <| Finset.subset_insert _ _)
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
comm : (↑(insert i s) : Set ι).Pairwise (Function.onFun Commute f)
hmem : ∀ x ∈ insert i s, f x ∈ K x
hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
⊢ f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x

Tactic:
simp only [Finset.forall_mem_insert] at hmem

Premises used: Finset.forall_mem_insert
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
comm : (↑(insert i s) : Set ι).Pairwise (Function.onFun Commute f)
hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
⊢ Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (s.noncommProd f hcomm)

Tactic:
Subgroup.noncommProd_mem _ _ ?_

Premises used: Subgroup.noncommProd_mem
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
comm : (↑(insert i s) : Set ι).Pairwise (Function.onFun Commute f)
hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
refine : ∀ c ∈ s, Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (f c)
⊢ Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (s.noncommProd f hcomm)

Tactic:
refine Subgroup.noncommProd_mem _ _ ?_

Premises used: Subgroup.noncommProd_mem
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
comm : (↑(insert i s) : Set ι).Pairwise (Function.onFun Commute f)
hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
x : ι
hx : x ∈ s
⊢ K x ≤ ⨆ i ∈ (↑s : Set ι), K i

Tactic:
have : K x ≤ ⨆ i ∈ (s : Set ι), K i := le_iSup₂ (f := fun i _ => K i) x hx
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
comm : (↑(insert i s) : Set ι).Pairwise (Function.onFun Commute f)
hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
x : ι
hx : x ∈ s
this : K x ≤ ⨆ i ∈ (↑s : Set ι), K i
⊢ Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (f x)

Tactic:
this (hmem.2 x hx)

Premises used: And.right
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
comm : (↑(insert i s) : Set ι).Pairwise (Function.onFun Commute f)
hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
x : ι
hx : x ∈ s
this : K x ≤ ⨆ i ∈ (↑s : Set ι), K i
⊢ Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (f x)

Tactic:
exact this (hmem.2 x hx)

Premises used: And.right
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
comm : (↑(insert i s) : Set ι).Pairwise (Function.onFun Commute f)
hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
⊢ Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (s.noncommProd f hcomm)

Tactic:
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)
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
comm : (↑(insert i s) : Set ι).Pairwise (Function.onFun Commute f)
hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (s.noncommProd f hcomm)
heq1 : (insert i s).noncommProd f comm = 1
⊢ f i * s.noncommProd f ⋯ = 1

Tactic:
rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hnotMem] at heq1

Premises used: Finset.noncommProd_insert_of_notMem
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
comm : (↑(insert i s) : Set ι).Pairwise (Function.onFun Commute f)
hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (s.noncommProd f hcomm)
heq1 : f i * s.noncommProd f ⋯ = 1
⊢ i ∉ (↑s : Set ι)

Tactic:
simpa
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
comm : (↑(insert i s) : Set ι).Pairwise (Function.onFun Commute f)
hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (s.noncommProd f hcomm)
heq1 : f i * s.noncommProd f ⋯ = 1
⊢ i ∉ (↑s : Set ι)

Tactic:
have hnotMem' : i ∉ (s : Set ι) := by simpa
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
comm : (↑(insert i s) : Set ι).Pairwise (Function.onFun Commute f)
hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (s.noncommProd f hcomm)
heq1 : f i * s.noncommProd f ⋯ = 1
hnotMem' : i ∉ (↑s : Set ι)
⊢ f i = 1

Tactic:
obtain ⟨heq1i : f i = 1, heq1S : s.noncommProd f _ = 1⟩ :=
        Subgroup.disjoint_iff_mul_eq_one.mp (hind.disjoint_biSup hnotMem') hmem.1 hmem_bsupr heq1

Premises used: iSupIndep.disjoint_biSup, Finset.noncommProd, And.left, Iff.mp, Subgroup.disjoint_iff_mul_eq_one
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i : ι
s : Finset ι
hnotMem : i ∉ s
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
comm : (↑(insert i s) : Set ι).Pairwise (Function.onFun Commute f)
hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (s.noncommProd f hcomm)
heq1 : f i * s.noncommProd f ⋯ = 1
hnotMem' : i ∉ (↑s : Set ι)
heq1i : f i = 1
⊢ s.noncommProd f hcomm = 1

Tactic:
obtain ⟨heq1i : f i = 1, heq1S : s.noncommProd f _ = 1⟩ :=
        Subgroup.disjoint_iff_mul_eq_one.mp (hind.disjoint_biSup hnotMem') hmem.1 hmem_bsupr heq1

Premises used: iSupIndep.disjoint_biSup, Finset.noncommProd, And.left, Iff.mp, Subgroup.disjoint_iff_mul_eq_one
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i_1 : ι
s : Finset ι
hnotMem : i_1 ∉ s
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
comm : (↑(insert i_1 s) : Set ι).Pairwise (Function.onFun Commute f)
hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
hmem : f i_1 ∈ K i_1 ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (s.noncommProd f hcomm)
heq1 : f i_1 * s.noncommProd f ⋯ = 1
hnotMem' : i_1 ∉ (↑s : Set ι)
heq1i : f i_1 = 1
heq1S : s.noncommProd f hcomm = 1
i : ι
h : i ∈ insert i_1 s
⊢ i = i_1 ∨ i ∈ s

Tactic:
simp only [Finset.mem_insert] at h

Premises used: Finset.mem_insert
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i_1 : ι
s : Finset ι
hnotMem : i_1 ∉ s
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
comm : (↑(Insert.insert i_1 s) : Set ι).Pairwise (Function.onFun Commute f)
hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
hmem : f i_1 ∈ K i_1 ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (s.noncommProd f hcomm)
heq1 : f i_1 * s.noncommProd f ⋯ = 1
hnotMem' : i_1 ∉ (↑s : Set ι)
heq1i : f i_1 = 1
heq1S : s.noncommProd f hcomm = 1
i : ι
h : i = i_1 ∨ i ∈ s
insert :
  ∀ (hnotMem : i ∉ s) (comm : (↑(Insert.insert i s) : Set ι).Pairwise (Function.onFun Commute f))
    (hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x) (heq1 : f i * s.noncommProd f ⋯ = 1) (hnotMem' : i ∉ (↑s : Set ι))
    (heq1i : f i = 1), f i = 1
insert₁ : ∀ (h : i ∈ s), f i = 1
⊢ f i = 1

Tactic:
rcases h with (rfl | h)

Premises used: rfl
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
s : Finset ι
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
hmem_bsupr : Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (s.noncommProd f hcomm)
heq1S : s.noncommProd f hcomm = 1
i : ι
hnotMem : i ∉ s
comm : (↑(insert i s) : Set ι).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
heq1 : f i * s.noncommProd f ⋯ = 1
hnotMem' : i ∉ (↑s : Set ι)
heq1i : f i = 1
⊢ f i = 1

Tactic:
heq1i
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
s : Finset ι
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
hmem_bsupr : Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (s.noncommProd f hcomm)
heq1S : s.noncommProd f hcomm = 1
i : ι
hnotMem : i ∉ s
comm : (↑(insert i s) : Set ι).Pairwise (Function.onFun Commute f)
hmem : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
heq1 : f i * s.noncommProd f ⋯ = 1
hnotMem' : i ∉ (↑s : Set ι)
heq1i : f i = 1
⊢ f i = 1

Tactic:
exact heq1i
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i_1 : ι
s : Finset ι
hnotMem : i_1 ∉ s
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
comm : (↑(insert i_1 s) : Set ι).Pairwise (Function.onFun Commute f)
hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
hmem : f i_1 ∈ K i_1 ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (s.noncommProd f hcomm)
heq1 : f i_1 * s.noncommProd f ⋯ = 1
hnotMem' : i_1 ∉ (↑s : Set ι)
heq1i : f i_1 = 1
heq1S : s.noncommProd f hcomm = 1
i : ι
h : i ∈ s
⊢ f i = 1

Tactic:
ih hcomm hmem.2 heq1S _ h

Premises used: And.right
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
f : ι → G
K : ι → Subgroup G
hind : iSupIndep K
i_1 : ι
s : Finset ι
hnotMem : i_1 ∉ s
ih :
  ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
    (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
comm : (↑(insert i_1 s) : Set ι).Pairwise (Function.onFun Commute f)
hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
hmem : f i_1 ∈ K i_1 ∧ ∀ x ∈ s, f x ∈ K x
hmem_bsupr : Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (s.noncommProd f hcomm)
heq1 : f i_1 * s.noncommProd f ⋯ = 1
hnotMem' : i_1 ∉ (↑s : Set ι)
heq1i : f i_1 = 1
heq1S : s.noncommProd f hcomm = 1
i : ι
h : i ∈ s
⊢ f i = 1

Tactic:
refine ih hcomm hmem.2 heq1S _ h

Premises used: And.right
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
f : ι → G
comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
K : ι → Subgroup G
hind : iSupIndep K
hmem : ∀ x ∈ s, f x ∈ K x
empty :
  ∀ (comm : (↑∅ : Set ι).Pairwise (Function.onFun Commute f))
    (hmem : ∀ (x : ι), Membership.mem (γ := Finset ι) ∅ x → f x ∈ K x) (heq1 : Finset.noncommProd ∅ f comm = 1) (i : ι),
    Membership.mem (γ := Finset ι) ∅ i → f i = 1
insert :
  ∀ (i : ι) (s : Finset ι) (hnotMem : i ∉ s)
    (ih :
      ∀ (comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ s, f x ∈ K x)
        (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1)
    (comm : (↑(Insert.insert i s) : Set ι).Pairwise (Function.onFun Commute f))
    (hmem : ∀ x ∈ Insert.insert i s, f x ∈ K x) (heq1 : (Insert.insert i s).noncommProd f comm = 1),
    ∀ i_1 ∈ Insert.insert i s, f i_1 = 1
⊢ ∀ (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1

Tactic:
induction s using Finset.induction_on with
    | empty => simp
    | insert i s hnotMem ih =>
      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_notMem _ _ _ _ hnotMem] at heq1
      have hnotMem' : 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 hnotMem') 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

Premises used: Finset.forall_mem_insert, Insert.insert, Finset.mem_insert, Finset.noncommProd, rfl
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
G : Type u_1
inst : Group G
ι : Type u_2
s : Finset ι
f : ι → G
comm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
K : ι → Subgroup G
hind : iSupIndep K
hmem : ∀ x ∈ s, f x ∈ K x
heq1 : s.noncommProd f comm = 1
revert : ∀ (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
⊢ ∀ i ∈ s, f i = 1

Tactic:
classical
    revert heq1
    induction s using Finset.induction_on with
    | empty => simp
    | insert i s hnotMem ih =>
      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_notMem _ _ _ _ hnotMem] at heq1
      have hnotMem' : 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 hnotMem') 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

Premises used: Finset.forall_mem_insert, Insert.insert, Finset.mem_insert, Finset.noncommProd, rfl
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
apply :
  ∀ (x : ι),
    Membership.mem (γ := Finset ι) Finset.univ x → Eq.{u_1 + 1} (α := M) ((ϕ x : (a : N x) → M) (1 x) : M) (1 : M)
⊢ Eq.{u_1 + 1} (α := M) (Finset.noncommProd Finset.univ (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (1 i)) ⋯) 1

Tactic:
apply (Finset.noncommProd_eq_pow_card _ _ _ _ _).trans (one_pow _)

Premises used: one_pow, Finset.noncommProd_eq_pow_card, Eq.trans
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
⊢ ∀ (x : ι),
    Membership.mem (γ := Finset ι) Finset.univ x → Eq.{u_1 + 1} (α := M) ((ϕ x : (a : N x) → M) (1 x) : M) (1 : M)

Tactic:
simp
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
f g : (i : ι) → N i
⊢ Finset.noncommProd Finset.univ
      (HMul.hMul (α := ι → M) (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (f i)) fun (i : ι) ↦ (ϕ i : (a : N i) → M) (g i)) ⋯ =
    HMul.hMul (α := M) (Finset.noncommProd Finset.univ (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (f i)) ⋯)
      (Finset.noncommProd Finset.univ (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (g i)) ⋯)

Tactic:
@Finset.noncommProd_mul_distrib _ _ _ _ (fun i => ϕ i (f i)) (fun i => ϕ i (g i)) _ _ _

Premises used: Finset.noncommProd_mul_distrib, DFunLike.coe
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
f g : (i : ι) → N i
h :
  ∀ (x : ι),
    Membership.mem (γ := Finset ι) Finset.univ x →
      (ϕ x : (a : N x) → M) ((f * g) x) =
        HMul.hMul (α := ι → M) (β := ι → M) (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (f i))
          (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (g i)) x
convert_4 :
  (↑Finset.univ : Set ι).Pairwise fun (x y : ι) ↦
    Commute.{u_1} (S := M) ((fun (i : ι) ↦ ((ϕ i : (a : N i) → M) (g i) : M)) x)
      ((fun (i : ι) ↦ ((ϕ i : (a : N i) → M) (f i) : M)) y)
⊢ Finset.noncommProd Finset.univ (fun (i : ι) ↦ (ϕ i : (a : N i) → M) ((f * g) i)) ⋯ =
    HMul.hMul (α := M) (Finset.noncommProd Finset.univ (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (f i)) ⋯)
      (Finset.noncommProd Finset.univ (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (g i)) ⋯)

Tactic:
convert! @Finset.noncommProd_mul_distrib _ _ _ _ (fun i => ϕ i (f i)) (fun i => ϕ i (g i)) _ _ _

Premises used: Finset.noncommProd_mul_distrib, DFunLike.coe
-- Module: Mathlib.GroupTheory.NoncommPiCoprod
Goal:
M : Type u_1
inst : Monoid M
ι : Type u_2
inst_1 : Fintype ι
N : ι → Type u_3
inst_2 : (i : ι) → Monoid (N i)
ϕ : (i : ι) → MonoidHom.{u_3, u_1} (N i) M
hcomm :
  Pairwise fun (i j : ι) ↦
    ∀ (x : N i) (y : N j), Commute.{u_1} (S := M) ((ϕ i : (a : N i) → M) x : M) ((ϕ j : (a : N j) → M) y : M)
f g : (i : ι) → N i
x : ι
h : Membership.mem (γ := Finset ι) Finset.univ x
⊢ (ϕ x : (a : N x) → M) ((f * g) x) =
    HMul.hMul (α := ι → M) (β := ι → M) (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (f i))
      (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (g i)) x

Tactic:
map_mul _ _ _

Premises used: map_mul