awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.negPart =
    μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) + s.toJordanDecomposition.negPart.singularPart μ
have h : s.toJordanDecomposition.negPart =
  s.toJordanDecomposition.negPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ)
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : SignedMeasure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)) ⟂ₘ
    t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)
have htμ₁ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
Tactic: rw [mutuallySingular_ennreal_iff, totalVariation_mutuallySingular_iff,
    VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure] at htμ
Cleared hypotheses: htμ
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
⊢ IsFiniteMeasure (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
have this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
Tactic: haveI := isFiniteMeasure_withDensity_ofReal hfi.2
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
⊢ IsFiniteMeasure (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x))
have this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
Tactic: haveI := isFiniteMeasure_withDensity_ofReal hfi.neg.2
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
⊢ s.toJordanDecomposition =
    { posPart := t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x),
      negPart := t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x),
      posPart_finite := ⋯, negPart_finite := ⋯, mutuallySingular := ⋯ }
have this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
Tactic: haveI := isFiniteMeasure_withDensity_ofReal hfi.2
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
⊢ s.toJordanDecomposition =
    { posPart := t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x),
      negPart := t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x),
      posPart_finite := ⋯, negPart_finite := ⋯, mutuallySingular := ⋯ }
have this₁ : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
Tactic: haveI := isFiniteMeasure_withDensity_ofReal hfi.neg.2
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
⊢ s.toJordanDecomposition =
    { posPart := t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x),
      negPart := t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x),
      posPart_finite := ⋯, negPart_finite := ⋯, mutuallySingular := ⋯ }
have refine : s =
  { posPart := t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x),
      negPart := t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x),
      posPart_finite := sorry, negPart_finite := sorry, mutuallySingular := sorry }.toSignedMeasure
Tactic: refine toJordanDecomposition_eq ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
⊢ s =
    { posPart := t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x),
        negPart := t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x),
        posPart_finite := ⋯, negPart_finite := ⋯, mutuallySingular := ⋯ }.toSignedMeasure
