awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
refine_2 : Measurable (β := ℝ) fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ

Tactic:
apply Measurable.aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Measurable (β := ℝ) fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ

Tactic:
hasFiniteIntegral_toReal_of_lintegral_ne_top (lintegral_rnDeriv_lt_top _ μ).ne

Premises used: MeasureTheory.hasFiniteIntegral_toReal_of_lintegral_ne_top, MeasureTheory.Measure.lintegral_rnDeriv_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ

Tactic:
exact hasFiniteIntegral_toReal_of_lintegral_ne_top (lintegral_rnDeriv_lt_top _ μ).ne

Premises used: MeasureTheory.hasFiniteIntegral_toReal_of_lintegral_ne_top, MeasureTheory.Measure.lintegral_rnDeriv_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
rw : s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
| s

Tactic:
rw [← toSignedMeasure_toJordanDecomposition s, JordanDecomposition.toSignedMeasure]

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure, MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
conv_rhs :
  s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
⊢ s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s

Tactic:
conv_rhs =>
    rw [← toSignedMeasure_toJordanDecomposition s, JordanDecomposition.toSignedMeasure]

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure, MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
rw :
  (s.toJordanDecomposition.posPart.singularPart μ +
          μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)).toSignedMeasure -
      (μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) +
          s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
hfm : AEMeasurable (s.toJordanDecomposition.negPart.rnDeriv μ) μ
hf : ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ∞
hfm₁ : AEMeasurable (s.toJordanDecomposition.posPart.rnDeriv μ) μ
hf₁ : ∫⁻ (x : α), s.toJordanDecomposition.posPart.rnDeriv μ x ∂μ ≠ ∞
rw₁ : AEMeasurable (s.toJordanDecomposition.posPart.rnDeriv μ) μ
rw₂ : ∫⁻ (x : α), s.toJordanDecomposition.posPart.rnDeriv μ x ∂μ ≠ ∞
rw₃ : AEMeasurable (s.toJordanDecomposition.negPart.rnDeriv μ) μ
rw₄ : ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ∞
⊢ s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure

Tactic:
rw [singularPart, rnDeriv_def,
    withDensityᵥ_sub' (integrable_toReal_of_lintegral_ne_top _ _)
      (integrable_toReal_of_lintegral_ne_top _ _),
    withDensityᵥ_toReal, withDensityᵥ_toReal, sub_eq_add_neg, sub_eq_add_neg,
    add_comm (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure, ← add_assoc,
    add_assoc (-(s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure),
    ← toSignedMeasure_add, add_comm, ← add_assoc, ← neg_add, ← toSignedMeasure_add, add_comm,
    ← sub_eq_add_neg]

Premises used: MeasureTheory.JordanDecomposition.posPart, MeasureTheory.SignedMeasure.rnDeriv_def, add_assoc, sub_eq_add_neg, MeasureTheory.SignedMeasure.toJordanDecomposition, neg_add, MeasureTheory.JordanDecomposition.negPart, MeasureTheory.integrable_toReal_of_lintegral_ne_top, add_comm, MeasureTheory.Measure.toSignedMeasure_add, MeasureTheory.Measure.singularPart, MeasureTheory.withDensityᵥ_toReal, MeasureTheory.withDensityᵥ_sub', MeasureTheory.SignedMeasure.singularPart, MeasureTheory.Measure.toSignedMeasure, Neg.neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ (s.toJordanDecomposition.posPart.singularPart μ +
          μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)).toSignedMeasure -
      (μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) +
          s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    (s.toJordanDecomposition.posPart.singularPart μ +
          μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)).toSignedMeasure -
      (μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) +
          s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
h :
  s.toJordanDecomposition.posPart =
    s.toJordanDecomposition.posPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)
h₁ :
  s.toJordanDecomposition.negPart =
    μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) + s.toJordanDecomposition.negPart.singularPart μ
