Lemmas from https://github.com/leanprover-community/mathlib4/pull/32986

instance IsLocallyFiniteMeasure.prod {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace X] [MeasurableSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) [MeasureTheory.IsLocallyFiniteMeasure μ] [MeasureTheory.IsLocallyFiniteMeasure ν] : MeasureTheory.IsLocallyFiniteMeasure (μ.prod ν)