-- 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:
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)
h2f' : Tendsto f' atTop (𝓝 fun x => ∫ (y : β), f x y ∂ν)
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂ν

Tactic:
exact stronglyMeasurable_of_tendsto _ hf' h2f'

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 ∂ν

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:
swap

Result:
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 ∂ν

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 ∂ν

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)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
n : ℕ
⊢ Integrable (⇑(s' n x)) ν

Tactic:
apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable

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)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : α
hfx : Integrable (f x) ν
n : ℕ
⊢ ∀ᵐ (a : β) ∂ν, ‖(s' n x) a‖ ≤ ((fun a => ‖f x a‖) + fun a => ‖f x a‖) 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
⊢ StronglyMeasurable fun x => ∫ (y : β), f x y ∂ν

Tactic:
haveI : SeparableSpace (range (uncurry f) ∪ {0} : Set E) :=
  hf.separableSpace_range_union_singleton

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})
⊢ 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 => SimpleFunc.integral ν (s' n x)

Tactic:
simp only [SimpleFunc.integral_eq_sum_of_subset (this _)]

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
⊢ StronglyMeasurable fun x => ∑ x_1 ∈ (s n).range, (ν (⇑(s' n x) ⁻¹' {x_1})).toReal • x_1