awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
hu₂ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) uᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
mpr : ∀ (t : Set α) (htv : t ⊆ uᶜ) (hmt : MeasurableSet t), (↑μ : Set α → ℝ≥0∞) t = 0
⊢ s ⟂ᵥ μ

Tactic:
refine
      VectorMeasure.MutuallySingular.mk u hmeas
        (fun t htu _ => null_of_totalVariation_zero _ (measure_mono_null htu hu₁)) fun t htv hmt =>
        ?_

Premises used: MeasureTheory.VectorMeasure.MutuallySingular.mk, MeasureTheory.measure_mono_null, MeasureTheory.SignedMeasure.null_of_totalVariation_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
hu₂ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) uᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
htv : t ⊆ uᶜ
hmt : MeasurableSet t
mpr : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (↑μ : Set α → ℝ≥0∞) t = 0

Tactic:
rw [← VectorMeasure.ennrealToMeasure_apply hmt]

Premises used: MeasureTheory.VectorMeasure.ennrealToMeasure_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
hu₂ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) uᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
htv : t ⊆ uᶜ
hmt : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_mono_null htv hu₂

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
hu₂ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) uᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
htv : t ⊆ uᶜ
hmt : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact measure_mono_null htv hu₂

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ s.totalVariation ⟂ₘ μ ↔ s.toJordanDecomposition.posPart ⟂ₘ μ ∧ s.toJordanDecomposition.negPart ⟂ₘ μ

Tactic:
Measure.MutuallySingular.add_left_iff

