awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : ClosedIciTopology E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
hf : f ≤ᶠ[ae μ] 0
hfint : Integrable f μ
⊢ μ[f | m] ≤ᶠ[ae μ] μ[0 | m]

Tactic:
condExp_mono hfint (integrable_zero _ _ _) hf

Premises used: MeasureTheory.condExp_mono, MeasureTheory.integrable_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : ClosedIciTopology E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
hf : f ≤ᶠ[ae μ] 0
hfint : Integrable f μ
⊢ μ[f | m] ≤ᶠ[ae μ] μ[0 | m]

Tactic:
exact condExp_mono hfint (integrable_zero _ _ _) hf

Premises used: MeasureTheory.condExp_mono, MeasureTheory.integrable_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : PartialOrder E
inst_4 : ClosedIciTopology E
inst_5 : IsOrderedAddMonoid E
inst_6 : IsOrderedModule ℝ E
hf : f ≤ᶠ[ae μ] 0
hfint : ¬Integrable f μ
neg neg₁ : EventuallyLE.{u_1, u_3} (β := E) (ae μ) 0 0
⊢ μ[f | m] ≤ᶠ[ae μ] 0

Tactic:
rw [condExp_of_not_integrable hfint]

Premises used: MeasureTheory.condExp_of_not_integrable
-- 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
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
inst_4 : HereditarilyLindelofSpace E
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
obtain :
  ∀ (L : ℕ → StrongDual ℝ E) (c : ℕ → ℝ)
    (hLc : ⋂ (n : ℕ), {x : E | (RCLike.re : (a : ℝ) → ℝ) ((L n : (a : E) → ℝ) x : ℝ) ≤ c n} = s),
    ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s

Tactic:
obtain ⟨L, c, hLc⟩ := RCLike.iInter_countable_halfSpaces_eq (𝕜 := ℝ) hc hs

Premises used: RCLike.iInter_countable_halfSpaces_eq
-- 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
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
inst_4 : HereditarilyLindelofSpace E
hm : m ≤ mα
hf_int : Integrable f μ
hs : IsClosed s
hc : Convex ℝ s
hf : ∀ᵐ (a : α) ∂μ, f a ∈ s
L : ℕ → StrongDual ℝ E
c : ℕ → ℝ
hLc : ⋂ (n : ℕ), {x : E | (RCLike.re : (a : ℝ) → ℝ) ((L n : (a : E) → ℝ) x : ℝ) ≤ c n} = s
simp_all :
  ∀ (hs : IsClosed.{u_1} (X := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n}))
    (hc : Convex.{0, u_1} ℝ (E := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n}))
    (hf : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) {x : E | (L i : (a : E) → ℝ) x ≤ c i} (f a)) (i : ℕ),
    ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) {x : E | (L i : (a : E) → ℝ) x ≤ c i} (μ[f | m] a)
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s

Tactic:
simp_all only [← hLc, RCLike.re_to_real, mem_iInter, ae_all_iff]

Premises used: RCLike.re_to_real, Set.mem_iInter, MeasureTheory.ae_all_iff
-- 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
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
inst_4 : HereditarilyLindelofSpace E
hm : m ≤ mα
hf_int : Integrable f μ
L : ℕ → StrongDual ℝ E
c : ℕ → ℝ
hs : IsClosed.{u_1} (X := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hc : Convex.{0, u_1} ℝ (E := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hf : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) {x : E | (L i : (a : E) → ℝ) x ≤ c i} (f a)
n : ℕ
⊢ (ae μ).EventuallyEq (β := ℝ) ((⇑(L n) : (a : E) → ℝ) ∘ μ[f | m]) μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m]

Tactic:
have h1 := ContinuousLinearMap.comp_condExp_comm (m := m) hf_int (L n)
-- 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
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
inst_4 : HereditarilyLindelofSpace E
hm : m ≤ mα
hf_int : Integrable f μ
L : ℕ → StrongDual ℝ E
c : ℕ → ℝ
hs : IsClosed.{u_1} (X := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hc : Convex.{0, u_1} ℝ (E := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hf : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) {x : E | (L i : (a : E) → ℝ) x ≤ c i} (f a)
n : ℕ
h1 : (ae μ).EventuallyEq (β := ℝ) ((⇑(L n) : (a : E) → ℝ) ∘ μ[f | m]) μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m]
⊢ (ae μ).EventuallyLE (β := ℝ) μ[fun (a : α) ↦ (L n : (a : E) → ℝ) (f a) | m] μ[fun (x : α) ↦ c n | m]

