awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ⟂ₘ μ
⊢ 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
have h : 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: refine ⟨hf.ennreal_ofReal, htμ.1, ?_⟩
-- 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 =
    (t.toJordanDecomposition.posPart, fun (x : α) ↦ ENNReal.ofReal (f x)).1 +
      μ.withDensity (t.toJordanDecomposition.posPart, fun (x : α) ↦ ENNReal.ofReal (f x)).2
have h : { 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 : JordanDecomposition α }.posPart =
  (t.toJordanDecomposition.posPart, fun (x : α) ↦ ENNReal.ofReal (f x)).1 +
    μ.withDensity (t.toJordanDecomposition.posPart, fun (x : α) ↦ ENNReal.ofReal (f x)).2
Tactic: rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]
-- 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.negPart.HaveLebesgueDecomposition μ
have h : Measurable (α := α) (β := ℝ≥0∞) (t.toJordanDecomposition.negPart, fun (x : α) ↦ ENNReal.ofReal (-f x)).2 ∧
  (t.toJordanDecomposition.negPart, fun (x : α) ↦ ENNReal.ofReal (-f x)).1 ⟂ₘ μ ∧
    s.toJordanDecomposition.negPart =
      (t.toJordanDecomposition.negPart, fun (x : α) ↦ ENNReal.ofReal (-f x)).1 +
        μ.withDensity (t.toJordanDecomposition.negPart, fun (x : α) ↦ ENNReal.ofReal (-f x)).2
Tactic: use ⟨t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)⟩
-- 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 ⟂ₘ μ
⊢ Measurable (α := α) (β := ℝ≥0∞) (t.toJordanDecomposition.negPart, fun (x : α) ↦ ENNReal.ofReal (-f x)).2 ∧
    (t.toJordanDecomposition.negPart, fun (x : α) ↦ ENNReal.ofReal (-f x)).1 ⟂ₘ μ ∧
      s.toJordanDecomposition.negPart =
        (t.toJordanDecomposition.negPart, fun (x : α) ↦ ENNReal.ofReal (-f x)).1 +
          μ.withDensity (t.toJordanDecomposition.negPart, fun (x : α) ↦ ENNReal.ofReal (-f x)).2
have h : s.toJordanDecomposition.negPart =
  (t.toJordanDecomposition.negPart, fun (x : α) ↦ ENNReal.ofReal (-f x)).1 +
    μ.withDensity (t.toJordanDecomposition.negPart, fun (x : α) ↦ ENNReal.ofReal (-f x)).2
Tactic: refine ⟨hf.neg.ennreal_ofReal, htμ.2, ?_⟩
-- 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.negPart =
    (t.toJordanDecomposition.negPart, fun (x : α) ↦ ENNReal.ofReal (-f x)).1 +
      μ.withDensity (t.toJordanDecomposition.negPart, fun (x : α) ↦ ENNReal.ofReal (-f x)).2
have h : { 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 : JordanDecomposition α }.negPart =
  (t.toJordanDecomposition.negPart, fun (x : α) ↦ ENNReal.ofReal (-f x)).1 +
    μ.withDensity (t.toJordanDecomposition.negPart, fun (x : α) ↦ ENNReal.ofReal (-f x)).2
Tactic: rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]
-- 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
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
⊢ s.HaveLebesgueDecomposition μ
have pos : ∀ (hfi : Integrable f μ), s.HaveLebesgueDecomposition μ
Tactic: by_cases hfi : Integrable f μ
-- 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
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
pos : ∀ (hfi : Integrable f μ), s.HaveLebesgueDecomposition μ
⊢ s.HaveLebesgueDecomposition μ
have neg : ∀ (hfi : ¬Integrable f μ), s.HaveLebesgueDecomposition μ
Tactic: by_cases hfi : Integrable f μ
-- 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
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : ¬Integrable f μ
⊢ s.HaveLebesgueDecomposition μ
have hadd₁ : s = t
Tactic: rw [withDensityᵥ, dif_neg hfi, add_zero] at hadd
Cleared hypotheses: hadd, hfi
-- 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
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ s.HaveLebesgueDecomposition μ
have neg : s = t + μ.withDensityᵥ 0
Tactic: refine haveLebesgueDecomposition_mk' μ measurable_zero (integrable_zero _ _ μ) 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
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ s = t + μ.withDensityᵥ 0
have neg : s = t + 0
Tactic: rwa [withDensityᵥ_zero, add_zero]
-- 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
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ t = s.singularPart μ
have htμ₁ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
Tactic: rw [mutuallySingular_ennreal_iff, totalVariation_mutuallySingular_iff,
    VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure] at htμ
