awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
f : α → β → β
s : Multiset α
h : LeftCommutative f
b : β
⊢ noncommFoldr f s ⋯ b = foldr f b s
have h₁ : ∀ (a : List α), noncommFoldr f ⟦a⟧ sorry b = foldr f b ⟦a⟧
Tactic: induction s using Quotient.inductionOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
assoc : Std.Associative op
s : Multiset α
comm : Set.Pairwise {x : α | x ∈ s} fun (x y : α) ↦ op x y = op y x
x : α
hx : Membership.mem (γ := Set α) {x : α | x ∈ s} x
y : α
hy : Membership.mem (γ := Set α) {x : α | x ∈ s} y
h : x ≠ y
b : α
⊢ op x (op y b) = op y (op x b)
have rw : op (op x y) b = op y (op x b)
Tactic: rw [← assoc.assoc, comm hx hy h, assoc.assoc]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
assoc : Std.Associative op
s : Multiset α
comm : Set.Pairwise {x : α | x ∈ s} fun (x y : α) ↦ op x y = op y x
x : α
hx : Membership.mem (γ := Set α) {x : α | x ∈ s} x
y : α
hy : Membership.mem (γ := Set α) {x : α | x ∈ s} y
h : x ≠ y
b : α
rw : op (op x y) b = op y (op x b)
⊢ op x (op y b) = op y (op x b)
have rw₁ : op (op y x) b = op y (op x b)
Tactic: rw [← assoc.assoc, comm hx hy h, assoc.assoc]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
assoc : Std.Associative op
s : Multiset α
comm : Set.Pairwise {x : α | x ∈ s} fun (x y : α) ↦ op x y = op y x
x : α
hx : Membership.mem (γ := Set α) {x : α | x ∈ s} x
y : α
hy : Membership.mem (γ := Set α) {x : α | x ∈ s} y
h : x ≠ y
b : α
rw : op (op x y) b = op y (op x b)
rw₁ : op (op y x) b = op y (op x b)
⊢ op x (op y b) = op y (op x b)
have rw₂ : op y (op x b) = op y (op x b)
Tactic: rw [← assoc.assoc, comm hx hy h, assoc.assoc]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
op : α → α → α
assoc : Std.Associative op
s : Multiset α
a : α
h : Set.Pairwise {x : α | x ∈ a ::ₘ s} fun (x y : α) ↦ op x y = op y x
h' : Set.Pairwise {x : α | x ∈ s} fun (x y : α) ↦ op x y = op y x
x : α
⊢ noncommFold op (a ::ₘ s) h x = op a (noncommFold op s h' x)
have h₁ : ∀ (a_1 : List α) (h : Set.Pairwise {x : α | x ∈ a ::ₘ ⟦a_1⟧} fun (x y : α) ↦ op x y = op y x)
  (h' : Set.Pairwise {x : α | x ∈ ⟦a_1⟧} fun (x y : α) ↦ op x y = op y x),
  noncommFold op (a ::ₘ ⟦a_1⟧) h x = op a (noncommFold op ⟦a_1⟧ h' x)
Tactic: induction s using Quotient.inductionOn
Cleared hypotheses: s, h, h'
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
op : α → α → α
assoc : Std.Associative op
s : Multiset α
inst : Std.Commutative op
a : α
⊢ noncommFold op s ⋯ a = fold op a s
have h : ∀ (a_1 : List α), noncommFold op ⟦a_1⟧ sorry a = fold op a ⟦a_1⟧
Tactic: induction s using Quotient.inductionOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
l : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑l : Multiset α)} Commute
⊢ noncommFold (fun (x1 x2 : α) ↦ x1 * x2) (↑l : Multiset α) comm 1 = l.prod
have simp : List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 l = l.prod
Tactic: simp only [noncommFold_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
hd : α
tl : List α
hl :
  ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑tl : Multiset α)} Commute),
    List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 tl = tl.prod
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑(hd :: tl) : Multiset α)} Commute
⊢ List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 (hd :: tl) = (hd :: tl).prod
have cons : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑tl : Multiset α)} Commute
Tactic: rw [List.prod_cons, List.foldr, hl]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
l : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑l : Multiset α)} Commute
⊢ List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 l = l.prod
have nil : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | Membership.mem (γ := Multiset α) (↑[] : Multiset α) x} Commute),
  Eq.{u_3 + 1} (α := α) (List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 []) (List.prod [])
