-- Mathlib/Data/Finset/NoncommProd.lean
theorem mul_noncommProd_erase [DecidableEq α] (s : Multiset α) {a : α} (h : a ∈ s) (comm)
    (comm' := fun _ hx _ hy hxy ↦ comm (s.mem_of_mem_erase hx) (s.mem_of_mem_erase hy) hxy) :
    a * (s.erase a).noncommProd comm' = s.noncommProd comm

Proof state:
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm✝ : {x | x ∈ ⟦l⟧}.Pairwise Commute
comm' : optParam (∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1) ⋯
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
this : ∀ x ∈ l, ∀ y ∈ l, x * y = y * x
⊢ a * (l.erase a).prod = l.prod

Tactic:
rw [List.prod_erase_of_comm h this]

Result:
no goals

Proof state:
case h
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm✝ : {x | x ∈ ⟦l⟧}.Pairwise Commute
comm' : optParam (∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1) ⋯
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
⊢ ∀ x ∈ l, ∀ y ∈ l, x * y = y * x

Tactic:
intro x hx y hy

Result:
case h
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm✝ : {x | x ∈ ⟦l⟧}.Pairwise Commute
comm' : optParam (∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1) ⋯
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
x : α
hx : x ∈ l
y : α
hy : y ∈ l
⊢ x * y = y * x

Proof state:
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : optParam (∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1) ⋯
⊢ a * (s.erase a).noncommProd comm' = s.noncommProd comm

Tactic:
induction' s using Quotient.inductionOn with l

Result:
case h
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ ⟦l⟧
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
comm' : optParam (∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1) ⋯
⊢ a * (erase ⟦l⟧ a).noncommProd comm' = noncommProd ⟦l⟧ comm

Proof state:
case h
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm✝ : {x | x ∈ ⟦l⟧}.Pairwise Commute
comm' : optParam (∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1) ⋯
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
⊢ 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]

Result:
case h
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm✝ : {x | x ∈ ⟦l⟧}.Pairwise Commute
comm' : optParam (∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1) ⋯
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
⊢ ∀ x ∈ l, ∀ y ∈ l, x * y = y * x

Proof state:
case h
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ ⟦l⟧
comm : {x | x ∈ ⟦l⟧}.Pairwise Commute
comm' : optParam (∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1) ⋯
⊢ 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 ⊢

Result:
case h
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm✝ : {x | x ∈ ⟦l⟧}.Pairwise Commute
comm' : optParam (∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1) ⋯
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
⊢ a * (l.erase a).prod = l.prod

Proof state:
case h.inl
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm✝ : {x | x ∈ ⟦l⟧}.Pairwise Commute
comm' : optParam (∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1) ⋯
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
x : α
hx hy : x ∈ l
⊢ x * x = x * x

Tactic:
rfl

Result:
no goals

Proof state:
case h.inr
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm✝ : {x | x ∈ ⟦l⟧}.Pairwise Commute
comm' : optParam (∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1) ⋯
comm : {x | x ∈ l}.Pairwise 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

Result:
no goals

Proof state:
case h
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm✝ : {x | x ∈ ⟦l⟧}.Pairwise Commute
comm' : optParam (∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1) ⋯
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
x : α
hx : x ∈ l
y : α
hy : y ∈ l
⊢ x * y = y * x

Tactic:
rcases eq_or_ne x y with rfl | hxy

Result:
case h.inl
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm✝ : {x | x ∈ ⟦l⟧}.Pairwise Commute
comm' : optParam (∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1) ⋯
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
x : α
hx hy : x ∈ l
⊢ x * x = x * x

case h.inr
α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
a : α
l : List α
comm✝ : {x | x ∈ ⟦l⟧}.Pairwise Commute
comm' : optParam (∀ x ∈ {x | x ∈ erase ⟦l⟧ a}, ∀ x_1 ∈ {x | x ∈ erase ⟦l⟧ a}, x ≠ x_1 → Commute x x_1) ⋯
comm : {x | x ∈ l}.Pairwise Commute
h : a ∈ l
x : α
hx : x ∈ l
y : α
hy : y ∈ l
hxy : x ≠ y
⊢ x * y = y * x