awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : ∀ b ∈ s.erase a, Commute a b
rw : a * (s.erase a).noncommProd comm' = s.noncommProd comm
rw₁ rw₂ : s.noncommProd comm = s.noncommProd comm
⊢ (s.erase a).noncommProd comm' * a = s.noncommProd comm

Tactic:
rw [← (noncommProd_commute (s.erase a) comm' a this).eq, mul_noncommProd_erase s h comm comm']

Premises used: Multiset.noncommProd_commute, Multiset.mul_noncommProd_erase, Multiset.erase, Commute.eq
-- 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
suffices : ∀ b ∈ s.erase a, Commute a b
⊢ (s.erase a).noncommProd comm' * a = s.noncommProd comm

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']
-- 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
b : α
hb : b ∈ s.erase a
inl : ∀ (hb : a ∈ s.erase a), Commute a a
inr : ∀ (hab : a ≠ b), Commute a b
⊢ Commute a b

Tactic:
rcases eq_or_ne a b with rfl | hab

Premises used: eq_or_ne, rfl
-- 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
hb : a ∈ s.erase a
⊢ Commute a a

Tactic:
rfl
-- 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
b : α
hb : b ∈ s.erase a
hab : a ≠ b
⊢ Commute a b

Tactic:
comm h (mem_of_mem_erase hb) hab

Premises used: Multiset.mem_of_mem_erase
-- 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
b : α
hb : b ∈ s.erase a
hab : a ≠ b
⊢ Commute a b

Tactic:
exact comm h (mem_of_mem_erase hb) hab

Premises used: Multiset.mem_of_mem_erase
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
s : Finset α
f : α → β
comm : (↑s : Set α).Pairwise (Commute on f)
⊢ Set.Pairwise.{u_4} (α := β) {x : β | x ∈ Multiset.map f s.val} Commute

Tactic:
Multiset.map_set_pairwise comm

Premises used: Multiset.map_set_pairwise
-- Module: Mathlib.Data.Finset.NoncommProd
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)

Tactic:
Multiset.noncommProd_induction _ _ _ hom unit fun b hb ↦ ?_

Premises used: Multiset.noncommProd_induction, Finset.noncommProd
-- Module: Mathlib.Data.Finset.NoncommProd
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)
refine : ∀ (b : β) (hb : b ∈ Multiset.map f s.val), p b
⊢ p (s.noncommProd f comm)

Tactic:
refine Multiset.noncommProd_induction _ _ _ hom unit fun b hb ↦ ?_

Premises used: Multiset.noncommProd_induction
-- Module: Mathlib.Data.Finset.NoncommProd
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
⊢ ∃ a ∈ s, f a = b

Tactic:
simpa using hb
-- Module: Mathlib.Data.Finset.NoncommProd
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
obtain : ∀ (a : α) (ha : a ∈ s) (hb : f a ∈ Multiset.map f s.val), p (f a)
⊢ p b

Tactic:
obtain (⟨a, ha : a ∈ s, rfl : f a = b⟩) := by simpa using hb

Premises used: rfl
-- Module: Mathlib.Data.Finset.NoncommProd
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)
a : α
ha : a ∈ s
hb : f a ∈ Multiset.map f s.val
⊢ p (f a)

Tactic:
base a ha
-- Module: Mathlib.Data.Finset.NoncommProd
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)
a : α
ha : a ∈ s
hb : f a ∈ Multiset.map f s.val
⊢ p (f a)

Tactic:
exact base a ha
-- Module: Mathlib.Data.Finset.NoncommProd
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
rw : Commute (f x) (f y)
⊢ Commute (g x) (g y)

Tactic:
rw [← h₂ _ hx, ← h₂ _ hy]
-- Module: Mathlib.Data.Finset.NoncommProd
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
⊢ ∀ x ∈ s₁, f x = g x

Tactic:
subst h₁
-- Module: Mathlib.Data.Finset.NoncommProd
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
⊢ x ∈ (↑s₁ : Set α)

Tactic:
subst h₁
-- Module: Mathlib.Data.Finset.NoncommProd
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 α)
⊢ y ∈ (↑s₁ : Set α)

Tactic:
subst h₁
-- Module: Mathlib.Data.Finset.NoncommProd
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₁ : Finset α
f g : α → β
comm : (↑s₁ : Set α).Pairwise (Commute on f)
x y : α
h : x ≠ y
h₂ : ∀ x ∈ s₁, f x = g x
hx : x ∈ (↑s₁ : Set α)
hy : y ∈ (↑s₁ : Set α)
⊢ Commute (f x) (f y)