Tactic: induction l with
  | nil => simp
  | cons hd tl hl =>
    rw [List.prod_cons, List.foldr, hl]
    intro x hx y hy
    exact comm (List.mem_cons_of_mem _ hx) (List.mem_cons_of_mem _ hy)
Cleared hypotheses: l, comm
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
l : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑l : Multiset α)} Commute
nil :
  ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | Membership.mem (γ := Multiset α) (↑[] : Multiset α) x} Commute),
    Eq.{u_3 + 1} (α := α) (List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 []) (List.prod [])
⊢ List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 l = l.prod
have cons : ∀ (hd : α) (tl : List α)
  (hl :
    ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑tl : Multiset α)} Commute),
      List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 tl = tl.prod)
  (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ (↑(hd :: tl) : Multiset α)} Commute),
  List.foldr (fun (x1 x2 : α) ↦ x1 * x2) 1 (hd :: tl) = (hd :: tl).prod
Tactic: induction l with
  | nil => simp
  | cons hd tl hl =>
    rw [List.prod_cons, List.foldr, hl]
    intro x hx y hy
    exact comm (List.mem_cons_of_mem _ hx) (List.mem_cons_of_mem _ hy)
Cleared hypotheses: l, comm
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
s : Multiset α
a : α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ s} Commute
⊢ (a ::ₘ s).noncommProd comm = a * s.noncommProd ⋯
have h : ∀ (a_1 : List α) (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦a_1⟧} Commute),
  (a ::ₘ ⟦a_1⟧).noncommProd comm = a * noncommProd ⟦a_1⟧ sorry
Tactic: induction s using Quotient.inductionOn
Cleared hypotheses: s, comm
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
s : Multiset α
a : α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ s} Commute
⊢ (a ::ₘ s).noncommProd comm = s.noncommProd ⋯ * a
have h : ∀ (s : List α) (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦s⟧} Commute),
  (a ::ₘ ⟦s⟧).noncommProd comm = noncommProd ⟦s⟧ sorry * a
