case h
F : Type ?u.10023
ι : Type ?u.10026
α : Type u_1
β : Type ?u.10032
γ : Type ?u.10035
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
a : α
a✝ : List α
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) a✝} Commute
⊢ noncommProd (a ::ₘ Quotient.mk (List.isSetoid α) a✝) comm =
    a *
      noncommProd (Quotient.mk (List.isSetoid α) a✝)
        (_ : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid α) a✝} Commute)
F : Type ?u.10023
ι : Type ?u.10026
α : Type u_1
β : Type ?u.10032
γ : Type ?u.10035
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
s : Multiset α
a : α
comm : Set.Pairwise {x | x ∈ a ::ₘ s} Commute
⊢ noncommProd (a ::ₘ s) comm = a * noncommProd s (_ : Set.Pairwise {x | x ∈ s} Commute)
induction s using Quotient.inductionOn
no goals
case h
F : Type ?u.10023
ι : Type ?u.10026
α : Type u_1
β : Type ?u.10032
γ : Type ?u.10035
f : α → β → β
op : α → α → α
inst✝¹ : Monoid α
inst✝ : Monoid β
a : α
a✝ : List α
comm : Set.Pairwise {x | x ∈ a ::ₘ Quotient.mk (List.isSetoid α) a✝} Commute
⊢ noncommProd (a ::ₘ Quotient.mk (List.isSetoid α) a✝) comm =
    a *
      noncommProd (Quotient.mk (List.isSetoid α) a✝)
        (_ : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid α) a✝} Commute)
simp