awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
h : Set.Pairwise.{u_3} (α := α) {x : α | Membership.mem (γ := Multiset α) 0 x} Commute
⊢ noncommProd 0 h = 1

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.noncommFoldr, Multiset.zero, Multiset.noncommFold, Multiset.ofList, List.foldr, rfl, Multiset.noncommProd
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
s : Multiset α
a : α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ s} Commute
h :
  ∀ (a_1 : List α) (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦a_1⟧} Commute),
    (a ::ₘ ⟦a_1⟧).noncommProd comm = a * noncommProd ⟦a_1⟧ ⋯
⊢ (a ::ₘ s).noncommProd comm = a * s.noncommProd ⋯

Tactic:
induction s using Quotient.inductionOn
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
a : α
a_1 : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦a_1⟧} Commute
⊢ (a ::ₘ ⟦a_1⟧).noncommProd comm = a * noncommProd ⟦a_1⟧ ⋯

Tactic:
simp
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
s : Multiset α
a : α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ s} Commute
h :
  ∀ (s : List α) (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦s⟧} Commute),
    (a ::ₘ ⟦s⟧).noncommProd comm = noncommProd ⟦s⟧ ⋯ * a
⊢ (a ::ₘ s).noncommProd comm = s.noncommProd ⋯ * a

Tactic:
induction s using Quotient.inductionOn with | _ s
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
a : α
s : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦s⟧} Commute
h : a * s.prod = s.prod * a
⊢ (a ::ₘ ⟦s⟧).noncommProd comm = noncommProd ⟦s⟧ ⋯ * a

Tactic:
simp only [quot_mk_to_coe, cons_coe, noncommProd_coe, List.prod_cons]

Premises used: Multiset.noncommProd_coe, Multiset.quot_mk_to_coe, Multiset.cons_coe, List.prod_cons
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
a : α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦[]⟧} Commute
⊢ a * List.prod [] = List.prod [] * a

Tactic:
simp
-- Module: Mathlib.Data.Finset.NoncommProd
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
h₁ : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ a ::ₘ ⟦tl⟧} Commute
⊢ a * (hd :: tl).prod = (hd :: tl).prod * a

Tactic:
rw [List.prod_cons, mul_assoc, ← IH, ← mul_assoc, ← mul_assoc]

Premises used: mul_assoc, List.prod_cons
-- Module: Mathlib.Data.Finset.NoncommProd
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 = hd * a
⊢ a * hd * tl.prod = hd * a * tl.prod

Tactic:
congr 1
-- Module: Mathlib.Data.Finset.NoncommProd
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
h₁ : Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} hd
⊢ a * hd = hd * a

Tactic:
apply comm.of_refl

Premises used: Set.Pairwise.of_refl
-- Module: Mathlib.Data.Finset.NoncommProd
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
⊢ Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} a

Tactic:
simp
-- Module: Mathlib.Data.Finset.NoncommProd
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
⊢ Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} hd

Tactic:
simp
-- Module: Mathlib.Data.Finset.NoncommProd
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
⊢ 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

Premises used: Multiset.mem_coe, Multiset.quot_mk_to_coe, Multiset.cons_coe, List.mem_cons
-- Module: Mathlib.Data.Finset.NoncommProd
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
⊢ 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

Premises used: Multiset.mem_coe, Multiset.quot_mk_to_coe, Multiset.cons_coe, List.mem_cons
-- Module: Mathlib.Data.Finset.NoncommProd
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
h₁ : Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} y
⊢ x ≠ y → Commute x y

Tactic:
apply comm
-- Module: Mathlib.Data.Finset.NoncommProd
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
h₁ : x ∈ tl → Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} x
⊢ Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} x

Tactic:
cases hx
-- Module: Mathlib.Data.Finset.NoncommProd
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 : α
hy : Membership.mem (γ := Set α) {x : α | x = a ∨ x ∈ tl} y
h : x = a
⊢ Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} x

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.NoncommProd
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 : α
hy : Membership.mem (γ := Set α) {x : α | x = a ∨ x ∈ tl} y
h : x ∈ tl
⊢ Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} x

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.NoncommProd
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
h₁ : y ∈ tl → Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} y
⊢ Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} y

Tactic:
cases hy
-- Module: Mathlib.Data.Finset.NoncommProd
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
h : y = a
⊢ Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} y

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.NoncommProd
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
h : y ∈ tl
⊢ Membership.mem (γ := Set α) {x : α | x ∈ a ::ₘ ⟦hd :: tl⟧} y

Tactic:
simp [*]
-- Module: Mathlib.Data.Finset.NoncommProd
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
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
⊢ a * s.prod = s.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 [*]