Tactic: induction s using Quotient.inductionOn with | _ s
Cleared hypotheses: s, comm
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
a : α
s : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦s⟧} Commute
⊢ (a ::ₘ ⟦s⟧).noncommProd comm = noncommProd ⟦s⟧ ⋯ * a
have h : a * s.prod = s.prod * a
Tactic: simp only [quot_mk_to_coe, cons_coe, noncommProd_coe, List.prod_cons]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
a hd : α
tl : List α
IH : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦tl⟧} Commute), a * tl.prod = tl.prod * a
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} Commute
⊢ a * (hd :: tl).prod = (hd :: tl).prod * a
have h : a * hd * tl.prod = hd * a * tl.prod
Tactic: rw [List.prod_cons, mul_assoc, ← IH, ← mul_assoc, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
a hd : α
tl : List α
IH : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦tl⟧} Commute), a * tl.prod = tl.prod * a
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} Commute
h : a * hd * tl.prod = hd * a * tl.prod
⊢ a * (hd :: tl).prod = (hd :: tl).prod * a
have h₁ : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦tl⟧} Commute
Tactic: rw [List.prod_cons, mul_assoc, ← IH, ← mul_assoc, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
a hd : α
tl : List α
IH : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦tl⟧} Commute), a * tl.prod = tl.prod * a
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} Commute
⊢ a * hd * tl.prod = hd * a * tl.prod
have h : a * hd = hd * a
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
a hd : α
tl : List α
IH : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦tl⟧} Commute), a * tl.prod = tl.prod * a
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} Commute
⊢ a * hd = hd * a
have h : Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} a
Tactic: apply comm.of_refl
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
a hd : α
tl : List α
IH : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦tl⟧} Commute), a * tl.prod = tl.prod * a
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} Commute
h : Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} a
⊢ a * hd = hd * a
have h₁ : Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} hd
Tactic: apply comm.of_refl
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (hypothesis)
Goal:
α : Type u_3
inst : Monoid α
a hd : α
tl : List α
IH : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦tl⟧} Commute), a * tl.prod = tl.prod * a
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} Commute
x : α
hx : Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦tl⟧} x
y : α
hy : Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦tl⟧} y
⊢ x ≠ y → Commute x y
have hx₁ : Membership.mem (γ := Set α) {x : α | x = a ∨ x ∈ tl} x
Tactic: simp only [quot_mk_to_coe, List.mem_cons, mem_coe, cons_coe] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (hypothesis)
Goal:
α : Type u_3
inst : Monoid α
a hd : α
tl : List α
IH : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦tl⟧} Commute), a * tl.prod = tl.prod * a
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} Commute
x : α
hx : Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦tl⟧} x
y : α
hy : Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦tl⟧} y
hx₁ : Membership.mem (γ := Set α) {x : α | x = a ∨ x ∈ tl} x
⊢ x ≠ y → Commute x y
have hy₁ : Membership.mem (γ := Set α) {x : α | x = a ∨ x ∈ tl} y
Tactic: simp only [quot_mk_to_coe, List.mem_cons, mem_coe, cons_coe] at hx hy
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
a hd : α
tl : List α
IH : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦tl⟧} Commute), a * tl.prod = tl.prod * a
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} Commute
x y : α
hx : Membership.mem (γ := Set α) {x : α | x = a ∨ x ∈ tl} x
hy : Membership.mem (γ := Set α) {x : α | x = a ∨ x ∈ tl} y
⊢ x ≠ y → Commute x y
have h : Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} x
Tactic: apply comm
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
a hd : α
tl : List α
IH : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦tl⟧} Commute), a * tl.prod = tl.prod * a
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} Commute
x y : α
hx : Membership.mem (γ := Set α) {x : α | x = a ∨ x ∈ tl} x
hy : Membership.mem (γ := Set α) {x : α | x = a ∨ x ∈ tl} y
h : Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} x
⊢ x ≠ y → Commute x y
have h₁ : Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} y
Tactic: apply comm
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
a hd : α
tl : List α
IH : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦tl⟧} Commute), a * tl.prod = tl.prod * a
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} Commute
x y : α
hx : Membership.mem (γ := Set α) {x : α | x = a ∨ x ∈ tl} x
hy : Membership.mem (γ := Set α) {x : α | x = a ∨ x ∈ tl} y
⊢ Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} x
have h : x = a → Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} x
Tactic: cases hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
a hd : α
tl : List α
IH : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦tl⟧} Commute), a * tl.prod = tl.prod * a
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} Commute
x y : α
hx : Membership.mem (γ := Set α) {x : α | x = a ∨ x ∈ tl} x
hy : Membership.mem (γ := Set α) {x : α | x = a ∨ x ∈ tl} y
h : x = a → Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} x
⊢ Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} x
have h₁ : x ∈ tl → Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} x
Tactic: cases hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
a hd : α
tl : List α
IH : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦tl⟧} Commute), a * tl.prod = tl.prod * a
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} Commute
x y : α
hx : Membership.mem (γ := Set α) {x : α | x = a ∨ x ∈ tl} x
hy : Membership.mem (γ := Set α) {x : α | x = a ∨ x ∈ tl} y
⊢ Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} y
have h : y = a → Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} y
Tactic: cases hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
a hd : α
tl : List α
IH : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦tl⟧} Commute), a * tl.prod = tl.prod * a
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} Commute
x y : α
hx : Membership.mem (γ := Set α) {x : α | x = a ∨ x ∈ tl} x
hy : Membership.mem (γ := Set α) {x : α | x = a ∨ x ∈ tl} y
h : y = a → Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} y
⊢ Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} y
have h₁ : y ∈ tl → Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} y
Tactic: cases hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
a : α
s : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦s⟧} Commute
⊢ a * s.prod = s.prod * a
have h : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦[]⟧} Commute), a * List.prod [] = List.prod [] * a
Tactic: induction s with
  | nil => simp
  | cons hd tl IH =>
    rw [List.prod_cons, mul_assoc, ← IH, ← mul_assoc, ← mul_assoc]
    · congr 1
      apply comm.of_refl <;> simp
    · intro x hx y hy
      simp only [quot_mk_to_coe, List.mem_cons, mem_coe, cons_coe] at hx hy
      apply comm
      · cases hx <;> simp [*]
      · cases hy <;> simp [*]
Cleared hypotheses: s, comm
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
a : α
s : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦s⟧} Commute
h : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦[]⟧} Commute), a * List.prod [] = List.prod [] * a
⊢ a * s.prod = s.prod * a
have h₁ : ∀ (hd : α) (tl : List α)
  (IH : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦tl⟧} Commute), a * tl.prod = tl.prod * a)
  (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} Commute), a * (hd :: tl).prod = (hd :: tl).prod * a