Tactic:
comm hx hy h
-- Module: Mathlib.Data.Finset.NoncommProd
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₁ : Finset α
f g : α → β
comm : (↑s₁ : Set α).Pairwise (Commute on f)
x y : α
h : x ≠ y
h₂ : ∀ x ∈ s₁, f x = g x
hx : x ∈ (↑s₁ : Set α)
hy : y ∈ (↑s₁ : Set α)
⊢ Commute (f x) (f y)

Tactic:
exact comm hx hy h
-- Module: Mathlib.Data.Finset.NoncommProd
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.dedup = l

Tactic:
rw [← List.dedup_eq_self] at hl

Premises used: List.dedup_eq_self
-- Module: Mathlib.Data.Finset.NoncommProd
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.dedup = l
⊢ l.toFinset.noncommProd f comm = (List.map f l).prod

Tactic:
simp [noncommProd, hl]

Premises used: Finset.noncommProd
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
f : α → β
h : (↑∅ : Set α).Pairwise (Commute on f)
⊢ noncommProd ∅ f h = 1

Tactic:
rfl

Premises used: Multiset.foldr, Multiset.map, Multiset.noncommFoldr, Multiset.noncommFold, Finset.noncommProd, Multiset.ofList, List.foldr, rfl, Multiset.noncommProd
-- Module: Mathlib.Data.Finset.NoncommProd
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 ⋯
simp_rw₂ : (f a ::ₘ Multiset.map f s.val).noncommProd ⋯ = f a * (Multiset.map f s.val).noncommProd ⋯
⊢ (cons a s ha).noncommProd f comm = f a * s.noncommProd f ⋯

Tactic:
simp_rw [noncommProd, Finset.cons_val, Multiset.map_cons, Multiset.noncommProd_cons]

Premises used: Multiset.map_cons, Finset.cons_val, Finset.noncommProd, Multiset.noncommProd_cons
-- Module: Mathlib.Data.Finset.NoncommProd
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
simp_rw₂ : (f a ::ₘ Multiset.map f s.val).noncommProd ⋯ = (Multiset.map f s.val).noncommProd ⋯ * f a
⊢ (cons a s ha).noncommProd f comm = s.noncommProd f ⋯ * f a

Tactic:
simp_rw [noncommProd, Finset.cons_val, Multiset.map_cons, Multiset.noncommProd_cons']

Premises used: Multiset.map_cons, Finset.cons_val, Finset.noncommProd, Multiset.noncommProd_cons'
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
inst_1 : DecidableEq α
s : Finset α
a : α
f : α → β
comm : (↑(insert a s) : Set α).Pairwise (Commute on f)
ha : a ∉ s
⊢ (insert a s).noncommProd f comm = f a * s.noncommProd f ⋯

Tactic:
simp only [← cons_eq_insert _ _ ha, noncommProd_cons]

Premises used: Finset.cons_eq_insert, Finset.noncommProd_cons
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
inst_1 : DecidableEq α
s : Finset α
a : α
f : α → β
comm : (↑(insert a s) : Set α).Pairwise (Commute on f)
ha : a ∉ s
⊢ (insert a s).noncommProd f comm = s.noncommProd f ⋯ * f a

Tactic:
simp only [← cons_eq_insert _ _ ha, noncommProd_cons']

Premises used: Finset.noncommProd_cons', Finset.cons_eq_insert
-- Module: Mathlib.Data.Finset.NoncommProd
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 : α → β
norm_cast : Set.Pairwise {a} (Commute on f)
⊢ (↑{a} : Set α).Pairwise (Commute on f)

Tactic:
norm_cast
-- Module: Mathlib.Data.Finset.NoncommProd
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 : α → β
⊢ Set.Pairwise {a} (Commute on f)

Tactic:
Set.pairwise_singleton _ _

Premises used: Set.pairwise_singleton
-- Module: Mathlib.Data.Finset.NoncommProd
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 : α → β
⊢ Set.Pairwise {a} (Commute on f)

Tactic:
exact Set.pairwise_singleton _ _

Premises used: Set.pairwise_singleton
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
a : α
f : α → β
⊢ noncommProd {a} f ⋯ = f a

Tactic:
mul_one _

Premises used: Multiset.foldr, Multiset.map, Multiset.noncommFoldr, Multiset.noncommFold, Finset.noncommProd, Multiset.ofList, mul_one, List.foldr, Multiset.noncommProd
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
F : Type u_1
α : Type u_3
β : Type u_4
γ : Type u_5
inst : Monoid β
inst_1 : Monoid γ
inst_2 : FunLike F β γ
inst_3 : MonoidHomClass F β γ
s : Finset α
f : α → β
comm : (↑s : Set α).Pairwise (Commute on f)
g : F
⊢ Eq.{u_5 + 1} (α := γ) ((g : (a : β) → γ) (s.noncommProd f comm) : γ)
    (s.noncommProd (fun (i : α) ↦ (g : (a : β) → γ) (f i)) ⋯ : γ)

Tactic:
simp [noncommProd, Multiset.map_noncommProd]

Premises used: Multiset.map_noncommProd, Finset.noncommProd
-- Module: Mathlib.Data.Finset.NoncommProd
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
rw₁ : ∀ x ∈ Multiset.map f s.val, x = m
⊢ s.noncommProd f comm = m ^ #s

Tactic:
rw [noncommProd, Multiset.noncommProd_eq_pow_card _ _ m]

Premises used: Finset.noncommProd, Multiset.noncommProd_eq_pow_card
-- Module: Mathlib.Data.Finset.NoncommProd
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
⊢ m ^ (Multiset.map f s.val).card = m ^ #s

Tactic:
simp only [Finset.card_def, Multiset.card_map]

Premises used: Finset.card_def, Multiset.card_map
-- Module: Mathlib.Data.Finset.NoncommProd
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
⊢ ∀ x ∈ Multiset.map f s.val, x = m

Tactic:
simpa using h
-- Module: Mathlib.Data.Finset.NoncommProd
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)
h₁ : ∀ x ∈ Multiset.map f s.val, Commute y x
⊢ Commute y (s.noncommProd f comm)

Tactic:
apply Multiset.noncommProd_commute

Premises used: Multiset.noncommProd_commute
-- Module: Mathlib.Data.Finset.NoncommProd
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 : β
h₁ : (∃ a ∈ s.val, f a = y) → Commute y_1 y
⊢ y ∈ Multiset.map f s.val → Commute y_1 y

Tactic:
rw [Multiset.mem_map]

Premises used: Multiset.mem_map
-- Module: Mathlib.Data.Finset.NoncommProd
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)
x : α
hx : x ∈ s.val
⊢ Commute y (f x)

