awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (HPow.hPow (β := ℕ) X 2) μ
aux₁ : Integrable (2 * X * μ[X | m]) μ
aux₂ : Integrable (HPow.hPow (β := ℕ) μ[X | m] 2) μ
⊢ μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] =ᶠ[ae μ]
    μ[HPow.hPow (β := ℕ) X 2 | m] - 2 * HPow.hPow (β := ℕ) μ[X | m] 2 + HPow.hPow (β := ℕ) μ[X | m] 2
have h : ∀ (ω : Ω)
  (hω₀ :
    μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] ω =
      (μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] | m] + μ[HPow.hPow (β := ℕ) μ[X | m] 2 | m]) ω)
  (hω₁ :
    μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] | m] ω = (μ[HPow.hPow (β := ℕ) X 2 | m] - μ[2 * X * μ[X | m] | m]) ω)
  (hω₂ : μ[2 * X * μ[X | m] | m] ω = (μ[2 * X | m] * μ[X | m]) ω)
  (hω₃ : μ[OfNat.ofNat 2 * X | m] ω = HMul.hMul (α := Ω → ℝ) (OfNat.ofNat 2) μ[X | m] ω),
  μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] ω =
    (μ[HPow.hPow (β := ℕ) X 2 | m] - 2 * HPow.hPow (β := ℕ) μ[X | m] 2 + HPow.hPow (β := ℕ) μ[X | m] 2) ω
Tactic: filter_upwards [condExp_add (m := m) (aux₀.sub aux₁) aux₂, condExp_sub (m := m) aux₀ aux₁,
        condExp_mul_of_stronglyMeasurable_right stronglyMeasurable_condExp aux₁
          ((hX.integrable one_le_two).const_mul _), condExp_ofNat (m := m) 2 X]
        with ω hω₀ hω₁ hω₂ hω₃
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (HPow.hPow (β := ℕ) X 2) μ
aux₁ : Integrable (2 * X * μ[X | m]) μ
aux₂ : Integrable (HPow.hPow (β := ℕ) μ[X | m] 2) μ
ω : Ω
hω₀ :
  μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] ω =
    (μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] | m] + μ[HPow.hPow (β := ℕ) μ[X | m] 2 | m]) ω
hω₁ : μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] | m] ω = (μ[HPow.hPow (β := ℕ) X 2 | m] - μ[2 * X * μ[X | m] | m]) ω
hω₂ : μ[2 * X * μ[X | m] | m] ω = (μ[2 * X | m] * μ[X | m]) ω
hω₃ : μ[OfNat.ofNat 2 * X | m] ω = HMul.hMul (α := Ω → ℝ) (OfNat.ofNat 2) μ[X | m] ω
⊢ μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] ω =
    (μ[HPow.hPow (β := ℕ) X 2 | m] - 2 * HPow.hPow (β := ℕ) μ[X | m] 2 + HPow.hPow (β := ℕ) μ[X | m] 2) ω
have h : OfNat.ofNat 2 * μ[X | m] ω * μ[X | m] ω = 2 * HPow.hPow (β := ℕ) (μ[X | m] ω) 2
Tactic: simp [hω₀, hω₁, hω₂, hω₃,
        condExp_of_stronglyMeasurable hm (stronglyMeasurable_condExp.pow _) aux₂]
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ Var[X; μ | m] =ᶠ[ae μ] μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2
have μ₁ : Var[X; μ | m] = μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m]
Tactic: calc
    Var[X; μ | m]
    _ = μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] := by rw [condVar, sub_sq]
    _ =ᵐ[μ] μ[X ^ 2 | m] - 2 * μ[X | m] ^ 2 + μ[X | m] ^ 2 := by
      have aux₀ : Integrable (X ^ 2) μ := hX.integrable_sq
      have aux₁ : Integrable (2 * X * μ[X | m]) μ := by
        rw [mul_assoc]
        exact (memLp_one_iff_integrable.1 <| hX.condExp.mul hX).const_mul _
      have aux₂ : Integrable (μ[X | m] ^ 2) μ := hX.condExp.integrable_sq
      filter_upwards [condExp_add (m := m) (aux₀.sub aux₁) aux₂, condExp_sub (m := m) aux₀ aux₁,
        condExp_mul_of_stronglyMeasurable_right stronglyMeasurable_condExp aux₁
          ((hX.integrable one_le_two).const_mul _), condExp_ofNat (m := m) 2 X]
        with ω hω₀ hω₁ hω₂ hω₃
      simp [hω₀, hω₁, hω₂, hω₃,
        condExp_of_stronglyMeasurable hm (stronglyMeasurable_condExp.pow _) aux₂]
      simp [mul_assoc, sq]
    _ = μ[X ^ 2 | m] - μ[X | m] ^ 2 := by ring
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
μ₁ : Var[X; μ | m] = μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m]
⊢ Var[X; μ | m] =ᶠ[ae μ] μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2
have μ₂ : μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] =ᶠ[ae μ]
  μ[HPow.hPow (β := ℕ) X 2 | m] - 2 * HPow.hPow (β := ℕ) μ[X | m] 2 + HPow.hPow (β := ℕ) μ[X | m] 2