Premises used: Multiset.mem_coe, mul_assoc, Multiset.quot_mk_to_coe, Multiset.cons, Set.Pairwise.of_refl, Multiset.cons_coe, List.mem_cons, List.prod_cons
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
s t : Multiset α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ s + t} Commute
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) ⋯ * t.noncommProd ⋯
⊢ (s + t).noncommProd comm = s.noncommProd ⋯ * t.noncommProd ⋯

Tactic:
rcases s with ⟨⟩
-- Module: Mathlib.Data.Finset.NoncommProd
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
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) ⋯ *
        noncommProd (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a_1) ⋯
⊢ (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a + t).noncommProd comm =
    noncommProd (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a) ⋯ * t.noncommProd ⋯

Tactic:
rcases t with ⟨⟩
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
s t : Multiset α
a 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) ⋯ *
      noncommProd (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) a_1) ⋯

Tactic:
simp
-- Module: Mathlib.Data.Finset.NoncommProd
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
h :
  ∀ (l : List α) (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ ⟦l⟧} Commute) (base : ∀ x ∈ ⟦l⟧, p x),
    p (noncommProd ⟦l⟧ comm)
⊢ p (s.noncommProd comm)

Tactic:
induction s using Quotient.inductionOn with | _ l
-- Module: Mathlib.Data.Finset.NoncommProd
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
h : ∀ (base : ∀ x ∈ l, p x), p l.prod
⊢ p (noncommProd ⟦l⟧ comm)

Tactic:
simp only [quot_mk_to_coe, noncommProd_coe, mem_coe] at base ⊢

Premises used: Multiset.mem_coe, Multiset.noncommProd_coe, Multiset.quot_mk_to_coe
-- Module: Mathlib.Data.Finset.NoncommProd
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 l.prod

Tactic:
l.prod_induction p hom unit base

Premises used: List.prod_induction
-- Module: Mathlib.Data.Finset.NoncommProd
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 l.prod

Tactic:
exact l.prod_induction p hom unit base

Premises used: List.prod_induction
-- Module: Mathlib.Data.Finset.NoncommProd
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
simp : Set.Pairwise.{u_4} (α := β) {x : β | ∃ a ∈ s, (f : (a : α) → β) a = x} Commute
⊢ Set.Pairwise.{u_4} (α := β) {x : β | Membership.mem (γ := Multiset β) (map (⇑f : (a : α) → β) s) x} Commute

Tactic:
simp only [Multiset.mem_map]

Premises used: Multiset.mem_map
-- Module: Mathlib.Data.Finset.NoncommProd
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
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : Ne.{u_4 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)
⊢ Commute.{u_4} (S := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
(comm.of_refl hx hy).map f

Premises used: Set.Pairwise.of_refl, Commute.map
-- Module: Mathlib.Data.Finset.NoncommProd
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
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : Ne.{u_4 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)
⊢ Commute.{u_4} (S := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
exact (comm.of_refl hx hy).map f

Premises used: Set.Pairwise.of_refl, Commute.map
-- Module: Mathlib.Data.Finset.NoncommProd
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
h :
  ∀ (a : List α) (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ ⟦a⟧} Commute),
    (f : (a : α) → β) (noncommProd ⟦a⟧ comm) = noncommProd (map (⇑f : (a : α) → β) ⟦a⟧) ⋯
⊢ (f : (a : α) → β) (s.noncommProd comm) = noncommProd (map (⇑f : (a : α) → β) s) ⋯

Tactic:
induction s using Quotient.inductionOn
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
F : Type u_1
α : Type u_3
β : Type u_4
inst : Monoid α
inst_1 : Monoid β
inst_2 : FunLike F α β
inst_3 : MonoidHomClass F α β
f : F
a : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ ⟦a⟧} Commute
⊢ (f : (a : α) → β) (noncommProd ⟦a⟧ comm) = noncommProd (map (⇑f : (a : α) → β) ⟦a⟧) ⋯

Tactic:
simpa using map_list_prod f _

Premises used: map_list_prod
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
s : Multiset α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ s} Commute
m : α
h : ∀ x ∈ s, x = m
h₁ :
  ∀ (a : List α) (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ ⟦a⟧} Commute) (h : ∀ x ∈ ⟦a⟧, x = m),
    noncommProd ⟦a⟧ comm = m ^ card ⟦a⟧
⊢ s.noncommProd comm = m ^ s.card

Tactic:
induction s using Quotient.inductionOn
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
m : α
a : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ ⟦a⟧} Commute
h : ∀ x ∈ ⟦a⟧, x = m
h₁ : ∀ (h : ∀ x ∈ a, x = m), a.prod = m ^ a.length
⊢ noncommProd ⟦a⟧ comm = m ^ card ⟦a⟧