have simp_rw : t + μ.withDensityᵥ f =
  (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
    (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure
Tactic: simp_rw [JordanDecomposition.toSignedMeasure, hadd]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
⊢ t + μ.withDensityᵥ f =
    (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
      (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure
have h : ∀ (i : Set α) (hi : MeasurableSet i),
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑((t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
Tactic: ext i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
⊢ (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑((t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
have h : (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
  (↑(t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure : Set α → ℝ)
      i -
    (↑(t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure : Set α → ℝ)
      i
Tactic: rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
      toSignedMeasure_apply_measurable hi, measureReal_add_apply, measureReal_add_apply,
      add_sub_add_comm, ← toSignedMeasure_apply_measurable hi,
      ← toSignedMeasure_apply_measurable hi, ← VectorMeasure.sub_apply,
      ← JordanDecomposition.toSignedMeasure, toSignedMeasure_toJordanDecomposition,
      VectorMeasure.add_apply, ← toSignedMeasure_apply_measurable hi,
      ← toSignedMeasure_apply_measurable hi,
      withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part hfi,
      VectorMeasure.sub_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
h :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑(t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure : Set α → ℝ)
        i -
      (↑(t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure :
          Set α → ℝ)
        i
⊢ (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑((t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
have h₁ : (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
  (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
    (↑(t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure : Set α → ℝ)
      i
Tactic: rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
      toSignedMeasure_apply_measurable hi, measureReal_add_apply, measureReal_add_apply,
      add_sub_add_comm, ← toSignedMeasure_apply_measurable hi,
      ← toSignedMeasure_apply_measurable hi, ← VectorMeasure.sub_apply,
      ← JordanDecomposition.toSignedMeasure, toSignedMeasure_toJordanDecomposition,
      VectorMeasure.add_apply, ← toSignedMeasure_apply_measurable hi,
      ← toSignedMeasure_apply_measurable hi,
      withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part hfi,
      VectorMeasure.sub_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
h :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑(t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure : Set α → ℝ)
        i -
      (↑(t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure :
          Set α → ℝ)
        i
h₁ :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (↑(t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure :
          Set α → ℝ)
        i
⊢ (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑((t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
have h₂ : (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
  (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
    (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i
Tactic: rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
      toSignedMeasure_apply_measurable hi, measureReal_add_apply, measureReal_add_apply,
      add_sub_add_comm, ← toSignedMeasure_apply_measurable hi,
      ← toSignedMeasure_apply_measurable hi, ← VectorMeasure.sub_apply,
      ← JordanDecomposition.toSignedMeasure, toSignedMeasure_toJordanDecomposition,
      VectorMeasure.add_apply, ← toSignedMeasure_apply_measurable hi,
      ← toSignedMeasure_apply_measurable hi,
      withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part hfi,
      VectorMeasure.sub_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
h :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑(t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure : Set α → ℝ)
        i -
      (↑(t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure :
          Set α → ℝ)
        i
h₁ :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (↑(t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure :
          Set α → ℝ)
        i
h₂ :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i
⊢ (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑((t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
have h₃ : (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
  t.toJordanDecomposition.posPart.real i + (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
    (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i
Tactic: rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
      toSignedMeasure_apply_measurable hi, measureReal_add_apply, measureReal_add_apply,
      add_sub_add_comm, ← toSignedMeasure_apply_measurable hi,
      ← toSignedMeasure_apply_measurable hi, ← VectorMeasure.sub_apply,
      ← JordanDecomposition.toSignedMeasure, toSignedMeasure_toJordanDecomposition,
      VectorMeasure.add_apply, ← toSignedMeasure_apply_measurable hi,
      ← toSignedMeasure_apply_measurable hi,
      withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part hfi,
      VectorMeasure.sub_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
h :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑(t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure : Set α → ℝ)
        i -
      (↑(t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure :
          Set α → ℝ)
        i
h₁ :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (↑(t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure :
          Set α → ℝ)
        i
h₂ :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i
h₃ :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    t.toJordanDecomposition.posPart.real i + (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i
⊢ (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑((t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
have h₄ : (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
  t.toJordanDecomposition.posPart.real i + (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
    (t.toJordanDecomposition.negPart.real i + (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i)
Tactic: rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
      toSignedMeasure_apply_measurable hi, measureReal_add_apply, measureReal_add_apply,
      add_sub_add_comm, ← toSignedMeasure_apply_measurable hi,
      ← toSignedMeasure_apply_measurable hi, ← VectorMeasure.sub_apply,
      ← JordanDecomposition.toSignedMeasure, toSignedMeasure_toJordanDecomposition,
      VectorMeasure.add_apply, ← toSignedMeasure_apply_measurable hi,
      ← toSignedMeasure_apply_measurable hi,
      withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part hfi,
      VectorMeasure.sub_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
i : Set α
hi : MeasurableSet i
h :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑(t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure : Set α → ℝ)
        i -
      (↑(t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure :
          Set α → ℝ)
        i
h₁ :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (↑(t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure :
          Set α → ℝ)
        i
h₂ :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i
h₃ :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    t.toJordanDecomposition.posPart.real i + (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i
h₄ :
  (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    t.toJordanDecomposition.posPart.real i + (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (t.toJordanDecomposition.negPart.real i + (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i)
⊢ (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
    (↑((t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).toSignedMeasure -
            (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).toSignedMeasure) :
        Set α → ℝ)
      i
have h₅ : (↑(t + μ.withDensityᵥ f) : Set α → ℝ) i =
  t.toJordanDecomposition.posPart.real i - t.toJordanDecomposition.negPart.real i +
    ((μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)).real i -
      (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)).real i)
Tactic: rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
      toSignedMeasure_apply_measurable hi, measureReal_add_apply, measureReal_add_apply,
      add_sub_add_comm, ← toSignedMeasure_apply_measurable hi,
      ← toSignedMeasure_apply_measurable hi, ← VectorMeasure.sub_apply,
      ← JordanDecomposition.toSignedMeasure, toSignedMeasure_toJordanDecomposition,
      VectorMeasure.add_apply, ← toSignedMeasure_apply_measurable hi,
      ← toSignedMeasure_apply_measurable hi,
      withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part hfi,
      VectorMeasure.sub_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ s.HaveLebesgueDecomposition μ
have htμ₁ : t.totalVariation ⟂ₘ μ.toENNRealVectorMeasure.ennrealToMeasure
Tactic: rw [mutuallySingular_ennreal_iff] at htμ
Cleared hypotheses: htμ, hadd, htμ'
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
htμ : t.totalVariation ⟂ₘ μ.toENNRealVectorMeasure.ennrealToMeasure
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ s.HaveLebesgueDecomposition μ
have htμ₁ : t.totalVariation ⟂ₘ Equiv.toFun VectorMeasure.equivMeasure (Equiv.invFun VectorMeasure.equivMeasure μ)
Tactic: change _ ⟂ₘ VectorMeasure.equivMeasure.toFun (VectorMeasure.equivMeasure.invFun μ) at htμ
Cleared hypotheses: htμ
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ : t.totalVariation ⟂ₘ Equiv.toFun VectorMeasure.equivMeasure (Equiv.invFun VectorMeasure.equivMeasure μ)
⊢ s.HaveLebesgueDecomposition μ
have htμ₁ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
Tactic: rw [VectorMeasure.equivMeasure.right_inv, totalVariation_mutuallySingular_iff] at htμ
Cleared hypotheses: htμ
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
hfi : Integrable f μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ
have h : Measurable (α := α) (β := ℝ≥0∞) (t.toJordanDecomposition.posPart, fun (x : α) ↦ ENNReal.ofReal (f x)).2 ∧
  (t.toJordanDecomposition.posPart, fun (x : α) ↦ ENNReal.ofReal (f x)).1 ⟂ₘ μ ∧
    s.toJordanDecomposition.posPart =
      (t.toJordanDecomposition.posPart, fun (x : α) ↦ ENNReal.ofReal (f x)).1 +
        μ.withDensity (t.toJordanDecomposition.posPart, fun (x : α) ↦ ENNReal.ofReal (f x)).2
Tactic: use ⟨t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)⟩