awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : α
hx : x ∈ l
y : α
hy : y ∈ l
⊢ x * y = y * x
have h₁ : ∀ (hy : x ∈ l), x * x = x * x
Tactic: rcases eq_or_ne x y with rfl | hxy
Cleared hypotheses: y, hy
-- 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
x : α
hx : x ∈ l
y : α
hy : y ∈ l
h₁ : ∀ (hy : x ∈ l), x * x = x * x
⊢ x * y = y * x
have h₂ : ∀ (hxy : x ≠ y), x * y = y * x
Tactic: rcases eq_or_ne x y with rfl | hxy
-- 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
this : ∀ b ∈ s.erase a, Commute a b
⊢ (s.erase a).noncommProd comm' * a = s.noncommProd comm
have rw : a * (s.erase a).noncommProd comm' = s.noncommProd comm
Tactic: rw [← (noncommProd_commute (s.erase a) comm' a this).eq, mul_noncommProd_erase s h comm comm']
-- 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
this : ∀ b ∈ s.erase a, Commute a b
rw : a * (s.erase a).noncommProd comm' = s.noncommProd comm
⊢ (s.erase a).noncommProd comm' * a = s.noncommProd comm
have rw₁ : s.noncommProd comm = s.noncommProd comm
Tactic: rw [← (noncommProd_commute (s.erase a) comm' a this).eq, mul_noncommProd_erase s h comm comm']
-- 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
⊢ (s.erase a).noncommProd comm' * a = s.noncommProd comm
have suffices : ∀ b ∈ s.erase a, Commute a b
Tactic: suffices ∀ b ∈ erase s a, Commute a b by
    rw [← (noncommProd_commute (s.erase a) comm' a this).eq, mul_noncommProd_erase s h comm comm']
-- 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
b : α
hb : b ∈ s.erase a
⊢ Commute a b
have inl : ∀ (hb : a ∈ s.erase a), Commute a a
Tactic: rcases eq_or_ne a b with rfl | hab
Cleared hypotheses: b, hb
-- 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
b : α
hb : b ∈ s.erase a
inl : ∀ (hb : a ∈ s.erase a), Commute a a
⊢ Commute a b
have inr : ∀ (hab : a ≠ b), Commute a b
Tactic: rcases eq_or_ne a b with rfl | hab
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
f : α → β
comm : (↑s : Set α).Pairwise (Commute on f)
p : β → Prop
hom : ∀ (a b : β), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p (f x)
⊢ p (s.noncommProd f comm)
have refine : ∀ (b : β) (hb : b ∈ Multiset.map f s.val), p b
Tactic: refine Multiset.noncommProd_induction _ _ _ hom unit fun b hb ↦ ?_
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
f : α → β
comm : (↑s : Set α).Pairwise (Commute on f)
p : β → Prop
hom : ∀ (a b : β), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p (f x)
b : β
hb : b ∈ Multiset.map f s.val
⊢ p b
have obtain : ∀ (a : α) (ha : a ∈ s) (hb : f a ∈ Multiset.map f s.val), p (f a)
Tactic: obtain (⟨a, ha : a ∈ s, rfl : f a = b⟩) := by simpa using hb
Cleared hypotheses: b, hb
-- 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_1 : α → β → β
op : α → α → α
inst : Monoid β
inst_1 : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁ : Set α).Pairwise (Commute on f)
x : α
hx : x ∈ (↑s₂ : Set α)
y : α
hy : y ∈ (↑s₂ : Set α)
h : x ≠ y
⊢ Commute (g x) (g y)
have rw : Commute (f x) (f y)
Tactic: rw [← h₂ _ hx, ← h₂ _ hy]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (hypothesis)
Goal:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f_1 : α → β → β
op : α → α → α
inst : Monoid β
inst_1 : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁ : Set α).Pairwise (Commute on f)
x : α
hx : x ∈ (↑s₂ : Set α)
y : α
hy : y ∈ (↑s₂ : Set α)
h : x ≠ y
⊢ Commute (f x) (f y)
have h₃ : ∀ x ∈ s₁, f x = g x
Tactic: subst h₁
Cleared hypotheses: s₂, h₁, h₂, hx, hy
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (hypothesis)
Goal:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f_1 : α → β → β
op : α → α → α
inst : Monoid β
inst_1 : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁ : Set α).Pairwise (Commute on f)
x : α
hx : x ∈ (↑s₂ : Set α)
y : α
hy : y ∈ (↑s₂ : Set α)
h : x ≠ y
h₃ : ∀ x ∈ s₁, f x = g x
⊢ Commute (f x) (f y)
have hx₁ : x ∈ (↑s₁ : Set α)
Tactic: subst h₁
Cleared hypotheses: s₂, h₁, h₂, hx, hy
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (hypothesis)
Goal:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f_1 : α → β → β
op : α → α → α
inst : Monoid β
inst_1 : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁ : Set α).Pairwise (Commute on f)
x : α
hx : x ∈ (↑s₂ : Set α)
y : α
hy : y ∈ (↑s₂ : Set α)
h : x ≠ y
h₃ : ∀ x ∈ s₁, f x = g x
hx₁ : x ∈ (↑s₁ : Set α)
⊢ Commute (f x) (f y)
have hy₁ : y ∈ (↑s₁ : Set α)
Tactic: subst h₁
Cleared hypotheses: s₂, h₁, h₂, hx, hy
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
inst_1 : DecidableEq α
l : List α
f : α → β
comm : (↑l.toFinset : Set α).Pairwise (Commute on f)
hl : l.Nodup
⊢ l.toFinset.noncommProd f comm = (List.map f l).prod
have hl₁ : l.dedup = l
Tactic: rw [← List.dedup_eq_self] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha) : Set α).Pairwise (Commute on f)
⊢ (cons a s ha).noncommProd f comm = f a * s.noncommProd f ⋯
have simp_rw : (Multiset.map f (cons a s ha).val).noncommProd sorry = f a * (Multiset.map f s.val).noncommProd sorry
Tactic: simp_rw [noncommProd, Finset.cons_val, Multiset.map_cons, Multiset.noncommProd_cons]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha) : Set α).Pairwise (Commute on f)
simp_rw : (Multiset.map f (cons a s ha).val).noncommProd ⋯ = f a * (Multiset.map f s.val).noncommProd ⋯
⊢ (cons a s ha).noncommProd f comm = f a * s.noncommProd f ⋯
have simp_rw₁ : (Multiset.map f (a ::ₘ s.val)).noncommProd sorry = f a * (Multiset.map f s.val).noncommProd sorry
Tactic: simp_rw [noncommProd, Finset.cons_val, Multiset.map_cons, Multiset.noncommProd_cons]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha) : Set α).Pairwise (Commute on f)
simp_rw : (Multiset.map f (cons a s ha).val).noncommProd ⋯ = f a * (Multiset.map f s.val).noncommProd ⋯
simp_rw₁ : (Multiset.map f (a ::ₘ s.val)).noncommProd ⋯ = f a * (Multiset.map f s.val).noncommProd ⋯
⊢ (cons a s ha).noncommProd f comm = f a * s.noncommProd f ⋯
have simp_rw₂ : (f a ::ₘ Multiset.map f s.val).noncommProd sorry = f a * (Multiset.map f s.val).noncommProd sorry
Tactic: simp_rw [noncommProd, Finset.cons_val, Multiset.map_cons, Multiset.noncommProd_cons]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha) : Set α).Pairwise (Commute on f)
⊢ (cons a s ha).noncommProd f comm = s.noncommProd f ⋯ * f a
have simp_rw : (Multiset.map f (cons a s ha).val).noncommProd sorry = (Multiset.map f s.val).noncommProd sorry * f a
Tactic: simp_rw [noncommProd, Finset.cons_val, Multiset.map_cons, Multiset.noncommProd_cons']
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha) : Set α).Pairwise (Commute on f)
simp_rw : (Multiset.map f (cons a s ha).val).noncommProd ⋯ = (Multiset.map f s.val).noncommProd ⋯ * f a
⊢ (cons a s ha).noncommProd f comm = s.noncommProd f ⋯ * f a
have simp_rw₁ : (Multiset.map f (a ::ₘ s.val)).noncommProd sorry = (Multiset.map f s.val).noncommProd sorry * f a
Tactic: simp_rw [noncommProd, Finset.cons_val, Multiset.map_cons, Multiset.noncommProd_cons']
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
a : α
f : α → β
ha : a ∉ s
comm : (↑(cons a s ha) : Set α).Pairwise (Commute on f)
simp_rw : (Multiset.map f (cons a s ha).val).noncommProd ⋯ = (Multiset.map f s.val).noncommProd ⋯ * f a
simp_rw₁ : (Multiset.map f (a ::ₘ s.val)).noncommProd ⋯ = (Multiset.map f s.val).noncommProd ⋯ * f a
⊢ (cons a s ha).noncommProd f comm = s.noncommProd f ⋯ * f a
have simp_rw₂ : (f a ::ₘ Multiset.map f s.val).noncommProd sorry = (Multiset.map f s.val).noncommProd sorry * f a
Tactic: simp_rw [noncommProd, Finset.cons_val, Multiset.map_cons, Multiset.noncommProd_cons']
-- 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_1 : α → β → β
op : α → α → α
inst : Monoid β
inst_1 : Monoid γ
a : α
f : α → β
⊢ (↑{a} : Set α).Pairwise (Commute on f)
have norm_cast : Set.Pairwise {a} (Commute on f)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
f : α → β
comm : (↑s : Set α).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ s.noncommProd f comm = m ^ #s
have rw : m ^ (Multiset.map f s.val).card = m ^ #s
Tactic: rw [noncommProd, Multiset.noncommProd_eq_pow_card _ _ m]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
f : α → β
comm : (↑s : Set α).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
rw : m ^ (Multiset.map f s.val).card = m ^ #s
⊢ s.noncommProd f comm = m ^ #s
have rw₁ : ∀ x ∈ Multiset.map f s.val, x = m
Tactic: rw [noncommProd, Multiset.noncommProd_eq_pow_card _ _ m]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
f : α → β
comm : (↑s : Set α).Pairwise (Commute on f)
y : β
h : ∀ x ∈ s, Commute y (f x)
⊢ Commute y (s.noncommProd f comm)
have h₁ : ∀ x ∈ Multiset.map f s.val, Commute y x
Tactic: apply Multiset.noncommProd_commute
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
f : α → β
comm : (↑s : Set α).Pairwise (Commute on f)
y_1 : β
h : ∀ x ∈ s, Commute y_1 (f x)
y : β
⊢ y ∈ Multiset.map f s.val → Commute y_1 y
have h₁ : (∃ a ∈ s.val, f a = y) → Commute y_1 y
Tactic: rw [Multiset.mem_map]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_6
inst : CommMonoid β
s : Finset α
f : α → β
⊢ s.noncommProd f ⋯ = s.prod f
have empty : noncommProd ∅ f sorry = Finset.prod ∅ f
Tactic: induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s ha IH => simp [IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_6
inst : CommMonoid β
s : Finset α
f : α → β
empty : noncommProd ∅ f ⋯ = Finset.prod ∅ f
⊢ s.noncommProd f ⋯ = s.prod f
have cons : ∀ (a : α) (s : Finset α) (ha : a ∉ s) (IH : s.noncommProd f sorry = s.prod f),
  (cons a s ha).noncommProd f sorry = (cons a s ha).prod f
Tactic: induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s ha IH => simp [IH]
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s : Set α).Pairwise (Commute on f)
comm_gg : (↑s : Set α).Pairwise (Commute on g)
comm_gf : (↑s : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)
x : α
hx : x ∈ (↑s : Set α)
y : α
hy : y ∈ (↑s : Set α)
h : x ≠ y
⊢ Commute ((f * g) x) ((f * g) y)
have hac : Commute (f x) ((f * g) y)
Tactic: apply Commute.mul_left
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s : Set α).Pairwise (Commute on f)
comm_gg : (↑s : Set α).Pairwise (Commute on g)
comm_gf : (↑s : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)
x : α
hx : x ∈ (↑s : Set α)
y : α
hy : y ∈ (↑s : Set α)
h : x ≠ y
hac : Commute (f x) ((f * g) y)
⊢ Commute ((f * g) x) ((f * g) y)
have hbc : Commute (g x) ((f * g) y)
Tactic: apply Commute.mul_left
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s : Set α).Pairwise (Commute on f)
comm_gg : (↑s : Set α).Pairwise (Commute on g)
comm_gf : (↑s : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)
x : α
hx : x ∈ (↑s : Set α)
y : α
hy : y ∈ (↑s : Set α)
h : x ≠ y
⊢ Commute (f x) ((f * g) y)
have hac : Commute (f x) (f y)
Tactic: apply Commute.mul_right
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s : Set α).Pairwise (Commute on f)
comm_gg : (↑s : Set α).Pairwise (Commute on g)
comm_gf : (↑s : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)
x : α
hx : x ∈ (↑s : Set α)
y : α
hy : y ∈ (↑s : Set α)
h : x ≠ y
hac : Commute (f x) (f y)
⊢ Commute (f x) ((f * g) y)
have hac₁ : Commute (f x) (g y)
Tactic: apply Commute.mul_right
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s : Set α).Pairwise (Commute on f)
comm_gg : (↑s : Set α).Pairwise (Commute on g)
comm_gf : (↑s : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)
x : α
hx : x ∈ (↑s : Set α)
y : α
hy : y ∈ (↑s : Set α)
h : x ≠ y
⊢ Commute (g x) ((f * g) y)
have hbc : Commute (g x) (f y)
Tactic: apply Commute.mul_right
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s : Set α).Pairwise (Commute on f)
comm_gg : (↑s : Set α).Pairwise (Commute on g)
comm_gf : (↑s : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)
x : α
hx : x ∈ (↑s : Set α)
y : α
hy : y ∈ (↑s : Set α)
h : x ≠ y
hbc : Commute (g x) (f y)
⊢ Commute (g x) ((f * g) y)
have hbc₁ : Commute (g x) (g y)
Tactic: apply Commute.mul_right
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
f g : α → β
x : α
s : Finset α
hnotMem : x ∉ s
ih :
  ∀ (comm_ff : (↑s : Set α).Pairwise (Commute on f)) (comm_gg : (↑s : Set α).Pairwise (Commute on g))
    (comm_gf : (↑s : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)),
    s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
