data.prod

Stream: mathlib4

[Patrick Massot]

While searching who to blame for names I just found out we have https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/Prod.lean which is a version of what should be data.prod.basic. So we probably also need a script hunting down files that exist in mathlib4 but not in mathlib (outside the tactic folder of course)

[Mario Carneiro]

There shouldn't be too many of these, we're trying to adhere to the convention that mathlib4 mimics mathlib file positioning, but I guess this predates that

[Mario Carneiro]

But you will find a fair number of files that have almost nothing in them because most theorems that were in the file have been moved to lean4 or std4