no goals
ι : Type ?u.887074
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g : α → β
M : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
x✝ : Nodup []
⊢ Finset.prod (toFinset []) f = prod (map f [])
simp
ι : Type ?u.887074
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
M : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
a : α
l : List α
hl✝ : Nodup (a :: l)
not_mem : ¬a ∈ l
hl : Nodup l
⊢ Finset.prod (toFinset (a :: l)) f = prod (map f (a :: l))
ι : Type ?u.887074
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
M : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
a : α
l : List α
hl : Nodup (a :: l)
⊢ Finset.prod (toFinset (a :: l)) f = prod (map f (a :: l))
let ⟨not_mem, hl⟩ := List.nodup_cons.mp hl
no goals
ι : Type ?u.887074
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a✝ : α
f✝ g : α → β
M : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
f : α → M
a : α
l : List α
hl✝ : Nodup (a :: l)
not_mem : ¬a ∈ l
hl : Nodup l
⊢ Finset.prod (toFinset (a :: l)) f = prod (map f (a :: l))
simp [Finset.prod_insert (mt List.mem_toFinset.mp not_mem), prod_toFinset _ hl]