comm_ff : (↑(cons x s hnotMem) : Set α).Pairwise (Commute on f)
comm_gg : (↑(cons x s hnotMem) : Set α).Pairwise (Commute on g)
comm_gf : (↑(cons x s hnotMem) : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)
⊢ (cons x s hnotMem).noncommProd (f * g) ⋯ =
    (cons x s hnotMem).noncommProd f comm_ff * (cons x s hnotMem).noncommProd g comm_gg
have rw : ∀ (y : α) (hy : y ∈ s), Commute (g x) (f y)
Tactic: rw [Finset.noncommProd_cons, Finset.noncommProd_cons, Finset.noncommProd_cons, Pi.mul_apply,
      ih (comm_ff.mono fun _ => mem_cons_of_mem) (comm_gg.mono fun _ => mem_cons_of_mem)
        (comm_gf.mono fun _ => mem_cons_of_mem),
      (noncommProd_commute _ _ _ _ fun y hy => ?_).mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s : Set α).Pairwise (Commute on f)
comm_gg : (↑s : Set α).Pairwise (Commute on g)
comm_gf : (↑s : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)
⊢ s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
have empty : ∀ (comm_ff : (↑∅ : Set α).Pairwise (Commute on f)) (comm_gg : (↑∅ : Set α).Pairwise (Commute on g))
  (comm_gf : (↑∅ : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)),
  noncommProd ∅ (f * g) sorry = noncommProd ∅ f comm_ff * noncommProd ∅ g comm_gg
