-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem MeasureTheory.StronglyMeasurable.integral_prod_right [SFinite ν] ⦃f : α → β → E⦄
    (hf : StronglyMeasurable (uncurry f)) : StronglyMeasurable fun x => ∫ y, f x y ∂ν

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun n x => (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E := fun n => {x | Integrable (f x) ν}.indicator fun x => SimpleFunc.integral ν (s' n x)
n : ℕ
this : ∀ (x : α), Finset.filter (fun x => x ≠ 0) (s' n x).range ⊆ (s n).range
⊢ StronglyMeasurable fun x => ∑ x_1 ∈ (s n).range, (ν (⇑(s' n x) ⁻¹' {x_1})).toReal • x_1

Tactic:
refine Finset.stronglyMeasurable_sum _ fun x _ => ?_

Result:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun n x => (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E := fun n => {x | Integrable (f x) ν}.indicator fun x => SimpleFunc.integral ν (s' n x)
n : ℕ
this : ∀ (x : α), Finset.filter (fun x => x ≠ 0) (s' n x).range ⊆ (s n).range
x : E
x✝ : x ∈ (s n).range
⊢ StronglyMeasurable fun x_1 => (ν (⇑(s' n x_1) ⁻¹' {x})).toReal • x

Proof state:
case neg
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : ¬CompleteSpace E
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂ν

Tactic:
simp [integral, hE, stronglyMeasurable_const]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂ν

Tactic:
borelize E

Result:
case pos
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂ν

Proof state:
case pos
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun n x => (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E := fun n => {x | Integrable (f x) ν}.indicator fun x => SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
this : ∀ (n : ℕ), Integrable (⇑(s' n x)) ν
⊢ Tendsto (fun i => ∫ (x_1 : β), (s' i x) x_1 ∂ν) atTop (𝓝 (∫ (y : β), f x y ∂ν))

Tactic:
refine
  tendsto_integral_of_dominated_convergence (fun y => ‖f x y‖ + ‖f x y‖)
    (fun n => (s' n x).aestronglyMeasurable) (hfx.norm.add hfx.norm) ?_ ?_

Result:
case pos.refine_1
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun n x => (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E := fun n => {x | Integrable (f x) ν}.indicator fun x => SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
this : ∀ (n : ℕ), Integrable (⇑(s' n x)) ν
⊢ ∀ (n : ℕ), ∀ᵐ (a : β) ∂ν, ‖(s' n x) a‖ ≤ (fun y => ‖f x y‖ + ‖f x y‖) a

case pos.refine_2
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this✝² : MeasurableSpace E := borel E
this✝¹ : BorelSpace E
this✝ : SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun n x => (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E := fun n => {x | Integrable (f x) ν}.indicator fun x => SimpleFunc.integral ν (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
this : ∀ (n : ℕ), Integrable (⇑(s' n x)) ν
⊢ ∀ᵐ (a : β) ∂ν, Tendsto (fun n => (s' n x) a) atTop (𝓝 (f x a))

Proof state:
case pos
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun n x => (s n).comp (Prod.mk x) ⋯
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂ν

Tactic:
let f' : ℕ → α → E := fun n => {x | Integrable (f x) ν}.indicator fun x => (s' n x).integral ν

Result:
case pos
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSpace β
ν : Measure β
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range (uncurry f) ∪ {0})
s : ℕ → SimpleFunc (α × β) E := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → α → SimpleFunc β E := fun n x => (s n).comp (Prod.mk x) ⋯
f' : ℕ → α → E := fun n => {x | Integrable (f x) ν}.indicator fun x => SimpleFunc.integral ν (s' n x)
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂ν