case h.e'_2.h.e'_2.h.a
F : Type ?u.142925
ι : Type ?u.142928
α : Type u_1
β : Type u_2
γ : Type ?u.142937
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : Set.Pairwise ↑(insert a s) fun a b => Commute (f a) (f b)
ha : ¬a ∈ s
x✝ : β
⊢ x✝ ∈ f a ::ₘ Multiset.map f s.val ↔ x✝ ∈ Multiset.map f (insert a s).val
F : Type ?u.142925
ι : Type ?u.142928
α : Type u_1
β : Type u_2
γ : Type ?u.142937
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : Set.Pairwise ↑(insert a s) fun a b => Commute (f a) (f b)
ha : ¬a ∈ s
⊢ Set.Pairwise {x | x ∈ f a ::ₘ Multiset.map f s.val} Commute
convert noncommProd_lemma _ f comm using 3
no goals
case h.e'_2.h.e'_2.h.a
F : Type ?u.142925
ι : Type ?u.142928
α : Type u_1
β : Type u_2
γ : Type ?u.142937
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : Set.Pairwise ↑(insert a s) fun a b => Commute (f a) (f b)
ha : ¬a ∈ s
x✝ : β
⊢ x✝ ∈ f a ::ₘ Multiset.map f s.val ↔ x✝ ∈ Multiset.map f (insert a s).val
simp [@eq_comm _ (f a)]
no goals
F : Type ?u.142925
ι : Type ?u.142928
α : Type u_1
β : Type u_2
γ : Type ?u.142937
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : Set.Pairwise ↑(insert a s) fun a b => Commute (f a) (f b)
ha : ¬a ∈ s
⊢ Multiset.noncommProd (f a ::ₘ Multiset.map f s.val)
      (_ : Set.Pairwise {x | x ∈ f a ::ₘ Multiset.map f s.val} Commute) =
    f a * noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b))
rw [Multiset.noncommProd_cons, noncommProd]