ι : Type ?u.992457
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : AddMonoid α
s : List α
⊢ List.sum s = List.prod s
ι : Type ?u.992457
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : AddMonoid α
s : List α
⊢ ↑ofAdd (List.sum s) = List.prod (List.map (↑ofAdd) s)
simp [ofAdd]
no goals
ι : Type ?u.992457
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : AddMonoid α
s : List α
⊢ List.sum s = List.prod s
rfl