case h
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
⊢ noncommProd (a ::ₘ Quotient.mk (List.isSetoid α) s) comm =
    noncommProd (Quotient.mk (List.isSetoid α) s) (_ : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid α) s} Commute) *
      a
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s : Multiset α
a : α
comm : Set.Pairwise {x | x ∈ a ::ₘ s} Commute
⊢ noncommProd (a ::ₘ s) comm = noncommProd s (_ : Set.Pairwise {x | x ∈ s} Commute) * a
induction' s using Quotient.inductionOn with s
case h
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
⊢ a * List.prod s = List.prod s * a
case h
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
⊢ noncommProd (a ::ₘ Quotient.mk (List.isSetoid α) s) comm =
    noncommProd (Quotient.mk (List.isSetoid α) s) (_ : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid α) s} Commute) *
      a
simp only [quot_mk_to_coe, cons_coe, noncommProd_coe, List.prod_cons]
case h.nil
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) []} Commute
⊢ a * List.prod [] = List.prod [] * a

case h.cons
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
⊢ a * List.prod (hd :: tl) = List.prod (hd :: tl) * a
case h
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
⊢ a * List.prod s = List.prod s * a
induction' s with hd tl IH
no goals
case h.nil
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) []} Commute
⊢ a * List.prod [] = List.prod [] * a
simp
case h.cons
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
⊢ a * hd * List.prod tl = hd * a * List.prod tl

case h.cons
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
⊢ Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute
case h.cons
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
⊢ a * List.prod (hd :: tl) = List.prod (hd :: tl) * a
rw [List.prod_cons, mul_assoc, ← IH, ← mul_assoc, ← mul_assoc]
case h.cons.e_a
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
⊢ a * hd = hd * a
case h.cons
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
⊢ a * hd * List.prod tl = hd * a * List.prod tl
congr 1
no goals
case h.cons.e_a
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
⊢ a * hd = hd * a
apply comm.of_refl <;> simp
case h.cons
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
x : α
hx : x ∈ {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl}
y : α
hy : y ∈ {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl}
⊢ x ≠ y → Commute x y
case h.cons
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
⊢ Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute
intro x hx y hy
case h.cons
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ x ≠ y → Commute x y
case h.cons
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
x : α
hx : x ∈ {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl}
y : α
hy : y ∈ {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl}
⊢ x ≠ y → Commute x y
simp only [quot_mk_to_coe, List.mem_cons, mem_coe, cons_coe] at hx hy
case h.cons.a
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ x ∈ {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)}

case h.cons.a
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ y ∈ {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)}
case h.cons
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ x ≠ y → Commute x y
apply comm
no goals
case h.cons.a
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ x ∈ {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)}
cases hx <;> simp [*]
no goals
case h.cons.a
F : Type ?u.11255
ι : Type ?u.11258
α : Type u_1
β : Type ?u.11264
γ : Type ?u.11267
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s✝ : Multiset α
a : α
comm✝¹ : Set.Pairwise {x | x ∈ a ::ₘ s✝} Commute
s : List α
comm✝ : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) s} Commute
hd : α
tl : List α
IH : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) tl} Commute → a * List.prod tl = List.prod tl * a
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)} Commute
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ y ∈ {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) (hd :: tl)}
cases hy <;> simp [*]