Tactic: calc
    Var[X; μ | m]
    _ = μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] := by rw [condVar, sub_sq]
    _ =ᵐ[μ] μ[X ^ 2 | m] - 2 * μ[X | m] ^ 2 + μ[X | m] ^ 2 := by
      have aux₀ : Integrable (X ^ 2) μ := hX.integrable_sq
      have aux₁ : Integrable (2 * X * μ[X | m]) μ := by
        rw [mul_assoc]
        exact (memLp_one_iff_integrable.1 <| hX.condExp.mul hX).const_mul _
      have aux₂ : Integrable (μ[X | m] ^ 2) μ := hX.condExp.integrable_sq
      filter_upwards [condExp_add (m := m) (aux₀.sub aux₁) aux₂, condExp_sub (m := m) aux₀ aux₁,
        condExp_mul_of_stronglyMeasurable_right stronglyMeasurable_condExp aux₁
          ((hX.integrable one_le_two).const_mul _), condExp_ofNat (m := m) 2 X]
        with ω hω₀ hω₁ hω₂ hω₃
      simp [hω₀, hω₁, hω₂, hω₃,
        condExp_of_stronglyMeasurable hm (stronglyMeasurable_condExp.pow _) aux₂]
      simp [mul_assoc, sq]
    _ = μ[X ^ 2 | m] - μ[X | m] ^ 2 := by ring
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
μ₁ : Var[X; μ | m] = μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m]
μ₂ :
  μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] =ᶠ[ae μ]
    μ[HPow.hPow (β := ℕ) X 2 | m] - 2 * HPow.hPow (β := ℕ) μ[X | m] 2 + HPow.hPow (β := ℕ) μ[X | m] 2
⊢ Var[X; μ | m] =ᶠ[ae μ] μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2
have μ₃ : μ[HPow.hPow (β := ℕ) X 2 | m] - 2 * HPow.hPow (β := ℕ) μ[X | m] 2 + HPow.hPow (β := ℕ) μ[X | m] 2 =
  μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2
Tactic: calc
    Var[X; μ | m]
    _ = μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] := by rw [condVar, sub_sq]
    _ =ᵐ[μ] μ[X ^ 2 | m] - 2 * μ[X | m] ^ 2 + μ[X | m] ^ 2 := by
      have aux₀ : Integrable (X ^ 2) μ := hX.integrable_sq
      have aux₁ : Integrable (2 * X * μ[X | m]) μ := by
        rw [mul_assoc]
        exact (memLp_one_iff_integrable.1 <| hX.condExp.mul hX).const_mul _
      have aux₂ : Integrable (μ[X | m] ^ 2) μ := hX.condExp.integrable_sq
      filter_upwards [condExp_add (m := m) (aux₀.sub aux₁) aux₂, condExp_sub (m := m) aux₀ aux₁,
        condExp_mul_of_stronglyMeasurable_right stronglyMeasurable_condExp aux₁
          ((hX.integrable one_le_two).const_mul _), condExp_ofNat (m := m) 2 X]
        with ω hω₀ hω₁ hω₂ hω₃
      simp [hω₀, hω₁, hω₂, hω₃,
        condExp_of_stronglyMeasurable hm (stronglyMeasurable_condExp.pow _) aux₂]
      simp [mul_assoc, sq]
    _ = μ[X ^ 2 | m] - μ[X | m] ^ 2 := by ring
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ Var[X; μ | m] ≤ᶠ[ae μ] μ[HPow.hPow (β := ℕ) X 2 | m]
have h : ∀ (ω : Ω) (hω : Var[X; μ | m] ω = (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) ω),
  Var[X; μ | m] ω ≤ μ[HPow.hPow (β := ℕ) X 2 | m] ω
