-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
α : Type u_2
f : α → E
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
hm : m ≤ mα
hφ_cvx : ConvexOn ℝ s φ
hφ_cont : LowerSemicontinuousOn φ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hs : IsClosed s
hf_int : Integrable f μ
hφ_int : Integrable (φ ∘ f) μ
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
φY : ↥Y → ℝ := φ ∘ (⇑Y.subtypeL : (a : ↥Y) → E)
let let₁ let₂ let₃ : φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]
let₄ : ∀ (lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y), φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]
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), φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]
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) (hfY_int : Integrable fY μ),
    φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]
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) (hfY_int : Integrable fY μ)
    (lem2 : μ[f | m] =ᶠ[ae μ] (⇑Y.subtypeL : (a : ↥Y) → E) ∘ μ[fY | m]), φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]
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) (hfY_int : Integrable fY μ)
    (lem2 : μ[f | m] =ᶠ[ae μ] (⇑Y.subtypeL : (a : ↥Y) → E) ∘ μ[fY | m]) (lem3 : φ ∘ f =ᶠ[ae μ] φY ∘ fY),
    φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]
⊢ φ ∘ μ[f | m] ≤ᶠ[ae μ] μ[φ ∘ f | m]

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 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 lem2 : μ[f | m] =ᵐ[μ] Y.subtypeL ∘ μ[fY | m] := calc
    _ =ᵐ[μ] μ[fX | m] := condExp_congr_ae lem1
    _ =ᵐ[μ] _ := (Y.subtypeL.comp_condExp_comm hfY_int).symm
  have lem3 : φ ∘ f =ᵐ[μ] φY ∘ fY := by filter_upwards [lem1] with a ha; simp [φY, ha, fX]
  calc
    φ ∘ μ[f | m]
      =ᵐ[μ] φY ∘ μ[fY | m] := by filter_upwards [lem2] with a ha; simp [φY, ha]
    _ ≤ᵐ[μ] μ[φY ∘ fY | m] := by
      refine (hφ_cvx.comp_linearMap Y.subtype).map_condExp_le_of_hereditarilyLindelofSpace
        (s := Y.subtypeL ⁻¹' s) hm ?_ ?_ ?_ hfY_int (Integrable.congr hφ_int lem3)
      · exact hφ_cont.comp (by fun_prop) fun x => by
          #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
          (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
          goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem
          in the new canonicalizer; a minimization would help. The original proof was: `grind` -/
          simp
      · filter_upwards [lem0, hf] with a ha hb
        simp_all [fY]
      · exact hs.preimage Y.subtypeL.continuous
    _ =ᵐ[μ] μ[φ ∘ f | m] := condExp_congr_ae lem3.symm