Lemmas re-exported from Mathlib (formerly PR33029)

The instances about IsUnifLocDoublingMeasure on products and pi-types that this file used to define have since been upstreamed to Mathlib. This module re-exports them via the relevant Mathlib imports so existing import sites continue to resolve.