Fix 2013 A5

[GeorgeTsoukalas]

Re: Joseph Myer's description of the issue

I think current PutnamBench still has the 2013 A5 problem discussed above (2-dimensional Hausdorff measure in Fin 3 → ℝ does not correspond to any standard notion of area). If you used EuclideanSpace ℝ (Fin 3) you still wouldn't have area (we still need a definition / API in mathlib for a version of Hausdorff measure that's appropriately scaled for the Euclidean metric), but you would at least have area scaled by some positive constant (so be clearly-to-humans equivalent to the original problem in this case, where scaling the area doesn't actually matter to the statement).

[GeorgeTsoukalas]

This also affects 2019 A4 which uses the Hausdorff measure to do a surface integral in R^3.

[GeorgeTsoukalas]

Resolved by #348