Tactic:
have h2 := condExp_mono (m := m) ((L n).integrable_comp hf_int) (integrable_const (c n)) (hf n)
-- 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
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
inst_4 : HereditarilyLindelofSpace E
hm : m ≤ mα
hf_int : Integrable f μ
L : ℕ → StrongDual ℝ E
c : ℕ → ℝ
hs : IsClosed.{u_1} (X := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hc : Convex.{0, u_1} ℝ (E := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hf : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) {x : E | (L i : (a : E) → ℝ) x ≤ c i} (f a)
n : ℕ
h1 : (ae μ).EventuallyEq (β := ℝ) ((⇑(L n) : (a : E) → ℝ) ∘ μ[f | m]) μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m]
h2 : (ae μ).EventuallyLE (β := ℝ) μ[fun (a : α) ↦ (L n : (a : E) → ℝ) (f a) | m] μ[fun (x : α) ↦ c n | m]
h :
  ∀ (a : α) (ha : Eq (α := ℝ) (((⇑(L n) : (a : E) → ℝ) ∘ μ[f | m]) a) (μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m] a))
    (hb : LE.le (α := ℝ) (μ[fun (a : α) ↦ (L n : (a : E) → ℝ) (f a) | m] a) (μ[fun (x : α) ↦ c n | m] a)),
    (L n : (a : E) → ℝ) (μ[f | m] a) ≤ c n
⊢ ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) {x : E | (L n : (a : E) → ℝ) x ≤ c n} (μ[f | m] a)

Tactic:
filter_upwards [h1, h2] with a ha hb
-- 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
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
inst_4 : HereditarilyLindelofSpace E
hm : m ≤ mα
hf_int : Integrable f μ
L : ℕ → StrongDual ℝ E
c : ℕ → ℝ
hs : IsClosed.{u_1} (X := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hc : Convex.{0, u_1} ℝ (E := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hf : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) {x : E | (L i : (a : E) → ℝ) x ≤ c i} (f a)
n : ℕ
h1 : (ae μ).EventuallyEq (β := ℝ) ((⇑(L n) : (a : E) → ℝ) ∘ μ[f | m]) μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m]
h2 : (ae μ).EventuallyLE (β := ℝ) μ[fun (a : α) ↦ (L n : (a : E) → ℝ) (f a) | m] μ[fun (x : α) ↦ c n | m]
a : α
ha : Eq (α := ℝ) (((⇑(L n) : (a : E) → ℝ) ∘ μ[f | m]) a) (μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m] a)
hb : LE.le (α := ℝ) (μ[fun (a : α) ↦ (L n : (a : E) → ℝ) (f a) | m] a) (μ[fun (x : α) ↦ c n | m] a)
h :
  ∀ (h2 : (ae μ).EventuallyLE (β := ℝ) μ[fun (a : α) ↦ (L n : (a : E) → ℝ) (f a) | m] fun (x : α) ↦ c n)
    (ha : Eq (α := ℝ) ((L n : (a : E) → ℝ) (μ[f | m] a) : ℝ) (μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m] a : ℝ))
    (hb : μ[fun (a : α) ↦ (L n : (a : E) → ℝ) (f a) | m] a ≤ c n), μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m] a ≤ c n
⊢ (L n : (a : E) → ℝ) (μ[f | m] a) ≤ c n

Tactic:
simp_all only [condExp_const, comp_apply]

Premises used: MeasureTheory.condExp_const, Function.comp_apply
-- 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
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
inst_4 : HereditarilyLindelofSpace E
hm : m ≤ mα
hf_int : Integrable f μ
L : ℕ → StrongDual ℝ E
c : ℕ → ℝ
hs : IsClosed.{u_1} (X := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hc : Convex.{0, u_1} ℝ (E := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hf : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) {x : E | (L i : (a : E) → ℝ) x ≤ c i} (f a)
n : ℕ
h1 : (ae μ).EventuallyEq (β := ℝ) ((⇑(L n) : (a : E) → ℝ) ∘ μ[f | m]) μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m]
a : α
h2 : (ae μ).EventuallyLE (β := ℝ) μ[fun (a : α) ↦ (L n : (a : E) → ℝ) (f a) | m] fun (x : α) ↦ c n
ha : Eq (α := ℝ) ((L n : (a : E) → ℝ) (μ[f | m] a) : ℝ) (μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m] a : ℝ)
hb : μ[fun (a : α) ↦ (L n : (a : E) → ℝ) (f a) | m] a ≤ c n
⊢ μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m] a ≤ c n

Tactic:
hb
-- 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
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
inst_4 : HereditarilyLindelofSpace E
hm : m ≤ mα
hf_int : Integrable f μ
L : ℕ → StrongDual ℝ E
c : ℕ → ℝ
hs : IsClosed.{u_1} (X := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hc : Convex.{0, u_1} ℝ (E := E) (⋂ (n : ℕ), {x : E | (L n : (a : E) → ℝ) x ≤ c n})
hf : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set E) {x : E | (L i : (a : E) → ℝ) x ≤ c i} (f a)
n : ℕ
h1 : (ae μ).EventuallyEq (β := ℝ) ((⇑(L n) : (a : E) → ℝ) ∘ μ[f | m]) μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m]
a : α
h2 : (ae μ).EventuallyLE (β := ℝ) μ[fun (a : α) ↦ (L n : (a : E) → ℝ) (f a) | m] fun (x : α) ↦ c n
ha : Eq (α := ℝ) ((L n : (a : E) → ℝ) (μ[f | m] a) : ℝ) (μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m] a : ℝ)
hb : μ[fun (a : α) ↦ (L n : (a : E) → ℝ) (f a) | m] a ≤ c n
⊢ μ[(⇑(L n) : (a : E) → ℝ) ∘ f | m] a ≤ c n

