awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set X
hs : IsHahnDecomposition μ ν s
hsc : IsHahnDecomposition ν μ sᶜ
h₁ :
  ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s
h₂ :
  ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ
h₁' : ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0
h₂' : ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0
partition₁ :
  VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ = (μ - ν).toSignedMeasure
partition₂ :
  VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s + 0 = (ν - μ).toSignedMeasure
⊢ VectorMeasure.restrict μ.toSignedMeasure s + VectorMeasure.restrict μ.toSignedMeasure sᶜ +
      -(VectorMeasure.restrict ν.toSignedMeasure s + VectorMeasure.restrict ν.toSignedMeasure sᶜ) =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ + -VectorMeasure.restrict ν.toSignedMeasure sᶜ +
      -(VectorMeasure.restrict ν.toSignedMeasure s + -VectorMeasure.restrict μ.toSignedMeasure s + 0)

Tactic:
abel
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ (μ.jordanDecompositionOfToSignedMeasureSub ν).posPart = μ - ν

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ (μ.jordanDecompositionOfToSignedMeasureSub ν).negPart = ν - μ

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
simp_rw :
  (μ.jordanDecompositionOfToSignedMeasureSub ν).posPart.toSignedMeasure -
      (μ.jordanDecompositionOfToSignedMeasureSub ν).negPart.toSignedMeasure =
    μ.toSignedMeasure - ν.toSignedMeasure
simp_rw₁ :
  (μ - ν).toSignedMeasure - (μ.jordanDecompositionOfToSignedMeasureSub ν).negPart.toSignedMeasure =
    μ.toSignedMeasure - ν.toSignedMeasure
simp_rw₂ : (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure = μ.toSignedMeasure - ν.toSignedMeasure
⊢ (μ.jordanDecompositionOfToSignedMeasureSub ν).toSignedMeasure = μ.toSignedMeasure - ν.toSignedMeasure

Tactic:
simp_rw [JordanDecomposition.toSignedMeasure, jordanDecompositionOfToSignedMeasureSub_posPart,
    jordanDecompositionOfToSignedMeasureSub_negPart, ← sub_toSignedMeasure_eq_toSignedMeasure_sub]

Premises used: MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub_posPart, MeasureTheory.JordanDecomposition.toSignedMeasure, MeasureTheory.Measure.sub_toSignedMeasure_eq_toSignedMeasure_sub, MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub_negPart
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
a :
  (μ.toSignedMeasure - ν.toSignedMeasure).toJordanDecomposition.toSignedMeasure =
    (μ.jordanDecompositionOfToSignedMeasureSub ν).toSignedMeasure
⊢ (μ.toSignedMeasure - ν.toSignedMeasure).toJordanDecomposition = μ.jordanDecompositionOfToSignedMeasureSub ν

Tactic:
apply JordanDecomposition.toSignedMeasure_injective

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure_injective
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
a : μ.toSignedMeasure - ν.toSignedMeasure = (μ.jordanDecompositionOfToSignedMeasureSub ν).toSignedMeasure
a₁ a₂ : μ.toSignedMeasure - ν.toSignedMeasure = μ.toSignedMeasure - ν.toSignedMeasure
⊢ (μ.toSignedMeasure - ν.toSignedMeasure).toJordanDecomposition.toSignedMeasure =
    (μ.jordanDecompositionOfToSignedMeasureSub ν).toSignedMeasure

Tactic:
rw [SignedMeasure.toSignedMeasure_toJordanDecomposition,
    jordanDecompositionOfToSignedMeasureSub_toSignedMeasure]

Premises used: MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub_toSignedMeasure, MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ ¬s.HaveLebesgueDecomposition μ ↔
    ¬s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ ∨
      ¬s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ

Tactic:
⟨fun h => not_or_of_imp fun hp hn => h ⟨hp, hn⟩, fun h hl => (not_and_or.2 h) ⟨hl.1, hl.2⟩⟩

Premises used: Iff.mpr, MeasureTheory.SignedMeasure.HaveLebesgueDecomposition.negPart, MeasureTheory.SignedMeasure.HaveLebesgueDecomposition.mk, MeasureTheory.SignedMeasure.HaveLebesgueDecomposition.posPart, And.intro, not_and_or, Iff.intro, not_or_of_imp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
rw : s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ
⊢ (-s).toJordanDecomposition.posPart.HaveLebesgueDecomposition μ

Tactic:
rw [toJordanDecomposition_neg, JordanDecomposition.neg_posPart]

Premises used: MeasureTheory.SignedMeasure.toJordanDecomposition_neg, MeasureTheory.JordanDecomposition.neg_posPart
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
rw : s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ
⊢ (-s).toJordanDecomposition.negPart.HaveLebesgueDecomposition μ

Tactic:
rw [toJordanDecomposition_neg, JordanDecomposition.neg_negPart]

Premises used: MeasureTheory.JordanDecomposition.neg_negPart, MeasureTheory.SignedMeasure.toJordanDecomposition_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
⊢ s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ≥0
rw : (r • s.toJordanDecomposition.posPart).HaveLebesgueDecomposition μ
⊢ (r • s).toJordanDecomposition.posPart.HaveLebesgueDecomposition μ

Tactic:
rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart]