Premises used: MeasureTheory.SignedMeasure.totalVariation, MeasureTheory.Measure.MutuallySingular.add_left_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
Goal:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ ν : Measure X
hs : IsHahnDecomposition μ ν s
rw : μ.restrict s - ν.restrict s = 0
⊢ Eq (α := ℝ≥0∞) ((μ - ν : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← restrict_eq_zero, restrict_sub_eq_restrict_sub_restrict hs.measurableSet]

Premises used: MeasureTheory.Measure.restrict_eq_zero, MeasureTheory.Measure.restrict_sub_eq_restrict_sub_restrict, MeasureTheory.IsHahnDecomposition.measurableSet
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
Goal:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ ν : Measure X
hs : IsHahnDecomposition μ ν s
⊢ μ.restrict s - ν.restrict s = 0

Tactic:
sub_eq_zero_of_le hs.le_on

Premises used: MeasureTheory.Measure.sub_eq_zero_of_le, MeasureTheory.IsHahnDecomposition.le_on
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
Goal:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ ν : Measure X
hs : IsHahnDecomposition μ ν s
⊢ μ.restrict s - ν.restrict s = 0

Tactic:
exact sub_eq_zero_of_le hs.le_on

Premises used: MeasureTheory.Measure.sub_eq_zero_of_le, MeasureTheory.IsHahnDecomposition.le_on
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
obtain : ∀ (s : Set X) (hs : IsHahnDecomposition μ ν s), μ - ν ⟂ₘ ν - μ
⊢ μ - ν ⟂ₘ ν - μ

Tactic:
obtain ⟨s, hs⟩ := exists_isHahnDecomposition μ ν

Premises used: MeasureTheory.exists_isHahnDecomposition
-- 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
⊢ μ - ν ⟂ₘ ν - μ

Tactic:
⟨s, hs.measurableSet,
    sub_apply_eq_zero_of_isHahnDecomposition hs,
    sub_apply_eq_zero_of_isHahnDecomposition hs.compl⟩

Premises used: MeasureTheory.IsHahnDecomposition.compl, MeasureTheory.Measure.MutuallySingular, And.intro, Exists.intro, MeasureTheory.Measure.sub_apply_eq_zero_of_isHahnDecomposition, MeasureTheory.IsHahnDecomposition.measurableSet
-- 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
⊢ μ - ν ⟂ₘ ν - μ

Tactic:
exact ⟨s, hs.measurableSet,
    sub_apply_eq_zero_of_isHahnDecomposition hs,
    sub_apply_eq_zero_of_isHahnDecomposition hs.compl⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
Goal:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hs : IsHahnDecomposition μ ν s
⊢ MeasurableSet s

Tactic:
have hmeas := hs.measurableSet
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
Goal:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hs : IsHahnDecomposition μ ν s
hmeas : MeasurableSet s
rw : ((ν - μ).restrict s + μ.restrict s).toSignedMeasure = VectorMeasure.restrict ν.toSignedMeasure s
⊢ ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s

Tactic:
rw [eq_sub_iff_add_eq, toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hmeas,
    ← toSignedMeasure_add]

Premises used: eq_sub_iff_add_eq, MeasureTheory.Measure.toSignedMeasure_add, MeasureTheory.Measure.toSignedMeasure_restrict_eq_restrict_toSignedMeasure
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
Goal:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hs : IsHahnDecomposition μ ν s
hmeas : MeasurableSet s
simp : (ν.restrict s).toSignedMeasure = VectorMeasure.restrict ν.toSignedMeasure s
⊢ ((ν - μ).restrict s + μ.restrict s).toSignedMeasure = VectorMeasure.restrict ν.toSignedMeasure s

Tactic:
simp only [restrict_sub_eq_restrict_sub_restrict, hmeas, sub_add_cancel_of_le hs.le_on]

Premises used: MeasureTheory.Measure.sub_add_cancel_of_le, MeasureTheory.Measure.restrict_sub_eq_restrict_sub_restrict, MeasureTheory.IsHahnDecomposition.le_on
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
Goal:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hs : IsHahnDecomposition μ ν s
hmeas : MeasurableSet s
⊢ (ν.restrict s).toSignedMeasure = VectorMeasure.restrict ν.toSignedMeasure s

Tactic:
(toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hmeas).symm

Premises used: MeasureTheory.Measure.toSignedMeasure_restrict_eq_restrict_toSignedMeasure, Eq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
Goal:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hs : IsHahnDecomposition μ ν s
hmeas : MeasurableSet s
⊢ (ν.restrict s).toSignedMeasure = VectorMeasure.restrict ν.toSignedMeasure s

Tactic:
exact (toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hmeas).symm

Premises used: MeasureTheory.Measure.toSignedMeasure_restrict_eq_restrict_toSignedMeasure, Eq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
Goal:
X : Type u_1
mX : MeasurableSpace X
μ ν : Measure X
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
obtain :
  ∀ (s : Set X) (hs : IsHahnDecomposition μ ν s),
    μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure

Tactic:
obtain ⟨s, hs⟩ := exists_isHahnDecomposition μ ν

Premises used: MeasureTheory.exists_isHahnDecomposition
-- 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
⊢ IsHahnDecomposition ν μ sᶜ

Tactic:
have hsc := hs.compl
-- 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ᶜ
⊢ ((ν - μ).restrict s).toSignedMeasure =
    VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s

Tactic:
have h₁ := toSignedMeasure_restrict_sub hs
-- 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
⊢ ((μ - ν).restrict sᶜ).toSignedMeasure =
    VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ

Tactic:
have h₂ := toSignedMeasure_restrict_sub hsc
-- 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ᶜ
⊢ ((μ - ν).restrict s).toSignedMeasure = toSignedMeasure 0

Tactic:
have h₁' := toSignedMeasure_congr <| restrict_eq_zero.mpr <|
    sub_apply_eq_zero_of_isHahnDecomposition hs
-- 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
⊢ ((ν - μ).restrict sᶜ).toSignedMeasure = toSignedMeasure 0

Tactic:
have h₂' := toSignedMeasure_congr <| restrict_eq_zero.mpr <|
  sub_apply_eq_zero_of_isHahnDecomposition hsc
-- 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
⊢ VectorMeasure.restrict (μ - ν).toSignedMeasure s + VectorMeasure.restrict (μ - ν).toSignedMeasure sᶜ =
    (μ - ν).toSignedMeasure

Tactic:
have partition₁ := VectorMeasure.restrict_add_restrict_compl (μ - ν).toSignedMeasure
    hs.measurableSet
-- 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
⊢ VectorMeasure.restrict (ν - μ).toSignedMeasure s + VectorMeasure.restrict (ν - μ).toSignedMeasure sᶜ =
    (ν - μ).toSignedMeasure

Tactic:
have partition₂ := VectorMeasure.restrict_add_restrict_compl (ν - μ).toSignedMeasure
    hs.measurableSet
-- 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ᶜ =
    (ν - μ).toSignedMeasure
⊢ ((μ - ν).restrict s).toSignedMeasure + ((μ - ν).restrict sᶜ).toSignedMeasure = (μ - ν).toSignedMeasure

Tactic:
rw [toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hs.measurableSet,
    toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hs.measurableSet.compl]
    at partition₁ partition₂

Premises used: MeasurableSet.compl, MeasureTheory.Measure.toSignedMeasure_restrict_eq_restrict_toSignedMeasure, MeasureTheory.IsHahnDecomposition.measurableSet
-- 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ᶜ =
    (ν - μ).toSignedMeasure
partition₃ : ((μ - ν).restrict s).toSignedMeasure + ((μ - ν).restrict sᶜ).toSignedMeasure = (μ - ν).toSignedMeasure
⊢ ((ν - μ).restrict s).toSignedMeasure + ((ν - μ).restrict sᶜ).toSignedMeasure = (ν - μ).toSignedMeasure

Tactic:
rw [toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hs.measurableSet,
    toSignedMeasure_restrict_eq_restrict_toSignedMeasure _ _ hs.measurableSet.compl]
    at partition₁ partition₂

Premises used: MeasurableSet.compl, MeasureTheory.Measure.toSignedMeasure_restrict_eq_restrict_toSignedMeasure, MeasureTheory.IsHahnDecomposition.measurableSet
-- 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₁ : ((μ - ν).restrict s).toSignedMeasure + ((μ - ν).restrict sᶜ).toSignedMeasure = (μ - ν).toSignedMeasure
partition₂ : ((ν - μ).restrict s).toSignedMeasure + ((ν - μ).restrict sᶜ).toSignedMeasure = (ν - μ).toSignedMeasure
⊢ toSignedMeasure 0 + (VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ) =
    (μ - ν).toSignedMeasure

Tactic:
rw [h₁', h₂] at partition₁
-- 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₁ : ((μ - ν).restrict s).toSignedMeasure + ((μ - ν).restrict sᶜ).toSignedMeasure = (μ - ν).toSignedMeasure
partition₂ : ((ν - μ).restrict s).toSignedMeasure + ((ν - μ).restrict sᶜ).toSignedMeasure = (ν - μ).toSignedMeasure
partition₃ :
  toSignedMeasure 0 + (VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ) =
    (μ - ν).toSignedMeasure
⊢ ((ν - μ).restrict s).toSignedMeasure + ((ν - μ).restrict sᶜ).toSignedMeasure = (ν - μ).toSignedMeasure

Tactic:
rw [h₁', h₂] at partition₁
-- 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₁ :
  toSignedMeasure 0 + (VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ) =
    (μ - ν).toSignedMeasure
partition₂ : ((ν - μ).restrict s).toSignedMeasure + ((ν - μ).restrict sᶜ).toSignedMeasure = (ν - μ).toSignedMeasure
⊢ VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s + toSignedMeasure 0 =
    (ν - μ).toSignedMeasure

Tactic:
rw [h₁, h₂'] at partition₂
-- 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₁ :
  toSignedMeasure 0 + (VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ) =
    (μ - ν).toSignedMeasure
partition₂ :
  VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s + toSignedMeasure 0 =
    (ν - μ).toSignedMeasure
⊢ VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ = (μ - ν).toSignedMeasure

Tactic:
simp only [toSignedMeasure_zero, zero_add] at partition₁ partition₂

Premises used: zero_add, MeasureTheory.Measure.toSignedMeasure_zero
-- 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₁ :
  toSignedMeasure 0 + (VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ) =
    (μ - ν).toSignedMeasure
partition₂ :
  VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s + toSignedMeasure 0 =
    (ν - μ).toSignedMeasure
partition₃ :
  VectorMeasure.restrict μ.toSignedMeasure sᶜ - VectorMeasure.restrict ν.toSignedMeasure sᶜ = (μ - ν).toSignedMeasure
⊢ VectorMeasure.restrict ν.toSignedMeasure s - VectorMeasure.restrict μ.toSignedMeasure s + 0 = (ν - μ).toSignedMeasure

Tactic:
simp only [toSignedMeasure_zero, zero_add] at partition₁ partition₂

Premises used: zero_add, MeasureTheory.Measure.toSignedMeasure_zero
-- 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
rw :
  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)
⊢ μ.toSignedMeasure - ν.toSignedMeasure = (μ - ν).toSignedMeasure - (ν - μ).toSignedMeasure

Tactic:
rw [← VectorMeasure.restrict_add_restrict_compl μ.toSignedMeasure hs.measurableSet,
    ← VectorMeasure.restrict_add_restrict_compl ν.toSignedMeasure hs.measurableSet,
    ← partition₁, ← partition₂]

Premises used: MeasureTheory.VectorMeasure.restrict_add_restrict_compl, MeasureTheory.Measure.toSignedMeasure, MeasureTheory.IsHahnDecomposition.measurableSet