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 g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]

Tactic:
exact (condExp_ae_eq_condExpL1 hm f).trans
    (Filter.EventuallyEq.trans (by rw [condExpL1_congr_ae hm h])
      (condExp_ae_eq_condExpL1 hm g).symm)

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_ae_eq_condExpL1, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfg : f =ᶠ[ae μ] g
⊢ μ[f | m] =ᶠ[ae (μ.trim hm)] μ[g | m]

Tactic:
StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable hm
    stronglyMeasurable_condExp stronglyMeasurable_condExp (condExp_congr_ae hfg)

Premises used: MeasureTheory.condExp_congr_ae, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hf : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ μ[f | m] =ᶠ[ae μ] f

Tactic:
((condExp_congr_ae hf.ae_eq_mk).trans ?_).trans hf.ae_eq_mk.symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_congr_ae, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hf : AEStronglyMeasurable f μ
hfi : Integrable f μ
refine : μ[AEStronglyMeasurable.mk f hf | m] =ᶠ[ae μ] AEStronglyMeasurable.mk f hf
⊢ μ[f | m] =ᶠ[ae μ] f

Tactic:
refine ((condExp_congr_ae hf.ae_eq_mk).trans ?_).trans hf.ae_eq_mk.symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_congr_ae, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hf : AEStronglyMeasurable f μ
hfi : Integrable f μ
rw rw₁ : AEStronglyMeasurable.mk f hf =ᶠ[ae μ] AEStronglyMeasurable.mk f hf
⊢ μ[AEStronglyMeasurable.mk f hf | m] =ᶠ[ae μ] AEStronglyMeasurable.mk f hf

Tactic:
rw [condExp_of_stronglyMeasurable hm hf.stronglyMeasurable_mk
    ((integrable_congr hf.ae_eq_mk).mp hfi)]

Premises used: MeasureTheory.integrable_congr, MeasureTheory.condExp_of_stronglyMeasurable, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, Iff.mp
-- 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
pos : ∀ (hm : m ≤ m₀), Integrable μ[f | m] μ
neg : ∀ (hm : ¬m ≤ m₀), Integrable μ[f | m] μ
⊢ Integrable μ[f | m] μ

Tactic:
by_cases hm : m ≤ m₀
-- 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
hm : ¬m ≤ m₀
neg : Integrable.{u_3, u_1} (ε := E) 0 μ
⊢ Integrable μ[f | m] μ

Tactic:
rw [condExp_of_not_le hm]

Premises used: MeasureTheory.condExp_of_not_le
-- 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
hm : ¬m ≤ m₀
⊢ Integrable.{u_3, u_1} (ε := E) 0 μ

Tactic:
integrable_zero _ _ _

Premises used: 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
hm : ¬m ≤ m₀
⊢ Integrable.{u_3, u_1} (ε := E) 0 μ

Tactic:
exact integrable_zero _ _ _

Premises used: 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
hm : m ≤ m₀
pos : ∀ (hμm : SigmaFinite (μ.trim hm)), Integrable μ[f | m] μ
neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), Integrable μ[f | m] μ
⊢ Integrable μ[f | m] μ

Tactic:
by_cases hμm : SigmaFinite (μ.trim hm)

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- 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
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
neg : Integrable.{u_3, u_1} (ε := E) 0 μ
⊢ Integrable μ[f | m] μ

Tactic:
rw [condExp_of_not_sigmaFinite hm hμm]

Premises used: MeasureTheory.condExp_of_not_sigmaFinite
-- 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
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ Integrable.{u_3, u_1} (ε := E) 0 μ

Tactic:
integrable_zero _ _ _

Premises used: 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
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ Integrable.{u_3, u_1} (ε := E) 0 μ

Tactic:
exact integrable_zero _ _ _

Premises used: 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
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ Integrable μ[f | m] μ

Tactic:
(integrable_condExpL1 f).congr (condExp_ae_eq_condExpL1 hm f).symm

Premises used: MeasureTheory.condExp_ae_eq_condExpL1, MeasureTheory.Integrable.congr, MeasureTheory.integrable_condExpL1, Filter.EventuallyEq.symm
-- 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
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ Integrable μ[f | m] μ

Tactic:
exact (integrable_condExpL1 f).congr (condExp_ae_eq_condExpL1 hm f).symm

Premises used: MeasureTheory.condExp_ae_eq_condExpL1, MeasureTheory.Integrable.congr, MeasureTheory.integrable_condExpL1, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
s : Set α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
inst_3 : SigmaFinite (μ.trim hm)
hf : Integrable f μ
hs : MeasurableSet s
rw : Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) x ∂μ) (∫ (x : α) in s, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, μ[f | m] x ∂μ) (∫ (x : α) in s, f x ∂μ)

Tactic:
rw [setIntegral_congr_ae (hm s hs) ((condExp_ae_eq_condExpL1 hm f).mono fun x hx _ => hx)]

