case mk
F : Type ?u.83828
ι : Type ?u.83831
α : Type u_1
β : Type ?u.83837
γ : Type ?u.83840
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s t : Multiset α
a✝ : List α
comm : Set.Pairwise {x | x ∈ Quot.mk Setoid.r a✝ + t} Commute
⊢ noncommProd (Quot.mk Setoid.r a✝ + t) comm =
    noncommProd (Quot.mk Setoid.r a✝) (_ : Set.Pairwise {x | x ∈ Quot.mk Setoid.r a✝} Commute) *
      noncommProd t (_ : Set.Pairwise {x | x ∈ t} Commute)
F : Type ?u.83828
ι : Type ?u.83831
α : Type u_1
β : Type ?u.83837
γ : Type ?u.83840
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s t : Multiset α
comm : Set.Pairwise {x | x ∈ s + t} Commute
⊢ noncommProd (s + t) comm =
    noncommProd s (_ : Set.Pairwise {x | x ∈ s} Commute) * noncommProd t (_ : Set.Pairwise {x | x ∈ t} Commute)
rcases s with ⟨⟩
case mk.mk
F : Type ?u.83828
ι : Type ?u.83831
α : Type u_1
β : Type ?u.83837
γ : Type ?u.83840
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s t : Multiset α
a✝¹ a✝ : List α
comm : Set.Pairwise {x | x ∈ Quot.mk Setoid.r a✝¹ + Quot.mk Setoid.r a✝} Commute
⊢ noncommProd (Quot.mk Setoid.r a✝¹ + Quot.mk Setoid.r a✝) comm =
    noncommProd (Quot.mk Setoid.r a✝¹) (_ : Set.Pairwise {x | x ∈ Quot.mk Setoid.r a✝¹} Commute) *
      noncommProd (Quot.mk Setoid.r a✝) (_ : Set.Pairwise {x | x ∈ Quot.mk Setoid.r a✝} Commute)
case mk
F : Type ?u.83828
ι : Type ?u.83831
α : Type u_1
β : Type ?u.83837
γ : Type ?u.83840
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s t : Multiset α
a✝ : List α
comm : Set.Pairwise {x | x ∈ Quot.mk Setoid.r a✝ + t} Commute
⊢ noncommProd (Quot.mk Setoid.r a✝ + t) comm =
    noncommProd (Quot.mk Setoid.r a✝) (_ : Set.Pairwise {x | x ∈ Quot.mk Setoid.r a✝} Commute) *
      noncommProd t (_ : Set.Pairwise {x | x ∈ t} Commute)
rcases t with ⟨⟩
no goals
case mk.mk
F : Type ?u.83828
ι : Type ?u.83831
α : Type u_1
β : Type ?u.83837
γ : Type ?u.83840
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s t : Multiset α
a✝¹ a✝ : List α
comm : Set.Pairwise {x | x ∈ Quot.mk Setoid.r a✝¹ + Quot.mk Setoid.r a✝} Commute
⊢ noncommProd (Quot.mk Setoid.r a✝¹ + Quot.mk Setoid.r a✝) comm =
    noncommProd (Quot.mk Setoid.r a✝¹) (_ : Set.Pairwise {x | x ∈ Quot.mk Setoid.r a✝¹} Commute) *
      noncommProd (Quot.mk Setoid.r a✝) (_ : Set.Pairwise {x | x ∈ Quot.mk Setoid.r a✝} Commute)
simp