-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem Integrable.prod_smul {𝕜 : Type*} [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E]
    {f : α → 𝕜} {g : β → E} (hf : Integrable f μ) (hg : Integrable g ν) :
    Integrable (fun z : α × β => f z.1 • g z.2) (μ.prod ν)

Proof state:
case refine_1
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
𝕜 : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hf : Integrable f μ
hg : Integrable g ν
⊢ AEStronglyMeasurable (fun z => f z.1 • g z.2) (μ.prod ν)

Tactic:
exact hf.1.fst.smul hg.1.snd

Result:
no goals

Proof state:
case refine_3
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
𝕜 : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hf : Integrable f μ
hg : Integrable g ν
⊢ Integrable (fun x => ∫ (y : β), ‖f (x, y).1 • g (x, y).2‖ ∂ν) μ

Tactic:
simpa only [norm_smul, integral_mul_left] using hf.norm.mul_const _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
𝕜 : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hf : Integrable f μ
hg : Integrable g ν
⊢ Integrable (fun z => f z.1 • g z.2) (μ.prod ν)

Tactic:
refine (integrable_prod_iff ?_).2 ⟨?_, ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
𝕜 : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hf : Integrable f μ
hg : Integrable g ν
⊢ AEStronglyMeasurable (fun z => f z.1 • g z.2) (μ.prod ν)

case refine_2
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
𝕜 : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hf : Integrable f μ
hg : Integrable g ν
⊢ ∀ᵐ (x : α) ∂μ, Integrable (fun y => f (x, y).1 • g (x, y).2) ν

case refine_3
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
𝕜 : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hf : Integrable f μ
hg : Integrable g ν
⊢ Integrable (fun x => ∫ (y : β), ‖f (x, y).1 • g (x, y).2‖ ∂ν) μ

Proof state:
case refine_2
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
𝕜 : Type u_4
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
f : α → 𝕜
g : β → E
hf : Integrable f μ
hg : Integrable g ν
⊢ ∀ᵐ (x : α) ∂μ, Integrable (fun y => f (x, y).1 • g (x, y).2) ν

Tactic:
exact Eventually.of_forall fun x => hg.smul (f x)

Result:
no goals