awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0
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)
g : α → E
hg1 : StronglyMeasurable g
hg2 : ∀ (x : α), g x ∈ (↑(Submodule.topologicalClosure (Submodule.span ℝ t)) : Set E)
hg3 : f =ᶠ[ae μ] g
⊢ fY =ᶠ[ae μ] codRestrict g (↑Y : Set E) hg2
have h : ∀ (a : α) (ha : f a = g a), fY a = codRestrict g (↑Y : Set E) hg2 a
Tactic: filter_upwards [hg3] with a ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (hypothesis)
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
fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0
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)
g : α → E
hg1 : StronglyMeasurable g
hg2 : ∀ (x : α), g x ∈ (↑(Submodule.topologicalClosure (Submodule.span ℝ t)) : Set E)
hg3 : f =ᶠ[ae μ] g
a : α
ha : f a = g a
⊢ fY a = codRestrict g (↑Y : Set E) hg2 a
have this₁ : g a ∈ Y
Tactic: have : g a ∈ Y := hg2 a
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (hypothesis)
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
fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0
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
have hfY_int : Integrable fY μ
Tactic: 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (hypothesis)
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
fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0
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
have lem3 : μ[f | m] =ᶠ[ae μ] (⇑Y.subtypeL : (a : ↥Y) → E) ∘ μ[fY | m]
Tactic: have lem3 : μ[f | m] =ᵐ[μ] Y.subtypeL ∘ μ[fY | m] := calc
    _ =ᵐ[μ] μ[fX | m] := condExp_congr_ae lem1
    _ =ᵐ[μ] _ := (Y.subtypeL.comp_condExp_comm hfY_int).symm
-- 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
fY : α → ↥Y := fun (a : α) ↦ if h : f a ∈ Y then Subtype.mk (p := fun (x : E) ↦ x ∈ Y) (f a) h else 0
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
have h : ∀ (a : α) (ha : Membership.mem (γ := Set ↥Y) ((⇑Y.subtypeL : (a : ↥Y) → E) ⁻¹' s) (μ[fY | m] a))
  (hb : μ[f | m] a = ((⇑Y.subtypeL : (a : ↥Y) → E) ∘ μ[fY | m]) a), μ[f | m] a ∈ s
Tactic: 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
-- 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
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
have let₄ : ∀ (lem0 : ∀ᵐ (a : α) ∂μ, f a ∈ Y), ∀ᵐ (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
-- 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
⊢ ∀ᵐ (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), ∀ᵐ (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
-- 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
⊢ ∀ᵐ (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)),
  ∀ᵐ (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
-- 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
⊢ ∀ᵐ (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 μ), ∀ᵐ (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
-- 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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
have hm₁ : range (spanningSets (μ.trim hm)) ⊆ MeasurableSet
Tactic: apply (isCountablySpanning_spanningSets (μ.trim hm)).null_of_forall_restrict_null
-- 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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
hm₁ : range (spanningSets (μ.trim hm)) ⊆ MeasurableSet
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
have ht : ∀ t ∈ range (spanningSets (μ.trim hm)),
  Eq (α := ENNReal) ((μ.restrict t : (a : Set α) → ENNReal) {x : α | (fun (a : α) ↦ μ[f | m] a ∈ s) x}ᶜ : ENNReal)
    (0 : ENNReal)
Tactic: apply (isCountablySpanning_spanningSets (μ.trim hm)).null_of_forall_restrict_null
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (hypothesis)
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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
n : ℕ
⊢ Eq (α := ENNReal)
    ((μ.restrict (spanningSets (μ.trim hm) n) : (a : Set α) → ENNReal) {x : α | (fun (a : α) ↦ μ[f | m] a ∈ s) x}ᶜ :
      ENNReal)
    (0 : ENNReal)
have h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))] μ[f | m]
Tactic: have h1 := condExp_restrict_ae_eq_restrict hm (measurableSet_spanningSets (μ.trim hm) n) hf_int
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (hypothesis)
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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))] μ[f | m]
⊢ Eq (α := ENNReal)
    ((μ.restrict (spanningSets (μ.trim hm) n) : (a : Set α) → ENNReal) {x : α | (fun (a : α) ↦ μ[f | m] a ∈ s) x}ᶜ :
      ENNReal)
    (0 : ENNReal)
have this : IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n))
Tactic: have : IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n)) := isFiniteMeasure_restrict.2
    ((le_trim hm).trans_lt (measure_spanningSets_lt_top (μ.trim hm) n)).ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen (hypothesis)
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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))] μ[f | m]
this : IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n))
⊢ Eq (α := ENNReal)
    ((μ.restrict (spanningSets (μ.trim hm) n) : (a : Set α) → ENNReal) {x : α | (fun (a : α) ↦ μ[f | m] a ∈ s) x}ᶜ :
      ENNReal)
    (0 : ENNReal)
have h2 : ∀ᵐ (a : α) ∂μ.restrict (spanningSets (μ.trim hm) n), (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a ∈ s
Tactic: have h2 := hc.condExp_mem_of_isFiniteMeasure (μ := μ.restrict (spanningSets (μ.trim hm) n)) hm
    hf_int.restrict hs (ae_restrict_of_ae hf)
-- 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
hm : m ≤ mα
inst_3 : SigmaFinite (μ.trim hm)
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
n : ℕ
h1 : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] =ᶠ[ae (μ.restrict (spanningSets (μ.trim hm) n))] μ[f | m]
this : IsFiniteMeasure (μ.restrict (spanningSets (μ.trim hm) n))
h2 : ∀ᵐ (a : α) ∂μ.restrict (spanningSets (μ.trim hm) n), (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a ∈ s
⊢ Eq (α := ENNReal)
    ((μ.restrict (spanningSets (μ.trim hm) n) : (a : Set α) → ENNReal) {x : α | (fun (a : α) ↦ μ[f | m] a ∈ s) x}ᶜ :
      ENNReal)
    (0 : ENNReal)
have h : ∀ (a : α) (ha : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a = μ[f | m] a)
  (hb : (μ.restrict (spanningSets (μ.trim hm) n))[f | m] a ∈ s), μ[f | m] a ∈ s
Tactic: filter_upwards [h1, h2] with a ha hb
-- 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
φ : E → ℝ
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
inst_4 : HereditarilyLindelofSpace E
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) μ
⊢ ∀ᵐ (a : α) ∂μ, φ (μ[f | m] a) ≤ μ[φ ∘ f | m] a
have obtain : ∀ (L : ℕ → E →L[ℝ] ℝ) (c : ℕ → ℝ)
  (hLc1 :
    ∀ (i : ℕ),
      HAdd.hAdd (α := (a : (↑s : Type u_1)) → ℝ) (β := (↑s : Type u_1) → ℝ)
          (s.restrict (π := fun (a : E) ↦ ℝ) (⇑(L i) : (a : E) → ℝ) : (a : (↑s : Type u_1)) → ℝ)
          (const (↑s : Type u_1) (c i)) ≤
        s.restrict (π := fun (a : E) ↦ ℝ) φ)
  (hLc2 :
    ⨆ (i : ℕ),
        HAdd.hAdd (α := (a : (↑s : Type u_1)) → ℝ) (β := (↑s : Type u_1) → ℝ)
          (s.restrict (π := fun (a : E) ↦ ℝ) (⇑(L i) : (a : E) → ℝ) : (a : (↑s : Type u_1)) → ℝ)
          (const (↑s : Type u_1) (c i)) =
      s.restrict (π := fun (a : E) ↦ ℝ) φ),
  ∀ᵐ (a : α) ∂μ, φ (μ[f | m] a) ≤ μ[φ ∘ f | m] a
Tactic: obtain ⟨L, c, hLc1, hLc2⟩ := hφ_cvx.real_sSup_of_nat_affine_eq hs hφ_cont