Tactic:
h x hx
-- Module: Mathlib.Data.Finset.NoncommProd
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)
x : α
hx : x ∈ s.val
⊢ Commute y (f x)

Tactic:
exact h x hx
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
inst_1 : DecidableEq α
s : Finset α
a : α
h : a ∈ s
f : α → β
comm : (↑s : Set α).Pairwise (Commute on f)
comm' :
  ∀ (x : α) (hx : x ∈ (↑(s.erase a) : Set α)) (x_1 : α) (hy : x_1 ∈ (↑(s.erase a) : Set α)) (hxy : x ≠ x_1),
    (Commute on f) x x_1
⊢ f a * (s.erase a).noncommProd f comm' = s.noncommProd f comm

Tactic:
simpa only [← Multiset.map_erase_of_mem _ _ h] using
    Multiset.mul_noncommProd_erase (s.1.map f) (Multiset.mem_map_of_mem f h) _

Premises used: Multiset.map, Multiset.mem_map_of_mem, Multiset.mul_noncommProd_erase, Finset.val, Multiset.map_erase_of_mem, Multiset.mem_of_mem_erase
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
inst_1 : DecidableEq α
s : Finset α
a : α
h : a ∈ s
f : α → β
comm : (↑s : Set α).Pairwise (Commute on f)
comm' :
  ∀ (x : α) (hx : x ∈ (↑(s.erase a) : Set α)) (x_1 : α) (hy : x_1 ∈ (↑(s.erase a) : Set α)) (hxy : x ≠ x_1),
    (Commute on f) x x_1
⊢ f a * (s.erase a).noncommProd f comm' = s.noncommProd f comm

Tactic:
classical
  simpa only [← Multiset.map_erase_of_mem _ _ h] using
    Multiset.mul_noncommProd_erase (s.1.map f) (Multiset.mem_map_of_mem f h) _

Premises used: Multiset.map_erase_of_mem
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
inst_1 : DecidableEq α
s : Finset α
a : α
h : a ∈ s
f : α → β
comm : (↑s : Set α).Pairwise (Commute on f)
comm' :
  ∀ (x : α) (hx : x ∈ (↑(s.erase a) : Set α)) (x_1 : α) (hy : x_1 ∈ (↑(s.erase a) : Set α)) (hxy : x ≠ x_1),
    (Commute on f) x x_1