Premises used: MeasureTheory.setIntegral_congr_ae, MeasureTheory.condExp_ae_eq_condExpL1, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
s : Set α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
inst_3 : SigmaFinite (μ.trim hm)
hf : Integrable f μ
hs : MeasurableSet s
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) x ∂μ) (∫ (x : α) in s, f x ∂μ)

Tactic:
setIntegral_condExpL1 hf hs

Premises used: MeasureTheory.setIntegral_condExpL1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
s : Set α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
inst_3 : SigmaFinite (μ.trim hm)
hf : Integrable f μ
hs : MeasurableSet s
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) x ∂μ) (∫ (x : α) in s, f x ∂μ)

Tactic:
exact setIntegral_condExpL1 hf hs

Premises used: MeasureTheory.setIntegral_condExpL1
-- 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
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
pos : ∀ (hf : Integrable f μ), Eq.{u_3 + 1} (α := E) (∫ (x : α), μ[f | m] x ∂μ) (∫ (x : α), f x ∂μ)
neg : ∀ (hf : ¬Integrable f μ), Eq.{u_3 + 1} (α := E) (∫ (x : α), μ[f | m] x ∂μ) (∫ (x : α), f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α), μ[f | m] x ∂μ) (∫ (x : α), f x ∂μ)

Tactic:
by_cases hf : Integrable f μ

Premises used: MeasureTheory.Integrable
-- 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
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : Integrable f μ
this : Eq.{u_3 + 1} (α := E) (∫ (x : α) in Set.univ, μ[f | m] x ∂μ) (∫ (x : α) in Set.univ, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α), μ[f | m] x ∂μ) (∫ (x : α), f x ∂μ)

Tactic:
simp_rw [setIntegral_univ] at this

Premises used: MeasureTheory.setIntegral_univ
-- 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
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : Integrable f μ
this : Eq.{u_3 + 1} (α := E) (∫ (x : α), μ[f | m] x ∂μ) (∫ (x : α), f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α), μ[f | m] x ∂μ) (∫ (x : α), f x ∂μ)

Tactic:
this
-- 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
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : Integrable f μ
this : Eq.{u_3 + 1} (α := E) (∫ (x : α), μ[f | m] x ∂μ) (∫ (x : α), f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α), μ[f | m] x ∂μ) (∫ (x : α), f x ∂μ)

Tactic:
exact this
-- 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
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : Integrable f μ
pos : Eq.{u_3 + 1} (α := E) (∫ (x : α) in Set.univ, μ[f | m] x ∂μ) (∫ (x : α) in Set.univ, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α), μ[f | m] x ∂μ) (∫ (x : α), f x ∂μ)

Tactic:
suffices ∫ x in Set.univ, (μ[f | m]) x ∂μ = ∫ x in Set.univ, f x ∂μ by
      simp_rw [setIntegral_univ] at this; exact this
-- 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
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : Integrable f μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α) in Set.univ, μ[f | m] x ∂μ) (∫ (x : α) in Set.univ, f x ∂μ)

Tactic:
setIntegral_condExp hm hf .univ

Premises used: MeasureTheory.setIntegral_condExp, MeasurableSet.univ
-- 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
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : Integrable f μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α) in Set.univ, μ[f | m] x ∂μ) (∫ (x : α) in Set.univ, f x ∂μ)

Tactic:
exact setIntegral_condExp hm hf .univ

Premises used: MeasureTheory.setIntegral_condExp, MeasurableSet.univ
-- 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
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hf : ¬Integrable f μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α), μ[f | m] x ∂μ) (∫ (x : α), f x ∂μ)

Tactic:
simp only [condExp_of_not_integrable hf, Pi.zero_apply, integral_zero, integral_undef hf]

Premises used: MeasureTheory.integral_undef, Pi.zero_apply, MeasureTheory.condExp_of_not_integrable, MeasureTheory.integral_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
β : Type u_2
m₀ : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
Y : α → β
hY : Measurable Y
inst : SigmaFinite (μ.trim ⋯)
A : Set α
hA : MeasurableSet A
rw : ∫ (x : α), A.indicator (fun (x : α) ↦ 1) x ∂μ = μ.real A
rw₁ : ∫ (x : α) in A, 1 ∂μ = μ.real A
rw₂ : HSMul.hSMul (β := ℝ) (μ.real A) 1 = μ.real A
rw₃ : μ.real A * 1 = μ.real A
rw₄ rw₅ : μ.real A = μ.real A
⊢ ∫ (x : α), μ[A.indicator fun (x : α) ↦ 1 | MeasurableSpace.comap Y mβ] x ∂μ = μ.real A

Tactic:
rw [integral_condExp, integral_indicator hA, setIntegral_const, smul_eq_mul, mul_one]

Premises used: MeasureTheory.integral_indicator, MeasureTheory.integral_condExp, smul_eq_mul, mul_one, MeasureTheory.setIntegral_const
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
inst_3 : SigmaFinite (μ.trim hm)
f g : α → E
hf : Integrable f μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hg_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, f x ∂μ)
hgm : AEStronglyMeasurable g μ
⊢ g =ᶠ[ae μ] μ[f | m]

