Theorem: MeasureTheory.measureReal_prod_prod (Carleson/ToMathlib/MeasureReal.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
x✝ : MeasurableSpace α
inst✝¹ : MeasurableSpace β
μ✝ : Measure α
s✝ s₁ s₂ t✝ : Set α
μ : Measure α
ν : Measure β
inst✝ : SigmaFinite ν
s : Set α
t : Set β
⊢ (μ.prod ν).real (s ×ˢ t) = μ.real s * ν.real t
Tactic:
simp only [measureReal_def, prod_prod, ENNReal.toReal_mul]
State after:
no goals