Cleared hypotheses: htμ, hadd, htμ'
-- 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.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ t = s.singularPart μ
have rw : t.toJordanDecomposition.posPart.toSignedMeasure - t.toJordanDecomposition.negPart.toSignedMeasure =
  (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
Tactic: rw [singularPart, ← t.toSignedMeasure_toJordanDecomposition,
    JordanDecomposition.toSignedMeasure]
-- 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.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ t.toJordanDecomposition.posPart.toSignedMeasure - t.toJordanDecomposition.negPart.toSignedMeasure =
    (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have e_a : t.toJordanDecomposition.posPart = s.toJordanDecomposition.posPart.singularPart μ
Tactic: congr
-- 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.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
e_a : t.toJordanDecomposition.posPart = s.toJordanDecomposition.posPart.singularPart μ
⊢ t.toJordanDecomposition.posPart.toSignedMeasure - t.toJordanDecomposition.negPart.toSignedMeasure =
    (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have e_a₁ : t.toJordanDecomposition.negPart = s.toJordanDecomposition.negPart.singularPart μ
Tactic: congr
-- 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.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ t.toJordanDecomposition.posPart = s.toJordanDecomposition.posPart.singularPart μ
have hfpos : Measurable (β := ℝ≥0∞) fun (x : α) ↦ ENNReal.ofReal (f x)
Tactic: have hfpos : Measurable fun x => ENNReal.ofReal (f x) := by fun_prop
-- 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.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
hfpos : Measurable (β := ℝ≥0∞) fun (x : α) ↦ ENNReal.ofReal (f x)
⊢ t.toJordanDecomposition.posPart = s.toJordanDecomposition.posPart.singularPart μ
have e_a : s.toJordanDecomposition.posPart = t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)
Tactic: refine eq_singularPart hfpos htμ.1 ?_
-- 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.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
hfpos : Measurable (β := ℝ≥0∞) fun (x : α) ↦ ENNReal.ofReal (f x)
⊢ s.toJordanDecomposition.posPart = t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)
have e_a : { 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 : JordanDecomposition α }.posPart =
  t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)
Tactic: rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]
-- 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.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
⊢ t.toJordanDecomposition.negPart = s.toJordanDecomposition.negPart.singularPart μ
have hfneg : Measurable (β := ℝ≥0∞) fun (x : α) ↦ ENNReal.ofReal (-f x)
Tactic: have hfneg : Measurable fun x => ENNReal.ofReal (-f x) := by fun_prop
-- 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.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
hfneg : Measurable (β := ℝ≥0∞) fun (x : α) ↦ ENNReal.ofReal (-f x)
⊢ t.toJordanDecomposition.negPart = s.toJordanDecomposition.negPart.singularPart μ
have e_a : s.toJordanDecomposition.negPart = t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)
Tactic: refine eq_singularPart hfneg htμ.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.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
hfneg : Measurable (β := ℝ≥0∞) fun (x : α) ↦ ENNReal.ofReal (-f x)
⊢ s.toJordanDecomposition.negPart = t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)
have e_a : { 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 : JordanDecomposition α }.negPart =
  t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)
