awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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
htμ₁ : t.totalVariation ⟂ₘ μ.toENNRealVectorMeasure.ennrealToMeasure
hadd₁ : s = t + μ.withDensityᵥ f
⊢ t ⟂ᵥ μ.toENNRealVectorMeasure

Tactic:
rw [mutuallySingular_ennreal_iff] at htμ

Premises used: MeasureTheory.SignedMeasure.mutuallySingular_ennreal_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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
⊢ t.totalVariation ⟂ₘ Equiv.toFun VectorMeasure.equivMeasure (Equiv.invFun VectorMeasure.equivMeasure μ)

Tactic:
change _ ⟂ₘ VectorMeasure.equivMeasure.toFun (VectorMeasure.equivMeasure.invFun μ) at htμ

Premises used: Equiv.toFun, Equiv.invFun, MeasureTheory.VectorMeasure.equivMeasure
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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 μ)
⊢ t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ

Tactic:
rw [VectorMeasure.equivMeasure.right_inv, totalVariation_mutuallySingular_iff] at htμ

Premises used: Equiv.right_inv, MeasureTheory.SignedMeasure.totalVariation_mutuallySingular_iff, MeasureTheory.VectorMeasure.equivMeasure
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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 ⟂ₘ μ
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
⊢ s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ

Tactic:
use ⟨t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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

Tactic:
⟨hf.ennreal_ofReal, htμ.1, ?_⟩

Premises used: Measurable.ennreal_ofReal, And.left, And.intro
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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 ⟂ₘ μ
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
⊢ 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:
refine ⟨hf.ennreal_ofReal, htμ.1, ?_⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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 ⟂ₘ μ
h 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 := ⋯, negPart_finite := ⋯, mutuallySingular := ⋯ : JordanDecomposition α }.posPart =
    (t.toJordanDecomposition.posPart, fun (x : α) ↦ ENNReal.ofReal (f x)).1 +
      μ.withDensity (t.toJordanDecomposition.posPart, fun (x : α) ↦ ENNReal.ofReal (f x)).2
⊢ 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:
rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]

Premises used: MeasureTheory.SignedMeasure.toJordanDecomposition_eq_of_eq_add_withDensity
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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 ⟂ₘ μ
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
⊢ s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ

Tactic:
use ⟨t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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

Tactic:
⟨hf.neg.ennreal_ofReal, htμ.2, ?_⟩

Premises used: Measurable.ennreal_ofReal, Measurable.neg, And.right, And.intro
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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 ⟂ₘ μ
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
⊢ 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:
refine ⟨hf.neg.ennreal_ofReal, htμ.2, ?_⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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 ⟂ₘ μ
h 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 := ⋯, negPart_finite := ⋯, mutuallySingular := ⋯ : JordanDecomposition α }.negPart =
    (t.toJordanDecomposition.negPart, fun (x : α) ↦ ENNReal.ofReal (-f x)).1 +
      μ.withDensity (t.toJordanDecomposition.negPart, fun (x : α) ↦ ENNReal.ofReal (-f x)).2
⊢ 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:
rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]

Premises used: MeasureTheory.SignedMeasure.toJordanDecomposition_eq_of_eq_add_withDensity
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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.HaveLebesgueDecomposition μ

Tactic:
refine
    { posPart := by
        use ⟨t.toJordanDecomposition.posPart, fun x => ENNReal.ofReal (f x)⟩
        refine ⟨hf.ennreal_ofReal, htμ.1, ?_⟩
        rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]
      negPart := by
        use ⟨t.toJordanDecomposition.negPart, fun x => ENNReal.ofReal (-f x)⟩
        refine ⟨hf.neg.ennreal_ofReal, htμ.2, ?_⟩
        rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd] }
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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 μ
neg : ∀ (hfi : ¬Integrable f μ), s.HaveLebesgueDecomposition μ
⊢ s.HaveLebesgueDecomposition μ

Tactic:
by_cases hfi : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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 μ

Tactic:
haveLebesgueDecomposition_mk' μ hf hfi htμ hadd

Premises used: _private.0.MeasureTheory.SignedMeasure.haveLebesgueDecomposition_mk'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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 μ

Tactic:
exact haveLebesgueDecomposition_mk' μ hf hfi htμ hadd

Premises used: _private.0.MeasureTheory.SignedMeasure.haveLebesgueDecomposition_mk'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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 = t

Tactic:
rw [withDensityᵥ, dif_neg hfi, add_zero] at hadd

Premises used: MeasureTheory.Measure.withDensityᵥ, dif_neg, add_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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 μ
hadd₁ : s = t
⊢ ¬Integrable f μ

Tactic:
rw [withDensityᵥ, dif_neg hfi, add_zero] at hadd

Premises used: MeasureTheory.Measure.withDensityᵥ, dif_neg, add_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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 μ

