no goals
α : Type u_1
α' : Type ?u.2396048
β : Type u_2
β' : Type ?u.2396054
γ : Type ?u.2396057
E : Type u_3
inst✝⁶ : MeasurableSpace α
inst✝⁵ : MeasurableSpace α'
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace β'
inst✝² : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝¹ : NormedAddCommGroup E
inst✝ : SigmaFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (Measure.prod μ ν)
⊢ Integrable f ↔ (∀ᵐ (x : α) ∂μ, Integrable fun y => f (x, y)) ∧ Integrable fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν
simp [Integrable, h1f, hasFiniteIntegral_prod_iff', h1f.norm.integral_prod_right',
  h1f.prod_mk_left]