Tactic: rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
⊢ t = s.singularPart μ
have pos : ∀ (hfi : Integrable f μ), t = s.singularPart μ
Tactic: by_cases hfi : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
pos : ∀ (hfi : Integrable f μ), t = s.singularPart μ
⊢ t = s.singularPart μ
have neg : ∀ (hfi : ¬Integrable f μ), t = s.singularPart μ
Tactic: by_cases hfi : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : Integrable f μ
⊢ t = s.singularPart μ
have pos : s = t + μ.withDensityᵥ (AEStronglyMeasurable.mk f sorry)
Tactic: refine eq_singularPart' t hfi.1.measurable_mk (hfi.congr hfi.1.ae_eq_mk) htμ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : Integrable f μ
⊢ s = t + μ.withDensityᵥ (AEStronglyMeasurable.mk f ⋯)
have h : μ.withDensityᵥ (AEStronglyMeasurable.mk f sorry) = μ.withDensityᵥ f
Tactic: convert! hadd using 2
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
hfi : ¬Integrable f μ
⊢ t = s.singularPart μ
have hadd₁ : s = t
Tactic: rw [withDensityᵥ, dif_neg hfi, add_zero] at hadd
Cleared hypotheses: hadd, hfi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ t = s.singularPart μ
have neg : s = t + μ.withDensityᵥ 0
Tactic: refine eq_singularPart' t measurable_zero (integrable_zero _ _ μ) htμ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
⊢ s = t + μ.withDensityᵥ 0
have neg : s = t + 0
Tactic: rwa [withDensityᵥ_zero, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ singularPart 0 μ = 0
have refine : 0 = HAdd.hAdd (α := SignedMeasure α) 0 (μ.withDensityᵥ 0)
Tactic: refine (eq_singularPart 0 0 VectorMeasure.MutuallySingular.zero_left ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ 0 = HAdd.hAdd (α := SignedMeasure α) 0 (μ.withDensityᵥ 0)
have rw : Eq (α := SignedMeasure α) 0 (μ.withDensityᵥ 0)
Tactic: rw [zero_add, withDensityᵥ_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
rw : Eq (α := SignedMeasure α) 0 (μ.withDensityᵥ 0)
⊢ 0 = HAdd.hAdd (α := SignedMeasure α) 0 (μ.withDensityᵥ 0)
have rw₁ : Eq.{u_1 + 1} (α := SignedMeasure α) 0 0
Tactic: rw [zero_add, withDensityᵥ_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
⊢ (r • s).singularPart μ = r • s.singularPart μ
have rw : ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
  (r • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    (r • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
Tactic: rw [singularPart, singularPart, smul_sub, ← toSignedMeasure_smul, ← toSignedMeasure_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have a : ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
a : ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have a₁ : ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure
have a : (r • s).toJordanDecomposition.posPart.singularPart μ
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
| (r • s).toJordanDecomposition.posPart.singularPart μ
have a : r • s.toJordanDecomposition.posPart.singularPart μ
Tactic: rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
| (r • s).toJordanDecomposition.posPart.singularPart μ
have a : (r • s.toJordanDecomposition).posPart.singularPart μ
Tactic: · rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
a : (r • s.toJordanDecomposition).posPart.singularPart μ
| (r • s).toJordanDecomposition.posPart.singularPart μ
have a₁ : (r • s.toJordanDecomposition.posPart).singularPart μ
Tactic: · rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
a : (r • s.toJordanDecomposition).posPart.singularPart μ
a₁ : (r • s.toJordanDecomposition.posPart).singularPart μ
| (r • s).toJordanDecomposition.posPart.singularPart μ
have a₂ : r • s.toJordanDecomposition.posPart.singularPart μ
Tactic: · rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure
have a : (r • s).toJordanDecomposition.posPart.singularPart μ
Tactic: congr
      · rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
| ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have a : (r • s).toJordanDecomposition.negPart.singularPart μ
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
| (r • s).toJordanDecomposition.negPart.singularPart μ
have a : r • s.toJordanDecomposition.negPart.singularPart μ
Tactic: rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
| ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have a : r • s.toJordanDecomposition.negPart.singularPart μ
Tactic: congr
      rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
| ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have a : (r • s).toJordanDecomposition.negPart.singularPart μ
Tactic: · congr
      rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart, singularPart_smul]