Tactic: filter_upwards [condVar_ae_eq_condExp_sq_sub_sq_condExp hm hX] with ω hω
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
ω : Ω
hω : Var[X; μ | m] ω = μ[HPow.hPow (β := ℕ) X 2 | m] ω - HPow.hPow (β := ℕ) (μ[X | m] ω) 2
⊢ Var[X; μ | m] ω ≤ μ[HPow.hPow (β := ℕ) X 2 | m] ω
have nlinarith : μ[HPow.hPow (β := ℕ) X 2 | m] ω < Var[X; μ | m] ω →
  0 - HPow.hPow (β := ℕ) (μ[X | m] ω) 2 +
        (Var[X; μ | m] ω - (μ[HPow.hPow (β := ℕ) X 2 | m] ω - HPow.hPow (β := ℕ) (μ[X | m] ω) 2)) +
      (μ[HPow.hPow (β := ℕ) X 2 | m] ω - Var[X; μ | m] ω) =
    0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), Var[X; μ | m] x ∂μ + Var[μ[X | m]; μ] =
    ∫ (x : Ω), (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) x ∂μ +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), μ[X | m] x ∂μ) 2)
have e_a : Eq (α := ℝ) (∫ (x : Ω), Var[X; μ | m] x ∂μ)
  (∫ (x : Ω), (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) x ∂μ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
e_a :
  Eq (α := ℝ) (∫ (x : Ω), Var[X; μ | m] x ∂μ)
    (∫ (x : Ω), (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) x ∂μ)
⊢ ∫ (x : Ω), Var[X; μ | m] x ∂μ + Var[μ[X | m]; μ] =
    ∫ (x : Ω), (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) x ∂μ +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), μ[X | m] x ∂μ) 2)
have e_a₁ : Var[μ[X | m]; μ] =
  ∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), μ[X | m] x ∂μ) 2
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) x ∂μ +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), μ[X | m] x ∂μ) 2) =
    HSub.hSub (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ) +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)
have rw : Integrable (HPow.hPow (β := ℕ) μ[X | m] 2) μ
Tactic: rw [integral_sub' integrable_condExp, integral_condExp hm, integral_condExp hm]
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ HSub.hSub (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ) +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2) =
    Var[X; μ]
have rw : HSub.hSub (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ) +
    (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2) =
  ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
Tactic: rw [variance_eq_sub hX]
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), Var[X; μ | m] x ∂μ + Var[μ[X | m]; μ] = Var[X; μ]
have μ₁ : ∫ (x : Ω), Var[X; μ | m] x ∂μ + Var[μ[X | m]; μ] =
  ∫ (x : Ω), (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) x ∂μ +
    (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), μ[X | m] x ∂μ) 2)
Tactic: calc
    μ[Var[X; μ | m]] + Var[μ[X | m]; μ]
    _ = μ[(μ[X ^ 2 | m] - μ[X | m] ^ 2 : Ω → ℝ)] + (μ[μ[X | m] ^ 2] - μ[μ[X | m]] ^ 2) := by
      congr 1
      · exact integral_congr_ae <| condVar_ae_eq_condExp_sq_sub_sq_condExp hm hX
      · exact variance_eq_sub hX.condExp
    _ = μ[X ^ 2] - μ[μ[X | m] ^ 2] + (μ[μ[X | m] ^ 2] - μ[X] ^ 2) := by
      rw [integral_sub' integrable_condExp, integral_condExp hm, integral_condExp hm]
      exact hX.condExp.integrable_sq
    _ = Var[X; μ] := by rw [variance_eq_sub hX]; ring
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
μ₁ :
  ∫ (x : Ω), Var[X; μ | m] x ∂μ + Var[μ[X | m]; μ] =
    ∫ (x : Ω), (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) x ∂μ +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), μ[X | m] x ∂μ) 2)
⊢ ∫ (x : Ω), Var[X; μ | m] x ∂μ + Var[μ[X | m]; μ] = Var[X; μ]
have μ₂ : ∫ (x : Ω), (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) x ∂μ +
    (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), μ[X | m] x ∂μ) 2) =
  HSub.hSub (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ) +
    (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)
Tactic: calc
    μ[Var[X; μ | m]] + Var[μ[X | m]; μ]
    _ = μ[(μ[X ^ 2 | m] - μ[X | m] ^ 2 : Ω → ℝ)] + (μ[μ[X | m] ^ 2] - μ[μ[X | m]] ^ 2) := by
      congr 1
      · exact integral_congr_ae <| condVar_ae_eq_condExp_sq_sub_sq_condExp hm hX
      · exact variance_eq_sub hX.condExp
    _ = μ[X ^ 2] - μ[μ[X | m] ^ 2] + (μ[μ[X | m] ^ 2] - μ[X] ^ 2) := by
      rw [integral_sub' integrable_condExp, integral_condExp hm, integral_condExp hm]
      exact hX.condExp.integrable_sq
    _ = Var[X; μ] := by rw [variance_eq_sub hX]; ring
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
μ₁ :
  ∫ (x : Ω), Var[X; μ | m] x ∂μ + Var[μ[X | m]; μ] =
    ∫ (x : Ω), (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) x ∂μ +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), μ[X | m] x ∂μ) 2)
