Fintype.sum of Fintype.sum

Stream: Is there code for X?

[David Renshaw]

import Mathlib.Tactic
import Mathlib.Data.Fintype.BigOperators

open BigOperators

lemma sum_of_sum {α β : Type} [Fintype α] [Fintype β]
    (f : α → β → ℤ) :
    ∑ a : α, ∑ b : β, f a b = ∑ ab : α × β, f.uncurry ab := by sorry

[David Renshaw]

Anyone have any ideas about how to prove this? Seems like there ought to be some existing lemma.

[Yaël Dillies]

This is exactly docs#Finset.sum_product'

[David Renshaw]

nice!

[David Renshaw]

I should have tried rw? first

[David Renshaw]

(Finset.sum_product' is among the suggestions given by rw?, but not among the top 10)

[Yaël Dillies]

Sadly, yael? is only available on Zulip :grinning:

[Henrik Böving]

Maybe we can train an LLM on the corpus of Yael Q&A's ...