case refine'_1
α : Type u_2
α' : Type ?u.2408961
β : Type u_3
β' : Type ?u.2408967
γ : Type ?u.2408970
E : Type ?u.2408973
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
L : Type u_1
inst✝ : IsROrC L
f : α → L
g : β → L
hf : Integrable f
hg : Integrable g
⊢ AEStronglyMeasurable (fun z => f z.fst * g z.snd) (Measure.prod μ ν)

case refine'_2
α : Type u_2
α' : Type ?u.2408961
β : Type u_3
β' : Type ?u.2408967
γ : Type ?u.2408970
E : Type ?u.2408973
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
L : Type u_1
inst✝ : IsROrC L
f : α → L
g : β → L
hf : Integrable f
hg : Integrable g
⊢ ∀ᵐ (x : α) ∂μ, Integrable fun y => f (x, y).fst * g (x, y).snd

case refine'_3
α : Type u_2
α' : Type ?u.2408961
β : Type u_3
β' : Type ?u.2408967
γ : Type ?u.2408970
E : Type ?u.2408973
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
L : Type u_1
inst✝ : IsROrC L
f : α → L
g : β → L
hf : Integrable f
hg : Integrable g
⊢ Integrable fun x => ∫ (y : β), ‖f (x, y).fst * g (x, y).snd‖ ∂ν
α : Type u_2
α' : Type ?u.2408961
β : Type u_3
β' : Type ?u.2408967
γ : Type ?u.2408970
E : Type ?u.2408973
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
L : Type u_1
inst✝ : IsROrC L
f : α → L
g : β → L
hf : Integrable f
hg : Integrable g
⊢ Integrable fun z => f z.fst * g z.snd
refine' (integrable_prod_iff _).2 ⟨_, _⟩
no goals
case refine'_1
α : Type u_2
α' : Type ?u.2408961
β : Type u_3
β' : Type ?u.2408967
γ : Type ?u.2408970
E : Type ?u.2408973
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
L : Type u_1
inst✝ : IsROrC L
f : α → L
g : β → L
hf : Integrable f
hg : Integrable g
⊢ AEStronglyMeasurable (fun z => f z.fst * g z.snd) (Measure.prod μ ν)
exact hf.1.fst.mul hg.1.snd
no goals
case refine'_2
α : Type u_2
α' : Type ?u.2408961
β : Type u_3
β' : Type ?u.2408967
γ : Type ?u.2408970
E : Type ?u.2408973
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
L : Type u_1
inst✝ : IsROrC L
f : α → L
g : β → L
hf : Integrable f
hg : Integrable g
⊢ ∀ᵐ (x : α) ∂μ, Integrable fun y => f (x, y).fst * g (x, y).snd
exact eventually_of_forall fun x => hg.const_mul (f x)
no goals
case refine'_3
α : Type u_2
α' : Type ?u.2408961
β : Type u_3
β' : Type ?u.2408967
γ : Type ?u.2408970
E : Type ?u.2408973
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace α'
inst✝⁵ : MeasurableSpace β
inst✝⁴ : MeasurableSpace β'
inst✝³ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝² : NormedAddCommGroup E
inst✝¹ : SigmaFinite ν
L : Type u_1
inst✝ : IsROrC L
f : α → L
g : β → L
hf : Integrable f
hg : Integrable g
⊢ Integrable fun x => ∫ (y : β), ‖f (x, y).fst * g (x, y).snd‖ ∂ν
simpa only [norm_mul, integral_mul_left] using hf.norm.mul_const _