Tactic: induction s using Finset.cons_induction_on with
  | empty => simp
  | cons x s hnotMem ih =>
    rw [Finset.noncommProd_cons, Finset.noncommProd_cons, Finset.noncommProd_cons, Pi.mul_apply,
      ih (comm_ff.mono fun _ => mem_cons_of_mem) (comm_gg.mono fun _ => mem_cons_of_mem)
        (comm_gf.mono fun _ => mem_cons_of_mem),
      (noncommProd_commute _ _ _ _ fun y hy => ?_).mul_mul_mul_comm]
    exact comm_gf (mem_cons_self x s) (mem_cons_of_mem hy) (ne_of_mem_of_not_mem hy hnotMem).symm
Cleared hypotheses: s, comm_ff, comm_gg, comm_gf
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s : Set α).Pairwise (Commute on f)
comm_gg : (↑s : Set α).Pairwise (Commute on g)
comm_gf : (↑s : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)
empty :
  ∀ (comm_ff : (↑∅ : Set α).Pairwise (Commute on f)) (comm_gg : (↑∅ : Set α).Pairwise (Commute on g))
    (comm_gf : (↑∅ : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)),
    noncommProd ∅ (f * g) ⋯ = noncommProd ∅ f comm_ff * noncommProd ∅ g comm_gg