⊢ (s.toJordanDecomposition.posPart.singularPart μ +
          μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)).toSignedMeasure -
      (μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) +
          s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure

Tactic:
convert! rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.posPart =
    s.toJordanDecomposition.posPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)

Tactic:
s.toJordanDecomposition.posPart.haveLebesgueDecomposition_add μ

Premises used: MeasureTheory.JordanDecomposition.posPart, MeasureTheory.Measure.haveLebesgueDecomposition_add, MeasureTheory.SignedMeasure.toJordanDecomposition
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.posPart =
    s.toJordanDecomposition.posPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)

Tactic:
exact s.toJordanDecomposition.posPart.haveLebesgueDecomposition_add μ

Premises used: MeasureTheory.JordanDecomposition.posPart, MeasureTheory.Measure.haveLebesgueDecomposition_add, MeasureTheory.SignedMeasure.toJordanDecomposition
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
h :
  s.toJordanDecomposition.negPart =
    s.toJordanDecomposition.negPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ)
⊢ s.toJordanDecomposition.negPart =
    μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) + s.toJordanDecomposition.negPart.singularPart μ

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.negPart =
    s.toJordanDecomposition.negPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ)

Tactic:
s.toJordanDecomposition.negPart.haveLebesgueDecomposition_add μ

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, MeasureTheory.SignedMeasure.toJordanDecomposition, MeasureTheory.JordanDecomposition.negPart
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.negPart =
    s.toJordanDecomposition.negPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ)

Tactic:
exact s.toJordanDecomposition.negPart.haveLebesgueDecomposition_add μ

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, MeasureTheory.SignedMeasure.toJordanDecomposition, MeasureTheory.JordanDecomposition.negPart
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ AEMeasurable (s.toJordanDecomposition.negPart.rnDeriv μ) μ

Tactic:
(lintegral_rnDeriv_lt_top _ _).ne

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ AEMeasurable (s.toJordanDecomposition.negPart.rnDeriv μ) μ

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ AEMeasurable (s.toJordanDecomposition.negPart.rnDeriv μ) μ

Tactic:
first
    | exact (lintegral_rnDeriv_lt_top _ _).ne
    | measurability

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ∞

Tactic:
(lintegral_rnDeriv_lt_top _ _).ne

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ∞

Tactic:
exact (lintegral_rnDeriv_lt_top _ _).ne

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ∞

Tactic:
first
    | exact (lintegral_rnDeriv_lt_top _ _).ne
    | measurability

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ AEMeasurable (s.toJordanDecomposition.posPart.rnDeriv μ) μ

Tactic:
(lintegral_rnDeriv_lt_top _ _).ne

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ AEMeasurable (s.toJordanDecomposition.posPart.rnDeriv μ) μ

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ AEMeasurable (s.toJordanDecomposition.posPart.rnDeriv μ) μ

Tactic:
first
    | exact (lintegral_rnDeriv_lt_top _ _).ne
    | measurability

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), s.toJordanDecomposition.posPart.rnDeriv μ x ∂μ ≠ ∞

Tactic:
(lintegral_rnDeriv_lt_top _ _).ne

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), s.toJordanDecomposition.posPart.rnDeriv μ x ∂μ ≠ ∞

Tactic:
exact (lintegral_rnDeriv_lt_top _ _).ne

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ ∫⁻ (x : α), s.toJordanDecomposition.posPart.rnDeriv μ x ∂μ ≠ ∞

Tactic:
first
    | exact (lintegral_rnDeriv_lt_top _ _).ne
    | measurability

Premises used: MeasureTheory.Measure.lintegral_rnDeriv_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : SignedMeasure α
f : α → ℝ
hf : Measurable 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 α
t : SignedMeasure α
f : α → ℝ
hf : Measurable f
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)) ⟂ₘ
    t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)

Tactic:
((JordanDecomposition.mutuallySingular _).add_right
          (htμ.1.mono_ac (refl _) (withDensity_absolutelyContinuous _ _))).add_left
      ((htμ.2.symm.mono_ac (withDensity_absolutelyContinuous _ _) (refl _)).add_right
        (withDensity_ofReal_mutuallySingular hf))

