case h
F : Type u_1
ι : Type ?u.95490
α : Type u_2
β : Type u_3
γ : Type ?u.95499
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
f : F
a✝ : List α
comm : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid α) a✝} Commute
⊢ ↑f (noncommProd (Quotient.mk (List.isSetoid α) a✝) comm) =
    noncommProd (map (↑f) (Quotient.mk (List.isSetoid α) a✝))
      (_ : Set.Pairwise {x | x ∈ map (↑f) (Quotient.mk (List.isSetoid α) a✝)} Commute)
F : Type u_1
ι : Type ?u.95490
α : Type u_2
β : Type u_3
γ : Type ?u.95499
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
s : Multiset α
comm : Set.Pairwise {x | x ∈ s} Commute
f : F
⊢ ↑f (noncommProd s comm) = noncommProd (map (↑f) s) (_ : Set.Pairwise {x | x ∈ map (↑f) s} Commute)
induction s using Quotient.inductionOn
no goals
case h
F : Type u_1
ι : Type ?u.95490
α : Type u_2
β : Type u_3
γ : Type ?u.95499
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
f : F
a✝ : List α
comm : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid α) a✝} Commute
⊢ ↑f (noncommProd (Quotient.mk (List.isSetoid α) a✝) comm) =
    noncommProd (map (↑f) (Quotient.mk (List.isSetoid α) a✝))
      (_ : Set.Pairwise {x | x ∈ map (↑f) (Quotient.mk (List.isSetoid α) a✝)} Commute)
simpa using map_list_prod f _