⊢ s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
have cons : ∀ (x : α) (s : Finset α) (hnotMem : x ∉ s)
  (ih :
    ∀ (comm_ff : (↑s : Set α).Pairwise (Commute on f)) (comm_gg : (↑s : Set α).Pairwise (Commute on g))
      (comm_gf : (↑s : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)),
      s.noncommProd (f * g) sorry = s.noncommProd f comm_ff * s.noncommProd g comm_gg)
  (comm_ff : (↑(cons x s hnotMem) : Set α).Pairwise (Commute on f))
  (comm_gg : (↑(cons x s hnotMem) : Set α).Pairwise (Commute on g))
  (comm_gf : (↑(cons x s hnotMem) : Set α).Pairwise fun (x y : α) ↦ Commute (g x) (f y)),
  (cons x s hnotMem).noncommProd (f * g) sorry =
    (cons x s hnotMem).noncommProd f comm_ff * (cons x s hnotMem).noncommProd g comm_gg
Tactic: induction s using Finset.cons_induction_on with
  | empty => simp
  | cons x s hnotMem ih =>
    rw [Finset.noncommProd_cons, Finset.noncommProd_cons, Finset.noncommProd_cons, Pi.mul_apply,
      ih (comm_ff.mono fun _ => mem_cons_of_mem) (comm_gg.mono fun _ => mem_cons_of_mem)
        (comm_gf.mono fun _ => mem_cons_of_mem),
      (noncommProd_commute _ _ _ _ fun y hy => ?_).mul_mul_mul_comm]
    exact comm_gf (mem_cons_self x s) (mem_cons_of_mem hy) (ne_of_mem_of_not_mem hy hnotMem).symm
