-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : SFinite ν
f : α → β → E
hf : StronglyMeasurable (uncurry f)
pos : ∀ (hE : CompleteSpace E), StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
neg : ∀ (hE : ¬CompleteSpace E), StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
pos₁ : ∀ (hE : CompleteSpace E), StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
neg₁ neg₂ : ∀ (hE : ¬CompleteSpace E), StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
pos₂ : ∀ (hE : CompleteSpace E), StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
neg₃ : ∀ (hE : ¬CompleteSpace E), StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
pos₃ pos₄ : ∀ (hE : CompleteSpace E), StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
pos₅ :
  ∀ (hE : CompleteSpace E),
    let this := borel E;
    BorelSpace E → StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
pos₆ pos₇ pos₈ pos₉ :
  ∀ (hE : CompleteSpace E),
    let this := borel E;
    BorelSpace E →
      ∀ (this : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)),
        StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
pos₁₀ :
  ∀ (hE : CompleteSpace E),
    let this := borel E;
    ∀ (this_1 : BorelSpace E) (this_2 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)),
      let s := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯;
      let s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯;
      let f' : ℕ → α → E := fun (n : ℕ) ↦
        indicator {x : α | Integrable (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x);
      ∀ (hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)),
        StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
pos₁₁ :
  ∀ (hE : CompleteSpace E),
    let this := borel E;
    ∀ (this_1 : BorelSpace E) (this_2 : SeparableSpace.{u_3} (↑(range (uncurry f) ∪ {0}) : Type u_3)),
      let s := SimpleFunc.approxOn (uncurry f) ⋯ (range (uncurry f) ∪ {0}) 0 ⋯;
      let s' : ℕ → α → SimpleFunc β E := fun (n : ℕ) (x : α) ↦ (s n).comp (Prod.mk x) ⋯;
      let f' : ℕ → α → E := fun (n : ℕ) ↦
        indicator {x : α | Integrable (f x) ν} fun (x : α) ↦ SimpleFunc.integral ν (s' n x);
      ∀ (hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)) (h2f' : Tendsto f' atTop (𝓝 fun (x : α) ↦ ∫ (y : β), f x y ∂ν)),
        StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν
⊢ StronglyMeasurable.{u_1, u_3} (β := E) fun (x : α) ↦ ∫ (y : β), f x y ∂ν

Tactic:
classical
  by_cases hE : CompleteSpace E; swap; · simp [integral, hE, stronglyMeasurable_const]
  borelize E
  haveI : SeparableSpace (range (uncurry f) ∪ {0} : Set E) :=
    hf.separableSpace_range_union_singleton
  let s : ℕ → SimpleFunc (α × β) E :=
    SimpleFunc.approxOn _ hf.measurable (range (uncurry f) ∪ {0}) 0 (by simp)
  let s' : ℕ → α → SimpleFunc β E := fun n x => (s n).comp (Prod.mk x) measurable_prodMk_left
  let f' : ℕ → α → E := fun n => {x | Integrable (f x) ν}.indicator fun x => (s' n x).integral ν
  have hf' : ∀ n, StronglyMeasurable (f' n) := by
    intro n; refine StronglyMeasurable.indicator ?_ (measurableSet_integrable hf)
    have : ∀ x, ((s' n x).range.filter fun x => x ≠ 0) ⊆ (s n).range := by
      intro x; refine Finset.Subset.trans (Finset.filter_subset _ _) ?_; intro y
      simp_rw [SimpleFunc.mem_range]; rintro ⟨z, rfl⟩; exact ⟨(x, z), rfl⟩
    simp only [SimpleFunc.integral_eq_sum_of_subset (this _)]
    refine Finset.stronglyMeasurable_fun_sum _ fun x _ => ?_
    refine (Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _
    simp only [s', SimpleFunc.coe_comp, preimage_comp]
    apply measurable_measure_prodMk_left
    exact (s n).measurableSet_fiber x
  have h2f' : Tendsto f' atTop (𝓝 fun x : α => ∫ y : β, f x y ∂ν) := by
    rw [tendsto_pi_nhds]; intro x
    by_cases hfx : Integrable (f x) ν
    · have (n : _) : Integrable (s' n x) ν := by
        apply (hfx.norm.add hfx.norm).mono' (s' n x).aestronglyMeasurable
        filter_upwards with y
        simp_rw [s', SimpleFunc.coe_comp]; exact SimpleFunc.norm_approxOn_zero_le _ _ (x, y) n
      simp only [f', hfx, SimpleFunc.integral_eq_integral _ (this _), indicator_of_mem,
        mem_setOf_eq]
      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) ?_ ?_
      · refine fun n => Eventually.of_forall fun y =>
          SimpleFunc.norm_approxOn_zero_le ?_ ?_ (x, y) n
        · exact hf.measurable
        · simp
      · refine Eventually.of_forall fun y => SimpleFunc.tendsto_approxOn ?_ ?_ ?_
        · exact hf.measurable.of_uncurry_left
        · simp
        apply subset_closure
        simp [-uncurry_apply_pair]
    · simp [f', hfx, integral_undef]
  exact stronglyMeasurable_of_tendsto _ hf' h2f'

Premises used: MeasureTheory.stronglyMeasurable_const, CompleteSpace, MeasureTheory.integral