Tactic: induction s with
  | nil => simp
  | cons hd tl IH =>
    rw [List.prod_cons, mul_assoc, ← IH, ← mul_assoc, ← mul_assoc]
    · congr 1
      apply comm.of_refl <;> simp
    · intro x hx y hy
      simp only [quot_mk_to_coe, List.mem_cons, mem_coe, cons_coe] at hx hy
      apply comm
      · cases hx <;> simp [*]
      · cases hy <;> simp [*]
Cleared hypotheses: s, comm
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
s t : Multiset α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ s + t} Commute
⊢ (s + t).noncommProd comm = s.noncommProd ⋯ * t.noncommProd ⋯
have mk : ∀ (a : List α)
  (comm :
    Set.Pairwise.{u_3} (α := α) {x : α | x ∈ Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a + t} Commute),
  (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a + t).noncommProd comm =
    noncommProd (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a) sorry * t.noncommProd sorry
Tactic: rcases s with ⟨⟩
Cleared hypotheses: comm
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
s t : Multiset α
a : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a + t} Commute
⊢ (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a + t).noncommProd comm =
    noncommProd (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a) ⋯ * t.noncommProd ⋯
have mk : ∀ (a_1 : List α)
  (comm :
    Set.Pairwise.{u_3} (α := α)
      {x : α |
        x ∈
          HAdd.hAdd (α := Multiset α) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a)
            (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a_1)}
      Commute),
  (HAdd.hAdd (α := Multiset α) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a)
          (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a_1)).noncommProd
      comm =
    noncommProd (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a) sorry *
      noncommProd (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a_1) sorry
Tactic: rcases t with ⟨⟩
Cleared hypotheses: comm
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
s : Multiset α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ s} Commute
p : α → Prop
hom : ∀ (a b : α), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p x
⊢ p (s.noncommProd comm)
have h : ∀ (l : List α) (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ ⟦l⟧} Commute) (base : ∀ x ∈ ⟦l⟧, p x),
  p (noncommProd ⟦l⟧ comm)
Tactic: induction s using Quotient.inductionOn with | _ l
Cleared hypotheses: s, comm, base
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
p : α → Prop
hom : ∀ (a b : α), p a → p b → p (a * b)
unit : p 1
l : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ ⟦l⟧} Commute
base : ∀ x ∈ ⟦l⟧, p x
⊢ p (noncommProd ⟦l⟧ comm)
have h : ∀ (base : ∀ x ∈ l, p x), p l.prod
Tactic: simp only [quot_mk_to_coe, noncommProd_coe, mem_coe] at base ⊢
Cleared hypotheses: base
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
F : Type u_1
α : Type u_3
β : Type u_4
inst : Monoid α
inst_1 : Monoid β
inst_2 : FunLike F α β
inst_3 : MulHomClass F α β
s : Multiset α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ s} Commute
f : F
⊢ Set.Pairwise.{u_4} (α := β) {x : β | Membership.mem (γ := Multiset β) (map (⇑f : (a : α) → β) s) x} Commute
have simp : Set.Pairwise.{u_4} (α := β) {x : β | ∃ a ∈ s, (f : (a : α) → β) a = x} Commute
Tactic: simp only [Multiset.mem_map]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
F : Type u_1
α : Type u_3
β : Type u_4
inst : Monoid α
inst_1 : Monoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
s : Multiset α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ s} Commute
f : F
⊢ (f : (a : α) → β) (s.noncommProd comm) = noncommProd (map (⇑f : (a : α) → β) s) ⋯
have h : ∀ (a : List α) (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ ⟦a⟧} Commute),
  (f : (a : α) → β) (noncommProd ⟦a⟧ comm) = noncommProd (map (⇑f : (a : α) → β) ⟦a⟧) sorry
Tactic: induction s using Quotient.inductionOn
Cleared hypotheses: s, comm
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
s : Multiset α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ s} Commute
m : α
h : ∀ x ∈ s, x = m
⊢ s.noncommProd comm = m ^ s.card
have h₁ : ∀ (a : List α) (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ ⟦a⟧} Commute) (h : ∀ x ∈ ⟦a⟧, x = m),
  noncommProd ⟦a⟧ comm = m ^ card ⟦a⟧
