convert hf.integrable
case hf
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SigmaFinite μ
f : α → β → E
s : Set α
t : Set β
hf : IntegrableOn (Function.uncurry f) (s ×ˢ t) (μ.prod ν)
⊢ Integrable (Function.uncurry fun x y => f x y) ((μ.restrict s).prod (ν.restrict t))
case h.e'_6
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SigmaFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SigmaFinite μ
f : α → β → E
s : Set α
t : Set β
hf : IntegrableOn (Function.uncurry f) (s ×ˢ t) (μ.prod ν)
⊢ (μ.restrict s).prod (ν.restrict t) = (μ.prod ν).restrict (s ×ˢ t)