-- Lean 4 proof step from Mathlib.Probability.Kernel.MeasurableIntegral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
pos :
  ∀ (hE : CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
neg :
  ∀ (hE : ¬CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
pos₁ :
  ∀ (hE : CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
neg₁ neg₂ :
  ∀ (hE : ¬CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
pos₂ pos₃ :
  ∀ (hE : CompleteSpace E),
    StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
      @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
pos₄ :
  ∀ (hE : CompleteSpace E),
    let this := borel E;
    BorelSpace E →
      StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
        @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
pos₅ pos₆ pos₇ :
  ∀ (hE : CompleteSpace E),
    let this := borel E;
    BorelSpace E →
      ∀ (this : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)),
        StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
          @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
pos₈ :
  ∀ (hE : CompleteSpace E),
    let this := borel E;
    ∀ (this_1 : BorelSpace E) (this_2 : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)),
      let s := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯;
      let f' : (n : ℕ) → α → E := fun (n : ℕ) ↦
        indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
          SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n);
      ∀ (n : ℕ), StronglyMeasurable (f' n)
⊢ StronglyMeasurable.{u_1, u_4} (β := E) fun (x : α) ↦
    @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y
have pos₉ : ∀ (hE : CompleteSpace E),
  let this := borel E;
  ∀ (this_1 : BorelSpace E) (this_2 : TopologicalSpace.SeparableSpace.{u_4} (↑(range f ∪ {0}) : Type u_4)),
    let s := SimpleFunc.approxOn f sorry (range f ∪ {0}) 0 sorry;
    let f' : (n : ℕ) → α → E := fun (n : ℕ) ↦
      indicator {x : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) x)} fun (x : α) ↦
        SimpleFunc.integral ((κ : (a : α) → Measure β) x) (s n);
    Tendsto f' atTop (𝓝 fun (x : α) ↦ @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) x) fun (y : β) ↦ f y)
Tactic: classical
  by_cases hE : CompleteSpace E; swap
  · simp [integral, hE, stronglyMeasurable_const]
  borelize E
  have : TopologicalSpace.SeparableSpace (range f ∪ {0} : Set E) :=
    hf.separableSpace_range_union_singleton
  let s : ℕ → SimpleFunc β E := SimpleFunc.approxOn _ hf.measurable (range f ∪ {0}) 0 (by simp)
  let f' n : α → E := {x | Integrable f (κ x)}.indicator fun x ↦ (s n).integral (κ x)
  refine stronglyMeasurable_of_tendsto (f := f') atTop (fun n ↦ ?_) ?_
  · refine StronglyMeasurable.indicator ?_ (measurableSet_integrable hf)
    simp_rw [SimpleFunc.integral_eq]
    refine Finset.stronglyMeasurable_fun_sum _ fun _ _ ↦ ?_
    refine (Measurable.ennreal_toReal ?_).stronglyMeasurable.smul_const _
    exact κ.measurable_coe ((s n).measurableSet_fiber _)
  · rw [tendsto_pi_nhds]; intro x
    by_cases hfx : Integrable f (κ x)
    · simp only [mem_setOf_eq, hfx, indicator_of_mem, f']
      apply tendsto_integral_approxOn_of_measurable_of_range_subset _ hfx
      exact subset_rfl
    · simp [f', hfx, integral_undef]