awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hf : ¬Integrable f μ
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f | m] = 0
have neg : Eq (α := α → E) 0 0
Tactic: rw [condExp_of_not_sigmaFinite hm hμm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hf : ¬Integrable f μ
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f | m] = 0
have pos : (if Integrable f μ then
    if StronglyMeasurable f then f
    else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) sorry
  else 0) =
  0
Tactic: rw [condExp_of_sigmaFinite, if_neg hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hf : ¬Integrable f μ
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
pos :
  (if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
    else 0) =
    0
⊢ μ[f | m] = 0
have pos₁ : Eq (α := α → E) 0 0
Tactic: rw [condExp_of_sigmaFinite, if_neg hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
⊢ Eq (α := α → E) μ[0 | m] 0
have pos : ∀ (hm : m ≤ m₀), Eq (α := α → E) μ[0 | m] 0
Tactic: by_cases hm : m ≤ m₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
pos : ∀ (hm : m ≤ m₀), Eq (α := α → E) μ[0 | m] 0
⊢ Eq (α := α → E) μ[0 | m] 0
have neg : ∀ (hm : ¬m ≤ m₀), Eq (α := α → E) μ[0 | m] 0
Tactic: by_cases hm : m ≤ m₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : ¬m ≤ m₀
⊢ Eq (α := α → E) μ[0 | m] 0
have neg : Eq (α := α → E) 0 0
Tactic: rw [condExp_of_not_le hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
⊢ Eq (α := α → E) μ[0 | m] 0
have pos : ∀ (hμm : SigmaFinite (μ.trim hm)), Eq (α := α → E) μ[0 | m] 0
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
pos : ∀ (hμm : SigmaFinite (μ.trim hm)), Eq (α := α → E) μ[0 | m] 0
⊢ Eq (α := α → E) μ[0 | m] 0
have neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), Eq (α := α → E) μ[0 | m] 0
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ Eq (α := α → E) μ[0 | m] 0
have neg : Eq (α := α → E) 0 0
Tactic: rw [condExp_of_not_sigmaFinite hm hμm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
⊢ StronglyMeasurable μ[f | m]
have pos : ∀ (hm : m ≤ m₀), StronglyMeasurable μ[f | m]
Tactic: by_cases hm : m ≤ m₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
pos : ∀ (hm : m ≤ m₀), StronglyMeasurable μ[f | m]
⊢ StronglyMeasurable μ[f | m]
have neg : ∀ (hm : ¬m ≤ m₀), StronglyMeasurable μ[f | m]
Tactic: by_cases hm : m ≤ m₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : ¬m ≤ m₀
⊢ StronglyMeasurable μ[f | m]
have neg : StronglyMeasurable.{u_1, u_3} (α := α) (β := E) 0
Tactic: rw [condExp_of_not_le hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
⊢ StronglyMeasurable μ[f | m]
have pos : ∀ (hμm : SigmaFinite (μ.trim hm)), StronglyMeasurable μ[f | m]
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
pos : ∀ (hμm : SigmaFinite (μ.trim hm)), StronglyMeasurable μ[f | m]
⊢ StronglyMeasurable μ[f | m]
have neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), StronglyMeasurable μ[f | m]
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ StronglyMeasurable μ[f | m]
have neg : StronglyMeasurable.{u_1, u_3} (α := α) (β := E) 0
Tactic: rw [condExp_of_not_sigmaFinite hm hμm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ StronglyMeasurable μ[f | m]
have pos : StronglyMeasurable
  (if Integrable f μ then
    if StronglyMeasurable f then f
    else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) sorry
  else 0)
Tactic: rw [condExp_of_sigmaFinite hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ StronglyMeasurable
    (if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
    else 0)
have pos : ∀ (hfi : Integrable f μ) (hfm : StronglyMeasurable f), StronglyMeasurable f
Tactic: split_ifs with hfi hfm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
pos : ∀ (hfi : Integrable f μ) (hfm : StronglyMeasurable f), StronglyMeasurable f
⊢ StronglyMeasurable
    (if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
    else 0)
have neg : ∀ (hfi : Integrable f μ) (hfm : ¬StronglyMeasurable f),
  StronglyMeasurable
    (AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) sorry)
Tactic: split_ifs with hfi hfm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
pos : ∀ (hfi : Integrable f μ) (hfm : StronglyMeasurable f), StronglyMeasurable f
neg :
  ∀ (hfi : Integrable f μ) (hfm : ¬StronglyMeasurable f),
    StronglyMeasurable
      (AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯)
⊢ StronglyMeasurable
    (if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
    else 0)
have neg₁ : ∀ (hfi : ¬Integrable f μ), StronglyMeasurable.{u_1, u_3} (α := α) (β := E) 0
Tactic: split_ifs with hfi hfm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]
have pos : ∀ (hm : m ≤ m₀), μ[f | m] =ᶠ[ae μ] μ[g | m]
Tactic: by_cases hm : m ≤ m₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
pos : ∀ (hm : m ≤ m₀), μ[f | m] =ᶠ[ae μ] μ[g | m]
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]
have neg : ∀ (hm : ¬m ≤ m₀), μ[f | m] =ᶠ[ae μ] μ[g | m]
Tactic: by_cases hm : m ≤ m₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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₀
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]
have neg : EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 0
Tactic: simp_rw [condExp_of_not_le hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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₀
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]
have pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[f | m] =ᶠ[ae μ] μ[g | m]
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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₀
pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[f | m] =ᶠ[ae μ] μ[g | m]
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]
have neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), μ[f | m] =ᶠ[ae μ] μ[g | m]
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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]
have neg : EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 0
Tactic: simp_rw [condExp_of_not_sigmaFinite hm hμm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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)
⊢ (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(condExpL1 hm μ g) : α →ₘ[μ] E) : α → E)
have rw : (↑(↑(condExpL1 hm μ g) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(condExpL1 hm μ g) : α →ₘ[μ] E) : α → E)
Tactic: rw [condExpL1_congr_ae hm h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
have refine : μ[AEStronglyMeasurable.mk f hf | m] =ᶠ[ae μ] AEStronglyMeasurable.mk f hf
Tactic: refine ((condExp_congr_ae hf.ae_eq_mk).trans ?_).trans hf.ae_eq_mk.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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 μ
⊢ μ[AEStronglyMeasurable.mk f hf | m] =ᶠ[ae μ] AEStronglyMeasurable.mk f hf
have rw : AEStronglyMeasurable.mk f hf =ᶠ[ae μ] AEStronglyMeasurable.mk f hf
Tactic: rw [condExp_of_stronglyMeasurable hm hf.stronglyMeasurable_mk
    ((integrable_congr hf.ae_eq_mk).mp hfi)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
⊢ Integrable μ[f | m] μ
have pos : ∀ (hm : m ≤ m₀), Integrable μ[f | m] μ
Tactic: by_cases hm : m ≤ m₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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] μ
⊢ Integrable μ[f | m] μ
have neg : ∀ (hm : ¬m ≤ m₀), Integrable μ[f | m] μ
Tactic: by_cases hm : m ≤ m₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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 μ[f | m] μ
have neg : Integrable.{u_3, u_1} (ε := E) 0 μ
Tactic: rw [condExp_of_not_le hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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 μ[f | m] μ
have pos : ∀ (hμm : SigmaFinite (μ.trim hm)), Integrable μ[f | m] μ
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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] μ
⊢ Integrable μ[f | m] μ
have neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), Integrable μ[f | m] μ
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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] μ
have neg : Integrable.{u_3, u_1} (ε := E) 0 μ
Tactic: rw [condExp_of_not_sigmaFinite hm hμm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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, μ[f | m] x ∂μ) (∫ (x : α) in s, f x ∂μ)
have rw : Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) 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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α), μ[f | m] x ∂μ) (∫ (x : α), f x ∂μ)
have pos : ∀ (hf : Integrable f μ), Eq.{u_3 + 1} (α := E) (∫ (x : α), μ[f | m] x ∂μ) (∫ (x : α), f x ∂μ)
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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 ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α), μ[f | m] x ∂μ) (∫ (x : α), f x ∂μ)
have neg : ∀ (hf : ¬Integrable f μ), Eq.{u_3 + 1} (α := E) (∫ (x : α), μ[f | m] x ∂μ) (∫ (x : α), f x ∂μ)
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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 ∂μ)
have pos : Eq.{u_3 + 1} (α := E) (∫ (x : α) in Set.univ, μ[f | m] x ∂μ) (∫ (x : α) in Set.univ, 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m₀ : MeasurableSpace α
μ : Measure α
mβ : MeasurableSpace β
Y : α → β
hY : Measurable Y
inst : SigmaFinite (μ.trim ⋯)
A : Set α
hA : MeasurableSet A
⊢ ∫ (x : α), μ[A.indicator fun (x : α) ↦ 1 | MeasurableSpace.comap Y mβ] x ∂μ = μ.real A
have rw : ∫ (x : α), A.indicator (fun (x : α) ↦ 1) x ∂μ = μ.real A
Tactic: rw [integral_condExp, integral_indicator hA, setIntegral_const, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
⊢ ∫ (x : α), μ[A.indicator fun (x : α) ↦ 1 | MeasurableSpace.comap Y mβ] x ∂μ = μ.real A
have rw₁ : ∫ (x : α) in A, 1 ∂μ = μ.real A
Tactic: rw [integral_condExp, integral_indicator hA, setIntegral_const, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
⊢ ∫ (x : α), μ[A.indicator fun (x : α) ↦ 1 | MeasurableSpace.comap Y mβ] x ∂μ = μ.real A
have rw₂ : HSMul.hSMul (β := ℝ) (μ.real A) 1 = μ.real A
Tactic: rw [integral_condExp, integral_indicator hA, setIntegral_const, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
⊢ ∫ (x : α), μ[A.indicator fun (x : α) ↦ 1 | MeasurableSpace.comap Y mβ] x ∂μ = μ.real A
have rw₃ : μ.real A * 1 = μ.real A
Tactic: rw [integral_condExp, integral_indicator hA, setIntegral_const, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
⊢ ∫ (x : α), μ[A.indicator fun (x : α) ↦ 1 | MeasurableSpace.comap Y mβ] x ∂μ = μ.real A
have rw₄ : μ.real A = μ.real A
Tactic: rw [integral_condExp, integral_indicator hA, setIntegral_const, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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]
have 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 ∂μ)
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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∞)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, μ[f | m] x ∂μ)
have rw : Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, μ[f | m] x ∂μ)
Tactic: rw [hg_eq s hs hμs, setIntegral_condExp hm hf hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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 ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, g x ∂μ) (∫ (x : α) in s, μ[f | m] x ∂μ)
have rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, f x ∂μ)
Tactic: rw [hg_eq s hs hμs, setIntegral_condExp hm hf hs]