μ₂ :
  ∫ (x : Ω), (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) x ∂μ +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), μ[X | m] x ∂μ) 2) =
    HSub.hSub (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ) +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)
⊢ ∫ (x : Ω), Var[X; μ | m] x ∂μ + Var[μ[X | m]; μ] = Var[X; μ]
have μ₃ : HSub.hSub (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ) +
    (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2) =
  Var[X; μ]
Tactic: calc
    μ[Var[X; μ | m]] + Var[μ[X | m]; μ]
    _ = μ[(μ[X ^ 2 | m] - μ[X | m] ^ 2 : Ω → ℝ)] + (μ[μ[X | m] ^ 2] - μ[μ[X | m]] ^ 2) := by
      congr 1
      · exact integral_congr_ae <| condVar_ae_eq_condExp_sq_sub_sq_condExp hm hX
      · exact variance_eq_sub hX.condExp
    _ = μ[X ^ 2] - μ[μ[X | m] ^ 2] + (μ[μ[X | m] ^ 2] - μ[X] ^ 2) := by
      rw [integral_sub' integrable_condExp, integral_condExp hm, integral_condExp hm]
      exact hX.condExp.integrable_sq
    _ = Var[X; μ] := by rw [variance_eq_sub hX]; ring
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
⊢ Var[X; μ | ⊥] =ᶠ[ae μ] fun (x : Ω) ↦ ⨍ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ⨍ (ω' : Ω), X ω' ∂μ) 2 ∂μ
have inl : condVar (m₀ := m₀) ⊥ X 0 =ᶠ[ae (F := Measure Ω) 0] fun (x : Ω) ↦
  ⨍ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ⨍ (ω' : Ω), X ω' ∂0) 2 ∂0
Tactic: obtain rfl | hμ := eq_zero_or_neZero μ
Cleared hypotheses: μ
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inl :
  condVar (m₀ := m₀) ⊥ X 0 =ᶠ[ae (F := Measure Ω) 0] fun (x : Ω) ↦
    ⨍ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ⨍ (ω' : Ω), X ω' ∂0) 2 ∂0
⊢ Var[X; μ | ⊥] =ᶠ[ae μ] fun (x : Ω) ↦ ⨍ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ⨍ (ω' : Ω), X ω' ∂μ) 2 ∂μ
have inr : ∀ (hμ : NeZero μ), Var[X; μ | ⊥] =ᶠ[ae μ] fun (x : Ω) ↦ ⨍ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ⨍ (ω' : Ω), X ω' ∂μ) 2 ∂μ
Tactic: obtain rfl | hμ := eq_zero_or_neZero μ
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ : MeasurableSpace Ω
X : Ω → ℝ
⊢ condVar (m₀ := m₀) ⊥ X 0 =ᶠ[ae (F := Measure Ω) 0] fun (x : Ω) ↦
    ⨍ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ⨍ (ω' : Ω), X ω' ∂0) 2 ∂0
have inl : condVar (m₀ := m₀) ⊥ X 0 =ᶠ[⊥] fun (x : Ω) ↦ ⨍ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ⨍ (ω' : Ω), X ω' ∂0) 2 ∂0
Tactic: rw [ae_zero]
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
⊢ μ[HPow.hPow (β := ℕ) (c • X - μ[c • X | m]) 2 | m] =ᶠ[ae μ]
    μ[HPow.hPow (β := ℕ) c 2 • HPow.hPow (β := ℕ) (X - μ[X | m]) 2 | m]
have refine : HPow.hPow (β := ℕ) (c • X - μ[c • X | m]) 2 =ᶠ[ae μ] HPow.hPow (β := ℕ) c 2 • HPow.hPow (β := ℕ) (X - μ[X | m]) 2
Tactic: refine condExp_congr_ae ?_
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
⊢ HPow.hPow (β := ℕ) (c • X - μ[c • X | m]) 2 =ᶠ[ae μ] HPow.hPow (β := ℕ) c 2 • HPow.hPow (β := ℕ) (X - μ[X | m]) 2
have h : ∀ (ω : Ω) (hω : μ[c • X | m] ω = (c • μ[X | m]) ω),
  HPow.hPow (β := ℕ) (c • X - μ[c • X | m]) 2 ω = (HPow.hPow (β := ℕ) c 2 • HPow.hPow (β := ℕ) (X - μ[X | m]) 2) ω
Tactic: filter_upwards [condExp_smul (m := m) c X] with ω hω
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
⊢ Var[c • X; μ | m] =ᶠ[ae μ] HPow.hPow (β := ℕ) c 2 • Var[X; μ | m]
have μ₁ : Var[c • X; μ | m] =ᶠ[ae μ] μ[HPow.hPow (β := ℕ) c 2 • HPow.hPow (β := ℕ) (X - μ[X | m]) 2 | m]
Tactic: calc
    Var[c • X; μ | m]
    _ =ᵐ[μ] μ[c ^ 2 • (X - μ[X | m]) ^ 2 | m] := by
      rw [condVar]
      refine condExp_congr_ae ?_
      filter_upwards [condExp_smul (m := m) c X] with ω hω
      simp [hω, ← mul_sub, mul_pow]
    _ =ᵐ[μ] c ^ 2 • Var[X; μ | m] := condExp_smul ..
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
⊢ Var[-X; μ | m] =ᶠ[ae μ] Var[X; μ | m]
have refine : HPow.hPow (β := ℕ) (-X - μ[-X | m]) 2 =ᶠ[ae μ] HPow.hPow (β := ℕ) (X - μ[X | m]) 2
Tactic: refine condExp_congr_ae ?_
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
⊢ HPow.hPow (β := ℕ) (-X - μ[-X | m]) 2 =ᶠ[ae μ] HPow.hPow (β := ℕ) (X - μ[X | m]) 2
have h : ∀ (ω : Ω) (hω : μ[-X | m] ω = (-μ[X | m]) ω),
  HPow.hPow (β := ℕ) (-X - μ[-X | m]) 2 ω = HPow.hPow (β := ℕ) (X - μ[X | m]) 2 ω
Tactic: filter_upwards [condExp_neg (m := m) X] with ω hω
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
ω : Ω
hω : μ[-X | m] ω = (-μ[X | m]) ω
⊢ HPow.hPow (β := ℕ) (-X - μ[-X | m]) 2 ω = HPow.hPow (β := ℕ) (X - μ[X | m]) 2 ω
have h : HPow.hPow (β := ℕ) (-X ω + μ[X | m] ω) 2 = HPow.hPow (β := ℕ) (X ω - μ[X | m] ω) 2
Tactic: simp [hω]
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
⊢ μ[f | m₂] =ᶠ[ae μ] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ
have pos : ∀ (hfint : Integrable f μ), μ[f | m₂] =ᶠ[ae μ] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ
Tactic: by_cases hfint : Integrable f μ
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
pos : ∀ (hfint : Integrable f μ), μ[f | m₂] =ᶠ[ae μ] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ
⊢ μ[f | m₂] =ᶠ[ae μ] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ
have neg : ∀ (hfint : ¬Integrable f μ), μ[f | m₂] =ᶠ[ae μ] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ
Tactic: by_cases hfint : Integrable f μ
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : ¬Integrable f μ
⊢ μ[f | m₂] =ᶠ[ae μ] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ
have neg : EventuallyEq.{u_1, u_2} (β := E) (ae μ) 0 0
Tactic: rw [condExp_of_not_integrable hfint, integral_undef hfint]
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : Integrable f μ
⊢ μ[f | m₂] =ᶠ[ae μ] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ
have pos : ∀ (s : Set Ω) (hms : MeasurableSet s) (hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, ∫ (x : Ω), f x ∂μ ∂μ) (∫ (x : Ω) in s, f x ∂μ)
Tactic: refine (ae_eq_condExp_of_forall_setIntegral_eq hle₂ hfint
    (fun s _ hs ↦ integrableOn_const hs.ne) (fun s hms hs => ?_)
      stronglyMeasurable_const.aestronglyMeasurable).symm
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : Integrable f μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : Ω) in s, ∫ (x : Ω), f x ∂μ ∂μ) (∫ (x : Ω) in s, f x ∂μ)
have pos : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ
Tactic: rw [setIntegral_const]
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : Integrable f μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ
have pos : ∀ (hfint : MemLp f 1 μ) (s : Set Ω) (hms : MeasurableSet s)
  (hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ
Tactic: rw [← memLp_one_iff_integrable] at hfint
Cleared hypotheses: hfint, s, hms, hs
-- Lean 4 proof step from Mathlib.Probability.ConditionalExpectation (goal)
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ
have pos : AEStronglyMeasurable f μ
Tactic: refine MemLp.induction_stronglyMeasurable hle₁ ENNReal.one_ne_top _ ?_ ?_ ?_ ?_ hfint ?_