Tactic:
haveLebesgueDecomposition_mk' μ measurable_zero (integrable_zero _ _ μ) htμ ?_

Premises used: _private.0.MeasureTheory.SignedMeasure.haveLebesgueDecomposition_mk', MeasureTheory.integrable_zero, measurable_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
neg : s = t + μ.withDensityᵥ 0
⊢ s.HaveLebesgueDecomposition μ

Tactic:
refine haveLebesgueDecomposition_mk' μ measurable_zero (integrable_zero _ _ μ) htμ ?_

Premises used: _private.0.MeasureTheory.SignedMeasure.haveLebesgueDecomposition_mk', MeasureTheory.integrable_zero, measurable_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
f : α → ℝ
hf : Measurable f
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t
hfi : ¬Integrable f μ
neg : s = t + 0
neg₁ neg₂ neg₃ neg₄ : s = t
⊢ s = t + μ.withDensityᵥ 0

Tactic:
rwa [withDensityᵥ_zero, add_zero]

Premises used: MeasureTheory.withDensityᵥ_zero, add_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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
⊢ t ⟂ᵥ μ.toENNRealVectorMeasure

Tactic:
have htμ' := htμ
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ

Tactic:
rw [mutuallySingular_ennreal_iff, totalVariation_mutuallySingular_iff,
    VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure] at htμ

Premises used: MeasureTheory.VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure, MeasureTheory.SignedMeasure.totalVariation_mutuallySingular_iff, MeasureTheory.SignedMeasure.mutuallySingular_ennreal_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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
htμ₁ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ s = t + μ.withDensityᵥ f

Tactic:
rw [mutuallySingular_ennreal_iff, totalVariation_mutuallySingular_iff,
    VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure] at htμ

Premises used: MeasureTheory.VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure, MeasureTheory.SignedMeasure.totalVariation_mutuallySingular_iff, MeasureTheory.SignedMeasure.mutuallySingular_ennreal_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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
htμ₁ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
hadd₁ : s = t + μ.withDensityᵥ f
⊢ t ⟂ᵥ μ.toENNRealVectorMeasure

Tactic:
rw [mutuallySingular_ennreal_iff, totalVariation_mutuallySingular_iff,
    VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure] at htμ

Premises used: MeasureTheory.VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure, MeasureTheory.SignedMeasure.totalVariation_mutuallySingular_iff, MeasureTheory.SignedMeasure.mutuallySingular_ennreal_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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
rw :
  t.toJordanDecomposition.posPart.toSignedMeasure - t.toJordanDecomposition.negPart.toSignedMeasure =
    (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
⊢ t = s.singularPart μ

Tactic:
rw [singularPart, ← t.toSignedMeasure_toJordanDecomposition,
    JordanDecomposition.toSignedMeasure]

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure, MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition, MeasureTheory.SignedMeasure.singularPart
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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 μ
e_a₁ : t.toJordanDecomposition.negPart = s.toJordanDecomposition.negPart.singularPart μ
⊢ t.toJordanDecomposition.posPart.toSignedMeasure - t.toJordanDecomposition.negPart.toSignedMeasure =
    (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
congr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ ENNReal.ofReal (f x)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ ENNReal.ofReal (f x)

Tactic:
have hfpos : Measurable fun x => ENNReal.ofReal (f x) := by fun_prop
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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 μ

Tactic:
eq_singularPart hfpos htμ.1 ?_

Premises used: And.left, MeasureTheory.Measure.eq_singularPart
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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)
e_a :
  s.toJordanDecomposition.posPart = t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)
⊢ t.toJordanDecomposition.posPart = s.toJordanDecomposition.posPart.singularPart μ

Tactic:
refine eq_singularPart hfpos htμ.1 ?_

Premises used: And.left, MeasureTheory.Measure.eq_singularPart
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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)
e_a 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 := ⋯, negPart_finite := ⋯, mutuallySingular := ⋯ : JordanDecomposition α }.posPart =
    t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)
⊢ s.toJordanDecomposition.posPart = t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)

Tactic:
rw [toJordanDecomposition_eq_of_eq_add_withDensity hf hfi htμ' hadd]

Premises used: MeasureTheory.SignedMeasure.toJordanDecomposition_eq_of_eq_add_withDensity
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ ENNReal.ofReal (-f x)

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ ENNReal.ofReal (-f x)

Tactic:
have hfneg : Measurable fun x => ENNReal.ofReal (-f x) := by fun_prop
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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 μ

Tactic:
eq_singularPart hfneg htμ.2 ?_

Premises used: And.right, MeasureTheory.Measure.eq_singularPart
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
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)
e_a :
  s.toJordanDecomposition.negPart = t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)
⊢ t.toJordanDecomposition.negPart = s.toJordanDecomposition.negPart.singularPart μ

Tactic:
refine eq_singularPart hfneg htμ.2 ?_

Premises used: And.right, MeasureTheory.Measure.eq_singularPart