Premises used: MeasureTheory.Measure.MutuallySingular.add_left, MeasureTheory.withDensity_ofReal_mutuallySingular, MeasureTheory.Measure.MutuallySingular.add_right, And.right, And.left, MeasureTheory.withDensity_absolutelyContinuous, refl, MeasureTheory.Measure.MutuallySingular.mono_ac, MeasureTheory.Measure.MutuallySingular.symm, MeasureTheory.JordanDecomposition.mutuallySingular
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : SignedMeasure α
f : α → ℝ
hf : Measurable f
htμ : t.toJordanDecomposition.posPart ⟂ₘ μ ∧ t.toJordanDecomposition.negPart ⟂ₘ μ
⊢ (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x)) ⟂ₘ
    t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x)

Tactic:
exact
    ((JordanDecomposition.mutuallySingular _).add_right
          (htμ.1.mono_ac (refl _) (withDensity_absolutelyContinuous _ _))).add_left
      ((htμ.2.symm.mono_ac (withDensity_absolutelyContinuous _ _) (refl _)).add_right
        (withDensity_ofReal_mutuallySingular hf))

Premises used: MeasureTheory.Measure.MutuallySingular.add_left, MeasureTheory.withDensity_ofReal_mutuallySingular, MeasureTheory.Measure.MutuallySingular.add_right, And.right, And.left, MeasureTheory.withDensity_absolutelyContinuous, refl, MeasureTheory.Measure.MutuallySingular.mono_ac, MeasureTheory.Measure.MutuallySingular.symm, MeasureTheory.JordanDecomposition.mutuallySingular
-- 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
⊢ IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))

Tactic:
haveI := isFiniteMeasure_withDensity_ofReal hfi.2
-- 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
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
⊢ IsFiniteMeasure (t.toJordanDecomposition.posPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))

Tactic:
infer_instance
-- 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
⊢ IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))

Tactic:
haveI := isFiniteMeasure_withDensity_ofReal hfi.neg.2
-- 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
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
⊢ IsFiniteMeasure (t.toJordanDecomposition.negPart + μ.withDensity fun (x : α) ↦ ENNReal.ofReal (-f x))

Tactic:
infer_instance
-- 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
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
⊢ IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))

Tactic:
haveI := isFiniteMeasure_withDensity_ofReal hfi.neg.2
-- 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
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 := ⋯ }

Tactic:
toJordanDecomposition_eq ?_

Premises used: MeasureTheory.SignedMeasure.toJordanDecomposition_eq
-- 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
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
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 := ⋯, negPart_finite := ⋯, mutuallySingular := ⋯ }.toSignedMeasure
⊢ 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 := ⋯ }

Tactic:
refine toJordanDecomposition_eq ?_

Premises used: MeasureTheory.SignedMeasure.toJordanDecomposition_eq
-- 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
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
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
⊢ 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

Tactic:
simp_rw [JordanDecomposition.toSignedMeasure, hadd]

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure
-- 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
this_1 : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal (f x))
this : IsFiniteMeasure (μ.withDensity fun (x : α) ↦ ENNReal.ofReal ((-f) x))
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
⊢ 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:
ext i hi
-- 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
⊢ t ⟂ᵥ μ.toENNRealVectorMeasure

Tactic:
have htμ' := htμ
-- 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
⊢ t.totalVariation ⟂ₘ μ.toENNRealVectorMeasure.ennrealToMeasure

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 ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
htμ' : t ⟂ᵥ μ.toENNRealVectorMeasure
htμ₁ : t.totalVariation ⟂ₘ μ.toENNRealVectorMeasure.ennrealToMeasure
⊢ s = t + μ.withDensityᵥ f

Tactic:
rw [mutuallySingular_ennreal_iff] at htμ

Premises used: MeasureTheory.SignedMeasure.mutuallySingular_ennreal_iff