Tactic:
exact hb
-- 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
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
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- 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
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 : MeasurableSpace E := borel E
this_1 : BorelSpace E
obtain :
  ∀ (t : Set E) (ht : TopologicalSpace.IsSeparable t) (htt : ∀ᵐ (x : α) ∂μ, f x ∈ t), ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s
⊢ ∀ᵐ (a : α) ∂μ, μ[f | m] a ∈ s

Tactic:
obtain ⟨t, ht, htt⟩ := hf_int.aestronglyMeasurable.isSeparable_ae_range

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.isSeparable_ae_range
-- 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
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 : MeasurableSpace E := borel E
this_1 : BorelSpace E
t : Set E
ht : TopologicalSpace.IsSeparable t
htt : ∀ᵐ (x : α) ∂μ, f x ∈ t
Y : Submodule ℝ E := Submodule.topologicalClosure (Submodule.span ℝ t)
⊢ CompleteSpace.{u_1} ↥Y

Tactic:
have : CompleteSpace Y := (Submodule.isClosed_topologicalClosure _).completeSpace_coe
-- 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
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 : CompleteSpace.{u_1} ↥Y
⊢ SecondCountableTopology.{u_1} ↥Y

Tactic:
have : SecondCountableTopology Y := ht.span.closure.secondCountableTopology
-- 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
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
a : α
ha : f a ∈ t
⊢ f a ∈ Y

Tactic:
(Submodule.closure_subset_topologicalClosure_span t) (subset_closure ha)

Premises used: Submodule.closure_subset_topologicalClosure_span, Set.Mem, subset_closure
-- 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
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
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ∈ t) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ f a ∈ Y) x} x}
      a
h₁ h₂ : ∀ (a : α) (ha : f a ∈ t), f a ∈ Y
⊢ ∀ᵐ (a : α) ∂μ, f a ∈ Y

Tactic:
filter_upwards [htt] with a ha using
      (Submodule.closure_subset_topologicalClosure_span t) (subset_closure ha)
-- 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
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
⊢ ∀ᵐ (a : α) ∂μ, f a ∈ Y

Tactic:
have lem0 : ∀ᵐ a ∂μ, f a ∈ Y := by
    filter_upwards [htt] with a ha using
      (Submodule.closure_subset_topologicalClosure_span t) (subset_closure ha)
-- 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
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
h : ∀ (a : α) (ha : f a ∈ Y), f a = fX a
⊢ f =ᶠ[ae μ] fX

Tactic:
filter_upwards [lem0] with a ha
-- 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
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
a : α
ha : f a ∈ Y
⊢ f a = fX a

Tactic:
simp_all [fX, fY]
-- 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
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
⊢ f =ᶠ[ae μ] fX

Tactic:
have lem1 : f =ᵐ[μ] fX := by
    filter_upwards [lem0] with a ha
    simp_all [fX, fY]
-- 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
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
h : ∀ (a : α) (ha : f a ∈ Y) (hs : f a ∈ s), Membership.mem (γ := Set ↥Y) ((⇑Y.subtypeL : (a : ↥Y) → E) ⁻¹' s) (fY a)
⊢ ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set ↥Y) ((⇑Y.subtypeL : (a : ↥Y) → E) ⁻¹' s) (fY a)

Tactic:
filter_upwards [lem0, hf] with a ha hs
-- 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
m mα : MeasurableSpace α
μ : Measure α
s : Set E
inst_3 : IsFiniteMeasure μ
hm : m ≤ mα
hf_int : Integrable f μ
hs_1 : 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
a : α
ha : f a ∈ Y
hs : f a ∈ s
⊢ Membership.mem (γ := Set ↥Y) ((⇑Y.subtypeL : (a : ↥Y) → E) ⁻¹' s) (fY a)

Tactic:
simpa [fY, ha]
-- 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
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
⊢ ∀ᵐ (a : α) ∂μ, Membership.mem (γ := Set ↥Y) ((⇑Y.subtypeL : (a : ↥Y) → E) ⁻¹' s) (fY a)

Tactic:
have lem2 : ∀ᵐ a ∂μ, fY a ∈ Y.subtypeL ⁻¹' s := by
    filter_upwards [lem0, hf] with a ha hs
    simpa [fY, ha]
-- 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
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 : α) ∂μ, ‖fY a‖ ≤ ‖fX a‖

Tactic:
simp [fX]
-- 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
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)
refine : AEStronglyMeasurable fY μ
⊢ Integrable fY μ

Tactic:
refine (hf_int.congr lem1).mono ?_ (by simp [fX])

Premises used: MeasureTheory.Integrable.mono, MeasureTheory.Integrable.congr