awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
⊢ ∀ i ∈ s, f i = 1
have revert : ∀ (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
Tactic: revert heq1
Cleared hypotheses: heq1
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (hypothesis)
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
⊢ ∀ (heq1 : (insert i s).noncommProd f comm = 1), ∀ i_1 ∈ insert i s, f i_1 = 1
have hcomm : (↑s : Set ι).Pairwise (Function.onFun Commute f)
Tactic: have hcomm := comm.mono (Finset.coe_subset.2 <| Finset.subset_insert _ _)
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (hypothesis)
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)
⊢ ∀ (heq1 : (insert i s).noncommProd f comm = 1), ∀ i_1 ∈ insert i s, f i_1 = 1
have hmem₁ : f i ∈ K i ∧ ∀ x ∈ s, f x ∈ K x
Tactic: simp only [Finset.forall_mem_insert] at hmem
Cleared hypotheses: hmem
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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)
have refine : ∀ c ∈ s, Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (f c)
Tactic: refine Subgroup.noncommProd_mem _ _ ?_
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (hypothesis)
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
⊢ Membership.mem (γ := Subgroup G) (⨆ i ∈ (↑s : Set ι), K i) (f x)
have this : 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
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (hypothesis)
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
⊢ ∀ (heq1 : (insert i s).noncommProd f comm = 1), ∀ i_1 ∈ insert i s, f i_1 = 1
have hmem_bsupr : 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)
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (hypothesis)
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
⊢ ∀ i_1 ∈ insert i s, f i_1 = 1
have heq1₁ : f i * s.noncommProd f sorry = 1
Tactic: rw [Finset.noncommProd_insert_of_notMem _ _ _ _ hnotMem] at heq1
Cleared hypotheses: heq1
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (hypothesis)
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_1 ∈ insert i s, f i_1 = 1
have hnotMem' : i ∉ (↑s : Set ι)
Tactic: have hnotMem' : i ∉ (s : Set ι) := by simpa
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (hypothesis)
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 ι)
⊢ ∀ i_1 ∈ insert i s, f i_1 = 1
have heq1i : 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
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (hypothesis)
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
⊢ ∀ i_1 ∈ insert i s, f i_1 = 1
have heq1S : 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
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (hypothesis)
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
⊢ f i = 1
have h₁ : i = i_1 ∨ i ∈ s
Tactic: simp only [Finset.mem_insert] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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 = i_1 ∨ i ∈ s
⊢ f i = 1
have insert : ∀ (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 sorry = 1) (hnotMem' : i ∉ (↑s : Set ι))
  (heq1i : f i = 1), f i = 1
Tactic: rcases h with (rfl | h)
Cleared hypotheses: i_1, hnotMem, comm, hmem, heq1, hnotMem', heq1i, h
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
⊢ f i = 1
have insert₁ : ∀ (h : i ∈ s), f i = 1
Tactic: rcases h with (rfl | h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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), ∀ i ∈ s, f i = 1
have 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
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
Cleared hypotheses: s, comm, hmem
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
⊢ ∀ (heq1 : s.noncommProd f comm = 1), ∀ i ∈ s, f i = 1
have 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 i s) : Set ι).Pairwise (Function.onFun Commute f)) (hmem : ∀ x ∈ insert i s, f x ∈ K x)
  (heq1 : (insert i s).noncommProd f comm = 1), ∀ i_1 ∈ insert i s, f i_1 = 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
Cleared hypotheses: s, comm, hmem
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
⊢ ∀ i ∈ s, f i = 1
have revert : ∀ (heq1 : s.noncommProd f comm = 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
Cleared hypotheses: heq1
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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)
⊢ Eq.{u_1 + 1} (α := M) (Finset.noncommProd Finset.univ (fun (i : ι) ↦ (ϕ i : (a : N i) → M) (1 i)) ⋯) 1
have apply : ∀ (x : ι),
  Membership.mem (γ := Finset ι) Finset.univ x → Eq.{u_1 + 1} (α := M) ((ϕ x : (a : N x) → M) (1 x) : M) (1 : M)
Tactic: apply (Finset.noncommProd_eq_pow_card _ _ _ _ _).trans (one_pow _)
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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 (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)) ⋯)
have 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
Tactic: convert! @Finset.noncommProd_mul_distrib _ _ _ _ (fun i => ϕ i (f i)) (fun i => ϕ i (g i)) _ _ _
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
⊢ 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)) ⋯)
have 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)
Tactic: convert! @Finset.noncommProd_mul_distrib _ _ _ _ (fun i => ϕ i (f i)) (fun i => ϕ i (g i)) _ _ _
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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 (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)) ⋯)
have 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
Tactic: classical
    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 _ _
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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
⊢ 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)) ⋯)
have 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)
Tactic: classical
    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 _ _
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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)
inst_3 : DecidableEq ι
i : ι
y : N i
⊢ Eq.{u_1 + 1} (α := M) ((noncommPiCoprod (N := N) ϕ hcomm : (a : (i : ι) → N i) → M) (Pi.mulSingle (M := N) i y) : M)
    ((ϕ i : (a : N i) → M) y : M)
have change : Eq.{u_1 + 1} (α := M)
  (Finset.noncommProd Finset.univ (fun (j : ι) ↦ (ϕ j : (a : N j) → M) (Pi.mulSingle (M := N) i y j)) sorry : M)
  ((ϕ i : (a : N i) → M) y : M)
Tactic: change Finset.univ.noncommProd (fun j => ϕ j (Pi.mulSingle i y j)) (fun _ _ _ _ h => hcomm h _ _)
    = ϕ i y
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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)
inst_3 : DecidableEq ι
i : ι
y : N i
⊢ Eq.{u_1 + 1} (α := M)
    (Finset.noncommProd Finset.univ (fun (j : ι) ↦ (ϕ j : (a : N j) → M) (Pi.mulSingle (M := N) i y j)) ⋯ : M)
    ((ϕ i : (a : N i) → M) y : M)
have rw : Eq.{u_1 + 1} (α := M)
  ((insert i (Finset.erase Finset.univ i)).noncommProd
      (fun (j : ι) ↦ (ϕ j : (a : N j) → M) (Pi.mulSingle (M := N) i y j)) sorry :
    M)
  ((ϕ i : (a : N i) → M) y : M)
Tactic: rw [← Finset.insert_erase (Finset.mem_univ i)]
-- Lean 4 proof step from Mathlib.GroupTheory.NoncommPiCoprod (goal)
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)
inst_3 : DecidableEq ι
i : ι
y : N i
⊢ Eq.{u_1 + 1} (α := M)
    ((insert i (Finset.erase Finset.univ i)).noncommProd
        (fun (j : ι) ↦ (ϕ j : (a : N j) → M) (Pi.mulSingle (M := N) i y j)) ⋯ :
      M)
    ((ϕ i : (a : N i) → M) y : M)
have rw : HMul.hMul (α := M) (β := M) ((ϕ i : (a : N i) → M) (Pi.mulSingle (M := N) i y i) : M)
    ((Finset.erase Finset.univ i).noncommProd (fun (j : ι) ↦ (ϕ j : (a : N j) → M) (Pi.mulSingle (M := N) i y j)) sorry :
      M) =
  (ϕ i : (a : N i) → M) y
Tactic: rw [Finset.noncommProd_insert_of_notMem _ _ _ _ (Finset.notMem_erase i _)]