Cleared hypotheses: s, comm_ff, comm_gg, comm_gf
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
⊢ noncommProd univ (fun (i : ι) ↦ Pi.mulSingle (M := M) i (x i)) ⋯ = x
have h : ∀ (i : ι), noncommProd univ (fun (i : ι) ↦ Pi.mulSingle (M := M) i (x i)) sorry i = x i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ noncommProd univ (fun (i : ι) ↦ Pi.mulSingle (M := M) i (x i)) ⋯ i = x i
have h : noncommProd univ
    (fun (i_1 : ι) ↦
      (Pi.evalMonoidHom M i : (a : (i : ι) → M i) → M i)
        (((MonoidHom.mulSingle M i_1 : M i_1 →* (i : ι) → M i) : (a : M i_1) → (i : ι) → M i) (x i_1)))
    sorry =
  x i
Tactic: apply (univ.map_noncommProd (fun i ↦ MonoidHom.mulSingle M i (x i)) ?a
    (Pi.evalMonoidHom M i)).trans
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i : ι
h :
  noncommProd univ
      (fun (i_1 : ι) ↦
        (Pi.evalMonoidHom M i : (a : (i : ι) → M i) → M i)
          (((MonoidHom.mulSingle M i_1 : M i_1 →* (i : ι) → M i) : (a : M i_1) → (i : ι) → M i) (x i_1)))
      ⋯ =
    x i
⊢ noncommProd univ (fun (i : ι) ↦ Pi.mulSingle (M := M) i (x i)) ⋯ i = x i
have apply : (↑univ : Set ι).Pairwise
  (Function.onFun (β := (i : ι) → M i) Commute fun (i : ι) ↦
    ((MonoidHom.mulSingle M i : M i →* (i : ι) → M i) : (a : M i) → (i : ι) → M i) (x i))
Tactic: apply (univ.map_noncommProd (fun i ↦ MonoidHom.mulSingle M i (x i)) ?a
    (Pi.evalMonoidHom M i)).trans
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ noncommProd univ
      (fun (i_1 : ι) ↦
        (Pi.evalMonoidHom M i : (a : (i : ι) → M i) → M i)
          (((MonoidHom.mulSingle M i_1 : M i_1 →* (i : ι) → M i) : (a : M i_1) → (i : ι) → M i) (x i_1)))
      ⋯ =
    x i
have h : ι → M i
Tactic: convert! (noncommProd_congr (insert_erase (mem_univ i)).symm _ _).trans _
-- Lean 4 proof step from Mathlib.Data.Finset.NoncommProd (goal)
Goal:
ι : Type u_2
M : ι → Type u_6
inst : (i : ι) → Monoid (M i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
x : (i : ι) → M i
i : ι
h : ι → M i
⊢ noncommProd univ
      (fun (i_1 : ι) ↦
        (Pi.evalMonoidHom M i : (a : (i : ι) → M i) → M i)
          (((MonoidHom.mulSingle M i_1 : M i_1 →* (i : ι) → M i) : (a : M i_1) → (i : ι) → M i) (x i_1)))
      ⋯ =
    x i
have h₁ : ∀ x_1 ∈ insert i (erase univ i),
  (Pi.evalMonoidHom M i : (a : (i : ι) → M i) → M i)
      (((MonoidHom.mulSingle M x_1 : M x_1 →* (i : ι) → M i) : (a : M x_1) → (i : ι) → M i) (x x_1)) =
    Pi.mulSingle (M := M) x_1 (x x_1) i
Tactic: convert! (noncommProd_congr (insert_erase (mem_univ i)).symm _ _).trans _