Premises used: MeasureTheory.JordanDecomposition.smul_posPart, MeasureTheory.SignedMeasure.toJordanDecomposition_smul
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ (r • s.toJordanDecomposition.posPart).HaveLebesgueDecomposition μ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ≥0
rw : (r • s.toJordanDecomposition.negPart).HaveLebesgueDecomposition μ
⊢ (r • s).toJordanDecomposition.negPart.HaveLebesgueDecomposition μ

Tactic:
rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart]

Premises used: MeasureTheory.JordanDecomposition.smul_negPart, MeasureTheory.SignedMeasure.toJordanDecomposition_smul
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ (r • s.toJordanDecomposition.negPart).HaveLebesgueDecomposition μ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
pos : ∀ (hr : 0 ≤ r), (r • s).HaveLebesgueDecomposition μ
neg : ∀ (hr : r < 0), (r • s).HaveLebesgueDecomposition μ
⊢ (r • s).HaveLebesgueDecomposition μ

Tactic:
by_cases! hr : 0 ≤ r
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ r

Tactic:
hr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
hr : 0 ≤ r
pos : ∀ (r : ℝ≥0), ((↑r : ℝ) • s).HaveLebesgueDecomposition μ
⊢ (r • s).HaveLebesgueDecomposition μ

Tactic:
lift r to ℝ≥0 using hr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ ((↑r : ℝ) • s).HaveLebesgueDecomposition μ

Tactic:
s.haveLebesgueDecomposition_smul μ _

Premises used: MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ ((↑r : ℝ) • s).HaveLebesgueDecomposition μ

Tactic:
exact s.haveLebesgueDecomposition_smul μ _

Premises used: MeasureTheory.SignedMeasure.haveLebesgueDecomposition_smul
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
hr : r < 0
rw : ((-r).toNNReal • s.toJordanDecomposition.negPart).HaveLebesgueDecomposition μ
⊢ (r • s).toJordanDecomposition.posPart.HaveLebesgueDecomposition μ

Tactic:
rw [toJordanDecomposition_smul_real, JordanDecomposition.real_smul_posPart_neg _ _ hr]

Premises used: MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real, MeasureTheory.JordanDecomposition.real_smul_posPart_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
hr : r < 0
⊢ ((-r).toNNReal • s.toJordanDecomposition.negPart).HaveLebesgueDecomposition μ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
hr : r < 0
rw : ((-r).toNNReal • s.toJordanDecomposition.posPart).HaveLebesgueDecomposition μ
⊢ (r • s).toJordanDecomposition.negPart.HaveLebesgueDecomposition μ

Tactic:
rw [toJordanDecomposition_smul_real, JordanDecomposition.real_smul_negPart_neg _ _ hr]

Premises used: MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real, MeasureTheory.JordanDecomposition.real_smul_negPart_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
hr : r < 0
⊢ ((-r).toNNReal • s.toJordanDecomposition.posPart).HaveLebesgueDecomposition μ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
hr : r < 0
⊢ (r • s).HaveLebesgueDecomposition μ

Tactic:
refine
      { posPart := by
          rw [toJordanDecomposition_smul_real, JordanDecomposition.real_smul_posPart_neg _ _ hr]
          infer_instance
        negPart := by
          rw [toJordanDecomposition_smul_real, JordanDecomposition.real_smul_negPart_neg _ _ hr]
          infer_instance }
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ s.toJordanDecomposition.posPart.singularPart μ ⟂ₘ s.toJordanDecomposition.negPart.singularPart μ

Tactic:
(s.toJordanDecomposition.mutuallySingular.singularPart μ).mono le_rfl (singularPart_le _ _)

Premises used: le_rfl, MeasureTheory.Measure.MutuallySingular.mono, MeasureTheory.SignedMeasure.toJordanDecomposition, MeasureTheory.Measure.singularPart_le, MeasureTheory.Measure.MutuallySingular.singularPart, MeasureTheory.JordanDecomposition.mutuallySingular
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ (s.singularPart μ).toJordanDecomposition =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
      negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
      mutuallySingular := ⋯ }