Tactic:
ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' hm hg_int_finite
    (fun s _ _ => integrable_condExp.integrableOn) (fun s hs hμs => ?_) hgm
    (StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_condExp)

Premises used: MeasureTheory.integrable_condExp, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.Integrable.integrableOn, MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
inst_3 : SigmaFinite (μ.trim hm)
f g : α → E
hf : Integrable f μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hg_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, f x ∂μ)
hgm : AEStronglyMeasurable g μ
refine :
  ∀ (s : Set α) (hs : MeasurableSet s) (hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, μ[f | m] x ∂μ)
⊢ g =ᶠ[ae μ] μ[f | m]

Tactic:
refine ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' hm hg_int_finite
    (fun s _ _ => integrable_condExp.integrableOn) (fun s hs hμs => ?_) hgm
    (StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_condExp)

Premises used: MeasureTheory.integrable_condExp, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.Integrable.integrableOn, MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
inst_3 : SigmaFinite (μ.trim hm)
f g : α → E
hf : Integrable f μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hg_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, f x ∂μ)
hgm : AEStronglyMeasurable g μ
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, μ[f | m] x ∂μ)
rw₁ rw₂ : Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, μ[f | m] x ∂μ)

Tactic:
rw [hg_eq s hs hμs, setIntegral_condExp hm hf hs]

Premises used: MeasureTheory.setIntegral_condExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hμ : NeZero μ
f : α → E
pos :
  ∀ (hμ_finite : IsFiniteMeasure μ),
    μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
neg :
  ∀ (hμ_finite : ¬IsFiniteMeasure μ),
    μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
⊢ μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)

Tactic:
by_cases hμ_finite : IsFiniteMeasure μ

Premises used: MeasureTheory.IsFiniteMeasure
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite rwa rwa₁ rwa₂ rwa₃ : ¬IsFiniteMeasure μ
⊢ ¬SigmaFinite (m0 := ⊥) (μ.trim ⋯)

Tactic:
rwa [sigmaFinite_trim_bot_iff]

Premises used: MeasureTheory.sigmaFinite_trim_bot_iff
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : ¬IsFiniteMeasure μ
⊢ ¬SigmaFinite (m0 := ⊥) (μ.trim ⋯)

Tactic:
have h : ¬SigmaFinite (μ.trim bot_le) := by rwa [sigmaFinite_trim_bot_iff]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : ¬IsFiniteMeasure μ
h : ¬SigmaFinite (m0 := ⊥) (μ.trim ⋯)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [not_isFiniteMeasure_iff] at hμ_finite

Premises used: MeasureTheory.not_isFiniteMeasure_iff
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : ¬IsFiniteMeasure μ
h : ¬SigmaFinite (m0 := ⊥) (μ.trim ⋯)
hμ_finite₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ¬SigmaFinite (m0 := ⊥) (μ.trim ⋯)

Tactic:
rw [not_isFiniteMeasure_iff] at hμ_finite

Premises used: MeasureTheory.not_isFiniteMeasure_iff
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
h : ¬SigmaFinite (m0 := ⊥) (μ.trim ⋯)
neg : Eq (α := α → E) 0 fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
⊢ μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)

Tactic:
rw [condExp_of_not_sigmaFinite bot_le h]

Premises used: MeasureTheory.condExp_of_not_sigmaFinite, bot_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
h : ¬SigmaFinite (m0 := ⊥) (μ.trim ⋯)
neg : Eq (α := α → E) 0 fun (x : α) ↦ 0
⊢ Eq (α := α → E) 0 fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)

Tactic:
simp only [hμ_finite, ENNReal.toReal_top, inv_zero, zero_smul, measureReal_def]

Premises used: inv_zero, zero_smul, MeasureTheory.measureReal_def, ENNReal.toReal_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
h : ¬SigmaFinite (m0 := ⊥) (μ.trim ⋯)
⊢ Eq (α := α → E) 0 fun (x : α) ↦ 0

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
⊢ StronglyMeasurable μ[f | ⊥]

Tactic:
have h_meas : StronglyMeasurable[⊥] (μ[f | ⊥]) := stronglyMeasurable_condExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable μ[f | ⊥]
pos :
  ∀ (c : E) (h_eq : μ[f | ⊥] = fun (x : α) ↦ c),
    μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
⊢ μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)

Tactic:
obtain ⟨c, h_eq⟩ := stronglyMeasurable_bot_iff.mp h_meas

Premises used: Iff.mp, stronglyMeasurable_bot_iff
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable μ[f | ⊥]
c : E
h_eq : μ[f | ⊥] = fun (x : α) ↦ c
pos : Eq (α := α → E) (fun (x : α) ↦ c) fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
⊢ μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)

Tactic:
rw [h_eq]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable μ[f | ⊥]
c : E
h_eq : μ[f | ⊥] = fun (x : α) ↦ c
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α), μ[f | ⊥] x ∂μ) (∫ (x : α), f x ∂μ)

Tactic:
have h_integral : ∫ x, (μ[f | ⊥]) x ∂μ = ∫ x, f x ∂μ := integral_condExp bot_le