⊢ (s.erase a).noncommProd f comm' * f a = s.noncommProd f comm

Tactic:
simpa only [← Multiset.map_erase_of_mem _ _ h] using
    Multiset.noncommProd_erase_mul (s.1.map f) (Multiset.mem_map_of_mem f h) _

Premises used: Multiset.noncommProd_erase_mul, Multiset.map, Multiset.mem_map_of_mem, Finset.val, Multiset.map_erase_of_mem, Multiset.mem_of_mem_erase
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_4
inst : Monoid β
inst_1 : DecidableEq α
s : Finset α
a : α
h : a ∈ s
f : α → β
comm : (↑s : Set α).Pairwise (Commute on f)
comm' :
  ∀ (x : α) (hx : x ∈ (↑(s.erase a) : Set α)) (x_1 : α) (hy : x_1 ∈ (↑(s.erase a) : Set α)) (hxy : x ≠ x_1),
    (Commute on f) x x_1
⊢ (s.erase a).noncommProd f comm' * f a = s.noncommProd f comm

Tactic:
classical
  simpa only [← Multiset.map_erase_of_mem _ _ h] using
    Multiset.noncommProd_erase_mul (s.1.map f) (Multiset.mem_map_of_mem f h) _

Premises used: Multiset.map_erase_of_mem
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_6
inst : CommMonoid β
f : α → β
⊢ noncommProd ∅ f ⋯ = Finset.prod ∅ f

Tactic:
simp
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_6
inst : CommMonoid β
f : α → β
a : α
s : Finset α
ha : a ∉ s
IH : s.noncommProd f ⋯ = s.prod f
⊢ (cons a s ha).noncommProd f ⋯ = (cons a s ha).prod f

Tactic:
simp [IH]
-- Module: Mathlib.Data.Finset.NoncommProd
Goal:
α : Type u_3
β : Type u_6
inst : CommMonoid β
s : Finset α
f : α → β
empty : noncommProd ∅ f ⋯ = Finset.prod ∅ f
cons :
  ∀ (a : α) (s : Finset α) (ha : a ∉ s) (IH : s.noncommProd f ⋯ = s.prod f),
    (Finset.cons a s ha).noncommProd f ⋯ = (Finset.cons a s ha).prod f
⊢ s.noncommProd f ⋯ = s.prod f

Tactic:
induction s using Finset.cons_induction_on with
  | empty => simp
  | cons a s ha IH => simp [IH]

Premises used: Finset.cons
-- Module: Mathlib.Data.Finset.NoncommProd
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)
hbc : Commute (g x) ((f * g) y)
⊢ Commute ((f * g) x) ((f * g) y)

Tactic:
apply Commute.mul_left

Premises used: Commute.mul_left
-- Module: Mathlib.Data.Finset.NoncommProd
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)
hac₁ : Commute (f x) (g y)
⊢ Commute (f x) ((f * g) y)

Tactic:
apply Commute.mul_right

Premises used: Commute.mul_right
-- Module: Mathlib.Data.Finset.NoncommProd
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)
hbc₁ : Commute (g x) (g y)
⊢ Commute (g x) ((f * g) y)

Tactic:
apply Commute.mul_right

Premises used: Commute.mul_right
-- Module: Mathlib.Data.Finset.NoncommProd
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 y)

Tactic:
comm_ff.of_refl hx hy

Premises used: Set.Pairwise.of_refl
-- Module: Mathlib.Data.Finset.NoncommProd
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 y)

Tactic:
exact comm_ff.of_refl hx hy

Premises used: Set.Pairwise.of_refl
-- Module: Mathlib.Data.Finset.NoncommProd
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) (g y)

Tactic:
(comm_gf hy hx h.symm).symm

Premises used: Ne.symm, Commute.symm
-- Module: Mathlib.Data.Finset.NoncommProd
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) (g y)

Tactic:
exact (comm_gf hy hx h.symm).symm

Premises used: Ne.symm, Commute.symm
-- Module: Mathlib.Data.Finset.NoncommProd
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 y)

Tactic:
comm_gf hx hy h
-- Module: Mathlib.Data.Finset.NoncommProd
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 y)

Tactic:
exact comm_gf hx hy h
-- Module: Mathlib.Data.Finset.NoncommProd
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) (g y)

Tactic:
comm_gg.of_refl hx hy

Premises used: Set.Pairwise.of_refl
-- Module: Mathlib.Data.Finset.NoncommProd
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) (g y)

Tactic:
exact comm_gg.of_refl hx hy

Premises used: Set.Pairwise.of_refl