Tactic:
JordanDecomposition.toSignedMeasure_injective ?_

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure_injective
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
refine :
  (s.singularPart μ).toJordanDecomposition.toSignedMeasure =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
        negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
        mutuallySingular := ⋯ }.toSignedMeasure
⊢ (s.singularPart μ).toJordanDecomposition =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
      negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
      mutuallySingular := ⋯ }

Tactic:
refine JordanDecomposition.toSignedMeasure_injective ?_

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure_injective
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
rw :
  s.singularPart μ =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
        negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
        mutuallySingular := ⋯ }.toSignedMeasure
rw₁ :
  (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
        negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
        mutuallySingular := ⋯ }.toSignedMeasure
rw₂ rw₃ :
  (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
            negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
            mutuallySingular := ⋯ : JordanDecomposition α }.posPart.toSignedMeasure -
      { posPart := s.toJordanDecomposition.posPart.singularPart μ,
            negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
            mutuallySingular := ⋯ : JordanDecomposition α }.negPart.toSignedMeasure
⊢ (s.singularPart μ).toJordanDecomposition.toSignedMeasure =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
        negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
        mutuallySingular := ⋯ }.toSignedMeasure

Tactic:
rw [toSignedMeasure_toJordanDecomposition, singularPart, 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 α
s : SignedMeasure α
μ : Measure α
⊢ (s.singularPart μ).toJordanDecomposition =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
      negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
      mutuallySingular := ⋯ }

Tactic:
have :
    (s.singularPart μ).toJordanDecomposition =
      ⟨s.toJordanDecomposition.posPart.singularPart μ,
        s.toJordanDecomposition.negPart.singularPart μ, singularPart_mutuallySingular s μ⟩ := by
    refine JordanDecomposition.toSignedMeasure_injective ?_
    rw [toSignedMeasure_toJordanDecomposition, singularPart, JordanDecomposition.toSignedMeasure]
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
this :
  (s.singularPart μ).toJordanDecomposition =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
      negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
      mutuallySingular := ⋯ }
rw :
  (s.singularPart μ).toJordanDecomposition.posPart + (s.singularPart μ).toJordanDecomposition.negPart =
    s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ
rw₁ rw₂ :
  { posPart := s.toJordanDecomposition.posPart.singularPart μ,
          negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
          mutuallySingular := ⋯ : JordanDecomposition α }.posPart +
      { posPart := s.toJordanDecomposition.posPart.singularPart μ,
          negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
          mutuallySingular := ⋯ : JordanDecomposition α }.negPart =
    s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ
⊢ (s.singularPart μ).totalVariation =
    s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ

Tactic:
rw [totalVariation, this]

Premises used: MeasureTheory.SignedMeasure.totalVariation
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
rw : s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ ⟂ₘ μ
⊢ s.singularPart μ ⟂ᵥ μ.toENNRealVectorMeasure

Tactic:
rw [mutuallySingular_ennreal_iff, singularPart_totalVariation,
    VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure]

Premises used: MeasureTheory.VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure, MeasureTheory.SignedMeasure.mutuallySingular_ennreal_iff, MeasureTheory.SignedMeasure.singularPart_totalVariation
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ ⟂ₘ μ

Tactic:
(mutuallySingular_singularPart _ _).add_left (mutuallySingular_singularPart _ _)

Premises used: MeasureTheory.Measure.MutuallySingular.add_left, MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ ⟂ₘ μ

Tactic:
exact (mutuallySingular_singularPart _ _).add_left (mutuallySingular_singularPart _ _)

Premises used: MeasureTheory.SignedMeasure.mutuallySingular_singularPart, MeasureTheory.VectorMeasure.MutuallySingular.add_left
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ s.rnDeriv μ = fun (x : α) ↦
    (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal - (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal

Tactic:
rfl

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

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Integrable (s.rnDeriv μ) μ

Tactic:
Integrable.sub ?_ ?_

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.SignedMeasure.rnDeriv
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
refine_1 : Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ
refine_2 : Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ
⊢ Integrable (s.rnDeriv μ) μ

Tactic:
refine Integrable.sub ?_ ?_

Premises used: MeasureTheory.Integrable.sub
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
refine_1 : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ
refine_1₁ : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
refine_1 : Measurable (β := ℝ) fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.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.posPart.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.posPart.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.posPart.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 α
s : SignedMeasure α
μ : Measure α
refine_2 : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ
refine_2₁ : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ

Tactic:
constructor