-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := Submodule.topologicalClosure (Submodule.span ℝ t)
this_3 : CompleteSpace.{u_1} ↥Y
this : SecondCountableTopology.{u_1} ↥Y
let let₁ let₂ let₃ : ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
let₄ : ∀ (lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y), ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
let₅ :
  let fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0;
  let fX : α → E := (⇑Y.subtypeL : (a : ↥Y) → E) ∘ fY;
  ∀ (lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y) (lem1 : f =ᶠ[ae μ] fX), ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
let₆ :
  let fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0;
  let fX : α → E := (⇑Y.subtypeL : (a : ↥Y) → E) ∘ fY;
  ∀ (lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y) (lem1 : f =ᶠ[ae μ] fX)
    (lem2 : ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set ↥Y) ((⇑Y.subtypeL : (a : ↥Y) → E) ⁻¹' s) (fY a)),
    ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
let₇ :
  let fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0;
  let fX : α → E := (⇑Y.subtypeL : (a : ↥Y) → E) ∘ fY;
  ∀ (lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y) (lem1 : f =ᶠ[ae μ] fX)
    (lem2 : ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set ↥Y) ((⇑Y.subtypeL : (a : ↥Y) → E) ⁻¹' s) (fY a))
    (hfY_int : Integrable fY μ), ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
have let₈ : let fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0;
let fX : α → E := (⇑Y.subtypeL : (a : ↥Y) → E) ∘ fY;
∀ (lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y) (lem1 : f =ᶠ[ae μ] fX)
  (lem2 : ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set ↥Y) ((⇑Y.subtypeL : (a : ↥Y) → E) ⁻¹' s) (fY a))
  (hfY_int : Integrable fY μ) (lem3 : μ[f | m] =ᶠ[ae μ] (⇑Y.subtypeL : (a : ↥Y) → E) ∘ μ[fY | m]),
  ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
Tactic: classical
  let fY : α → Y := fun a => if h : f a ∈ Y then ⟨f a, h⟩ else 0
  let fX : α → E := Y.subtypeL ∘ fY
  have lem0 : ∀ᵐ a ∂μ, f a ∈ Y := by
    filter_upwards [htt] with a ha using
      (Submodule.closure_subset_topologicalClosure_span t) (subset_closure ha)
  have lem1 : f =ᵐ[μ] fX := by
    filter_upwards [lem0] with a ha
    simp_all [fX, fY]
  have lem2 : ∀ᵐ a ∂μ, fY a ∈ Y.subtypeL ⁻¹' s := by
    filter_upwards [lem0, hf] with a ha hs
    simpa [fY, ha]
  have hfY_int : Integrable fY μ := by
    refine (hf_int.congr lem1).mono ?_ (by simp [fX])
    obtain ⟨g, hg1, hg2, hg3⟩ := hf_int.1.exists_stronglyMeasurable_range_subset
      ((Submodule.isClosed_topologicalClosure _).measurableSet) Nonempty.of_subtype lem0
    refine ⟨codRestrict g Y hg2, (hg1.measurable.codRestrict hg2).stronglyMeasurable, ?_⟩
    filter_upwards [hg3] with a ha
    have : g a ∈ Y := hg2 a
    simp_all [fY, codRestrict]
  have lem3 : μ[f | m] =ᵐ[μ] Y.subtypeL ∘ μ[fY | m] := calc
    _ =ᵐ[μ] μ[fX | m] := condExp_congr_ae lem1
    _ =ᵐ[μ] _ := (Y.subtypeL.comp_condExp_comm hfY_int).symm
  filter_upwards [(hc.linear_preimage Y.subtype).condExp_mem_of_hereditarilyLindelofSpace
    hm hfY_int (hs.preimage Y.subtypeL.continuous) lem2, lem3] with a ha hb
  simp_all