Tactic: induction s using Quotient.inductionOn
Cleared hypotheses: s, comm, h
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
m : α
a : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ ⟦a⟧} Commute
h : ∀ x ∈ ⟦a⟧, x = m
⊢ noncommProd ⟦a⟧ comm = m ^ card ⟦a⟧
have h₁ : ∀ (h : ∀ x ∈ a, x = m), a.prod = m ^ a.length
Tactic: simp only [quot_mk_to_coe, noncommProd_coe, coe_card, mem_coe] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_6
inst : CommMonoid α
s : Multiset α
⊢ s.noncommProd ⋯ = s.prod
have h : ∀ (a : List α), noncommProd ⟦a⟧ sorry = prod ⟦a⟧
Tactic: induction s using Quotient.inductionOn
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
s : Multiset α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ s} Commute
y : α
h : ∀ x ∈ s, Commute y x
⊢ Commute y (s.noncommProd comm)
have h₁ : ∀ (a : List α) (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ ⟦a⟧} Commute) (h : ∀ x ∈ ⟦a⟧, Commute y x),
  Commute y (noncommProd ⟦a⟧ comm)
Tactic: induction s using Quotient.inductionOn
Cleared hypotheses: s, comm, h
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
y : α
a : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ ⟦a⟧} Commute
h : ∀ x ∈ ⟦a⟧, Commute y x
⊢ Commute y (noncommProd ⟦a⟧ comm)
have h₁ : Commute y a.prod
Tactic: simp only [quot_mk_to_coe, noncommProd_coe]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
inst_1 : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ s} Commute
comm' :
  ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | x ∈ s.erase a} x) (x_1 : α)
    (hy : Membership.mem (γ := Set α) {x : α | x ∈ s.erase a} x_1) (hxy : x ≠ x_1), Commute x x_1
⊢ a * (s.erase a).noncommProd comm' = s.noncommProd comm
have h₁ : ∀ (l : List α) (h : a ∈ ⟦l⟧) (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ ⟦l⟧} Commute)
  (comm' :
    ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | x ∈ erase ⟦l⟧ a} x) (x_1 : α)
      (hy : Membership.mem (γ := Set α) {x : α | x ∈ erase ⟦l⟧ a} x_1) (hxy : x ≠ x_1), Commute x x_1),
  a * (erase ⟦l⟧ a).noncommProd comm' = noncommProd ⟦l⟧ comm
Tactic: induction s using Quotient.inductionOn with | _ l
Cleared hypotheses: s, h, comm, comm'
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
inst_1 : DecidableEq α
a : α
l : List α
h : a ∈ ⟦l⟧
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ ⟦l⟧} Commute
comm' :
  ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | x ∈ erase ⟦l⟧ a} x) (x_1 : α)
    (hy : Membership.mem (γ := Set α) {x : α | x ∈ erase ⟦l⟧ a} x_1) (hxy : x ≠ x_1), Commute x x_1
⊢ a * (erase ⟦l⟧ a).noncommProd comm' = noncommProd ⟦l⟧ comm
have h₁ : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ l} Commute) (h : a ∈ l), a * (l.erase a).prod = l.prod
Tactic: simp only [quot_mk_to_coe, mem_coe, coe_erase, noncommProd_coe] at comm h ⊢
Cleared hypotheses: h, comm
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
inst_1 : DecidableEq α
a : α
l : List α
comm' :
  ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | x ∈ erase ⟦l⟧ a} x) (x_1 : α)
    (hy : Membership.mem (γ := Set α) {x : α | x ∈ erase ⟦l⟧ a} x_1) (hxy : x ≠ x_1), Commute x x_1
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ l} Commute
h : a ∈ l
this : ∀ x ∈ l, ∀ y ∈ l, x * y = y * x
⊢ a * (l.erase a).prod = l.prod
have rw : l.prod = l.prod
Tactic: rw [List.prod_erase_of_comm h this]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
inst : Monoid α
inst_1 : DecidableEq α
a : α
l : List α
comm' :
  ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | x ∈ erase ⟦l⟧ a} x) (x_1 : α)
    (hy : Membership.mem (γ := Set α) {x : α | x ∈ erase ⟦l⟧ a} x_1) (hxy : x ≠ x_1), Commute x x_1
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ l} Commute
h : a ∈ l
⊢ a * (l.erase a).prod = l.prod
have h₁ : ∀ x ∈ l, ∀ y ∈ l, x * y = y * x
Tactic: suffices ∀ x ∈ l, ∀ y ∈ l, x * y = y * x by rw [List.prod_erase_of_comm h this]