F : Type ?u.140576
ι : Type ?u.140579
α : Type u_1
β : Type u_2
γ : Type ?u.140588
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
l : List α
f : α → β
comm : Set.Pairwise ↑(List.toFinset l) fun a b => Commute (f a) (f b)
hl✝ : List.Nodup l
hl : List.dedup l = l
⊢ noncommProd (List.toFinset l) f comm = List.prod (List.map f l)
F : Type ?u.140576
ι : Type ?u.140579
α : Type u_1
β : Type u_2
γ : Type ?u.140588
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
l : List α
f : α → β
comm : Set.Pairwise ↑(List.toFinset l) fun a b => Commute (f a) (f b)
hl : List.Nodup l
⊢ noncommProd (List.toFinset l) f comm = List.prod (List.map f l)
rw [← List.dedup_eq_self] at hl
no goals
F : Type ?u.140576
ι : Type ?u.140579
α : Type u_1
β : Type u_2
γ : Type ?u.140588
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid β
inst✝¹ : Monoid γ
inst✝ : DecidableEq α
l : List α
f : α → β
comm : Set.Pairwise ↑(List.toFinset l) fun a b => Commute (f a) (f b)
hl✝ : List.Nodup l
hl : List.dedup l = l
⊢ noncommProd (List.toFinset l) f comm = List.prod (List.map f l)
simp [noncommProd, hl]