Tactic:
simp only [quot_mk_to_coe, noncommProd_coe, coe_card, mem_coe] at *

Premises used: Multiset.mem_coe, Multiset.noncommProd_coe, Multiset.quot_mk_to_coe, Multiset.coe_card
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
m : α
a : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ ⟦a⟧} Commute
h : ∀ x ∈ a, x = m
⊢ a.prod = m ^ a.length

Tactic:
List.prod_eq_pow_card _ m h

Premises used: List.prod_eq_pow_card
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
m : α
a : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ ⟦a⟧} Commute
h : ∀ x ∈ a, x = m
⊢ a.prod = m ^ a.length

Tactic:
exact List.prod_eq_pow_card _ m h

Premises used: List.prod_eq_pow_card
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_6
inst : CommMonoid α
s : Multiset α
h : ∀ (a : List α), noncommProd ⟦a⟧ ⋯ = prod ⟦a⟧
⊢ s.noncommProd ⋯ = s.prod

Tactic:
induction s using Quotient.inductionOn
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_6
inst : CommMonoid α
a : List α
⊢ noncommProd ⟦a⟧ ⋯ = prod ⟦a⟧

Tactic:
simp
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
s : Multiset α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ s} Commute
y : α
h : ∀ x ∈ s, Commute y x
h₁ :
  ∀ (a : List α) (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ ⟦a⟧} Commute) (h : ∀ x ∈ ⟦a⟧, Commute y x),
    Commute y (noncommProd ⟦a⟧ comm)
⊢ Commute y (s.noncommProd comm)

Tactic:
induction s using Quotient.inductionOn
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
inst : Monoid α
y : α
a : List α
comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ ⟦a⟧} Commute
h : ∀ x ∈ ⟦a⟧, Commute y x
h₁ : Commute y a.prod
⊢ Commute y (noncommProd ⟦a⟧ comm)

Tactic:
simp only [quot_mk_to_coe, noncommProd_coe]

Premises used: Multiset.noncommProd_coe, Multiset.quot_mk_to_coe
-- Module: Mathlib.Data.Finset.NoncommProd
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 a.prod

Tactic:
Commute.list_prod_right _ _ h

Premises used: Commute.list_prod_right
-- Module: Mathlib.Data.Finset.NoncommProd
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 a.prod

Tactic:
exact Commute.list_prod_right _ _ h

Premises used: Commute.list_prod_right
-- Module: Mathlib.Data.Finset.NoncommProd
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
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
⊢ a * (s.erase a).noncommProd comm' = s.noncommProd comm

Tactic:
induction s using Quotient.inductionOn with | _ l
-- Module: Mathlib.Data.Finset.NoncommProd
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
h₁ : ∀ (comm : Set.Pairwise.{u_3} (α := α) {x : α | x ∈ l} Commute) (h : a ∈ l), a * (l.erase a).prod = l.prod
⊢ a * (erase ⟦l⟧ a).noncommProd comm' = noncommProd ⟦l⟧ comm

Tactic:
simp only [quot_mk_to_coe, mem_coe, coe_erase, noncommProd_coe] at comm h ⊢

Premises used: Multiset.mem_coe, Multiset.noncommProd_coe, Multiset.quot_mk_to_coe, Multiset.coe_erase
-- Module: Mathlib.Data.Finset.NoncommProd
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
rw rw₁ : l.prod = l.prod
⊢ a * (l.erase a).prod = l.prod

Tactic:
rw [List.prod_erase_of_comm h this]

Premises used: List.prod_erase_of_comm
-- Module: Mathlib.Data.Finset.NoncommProd
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
h₁ : ∀ x ∈ l, ∀ y ∈ l, x * y = y * x
⊢ a * (l.erase a).prod = l.prod

Tactic:
suffices ∀ x ∈ l, ∀ y ∈ l, x * y = y * x by rw [List.prod_erase_of_comm h this]
-- Module: Mathlib.Data.Finset.NoncommProd
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
h₂ : ∀ (hxy : x ≠ y), x * y = y * x
⊢ x * y = y * x

Tactic:
rcases eq_or_ne x y with rfl | hxy

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Finset.NoncommProd
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 hy : x ∈ l
⊢ x * x = x * x

Tactic:
rfl
-- Module: Mathlib.Data.Finset.NoncommProd
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
hxy : x ≠ y
⊢ x * y = y * x

Tactic:
comm hx hy hxy

Premises used: SemiconjBy, Commute
-- Module: Mathlib.Data.Finset.NoncommProd
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
hxy : x ≠ y
⊢ x * y = y * x

Tactic:
exact comm hx hy hxy