awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s.totalVariation ≪ μ.ennrealToMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (↑s : Set α → ℝ) S = 0

Tactic:
null_of_totalVariation_zero s (h hS₂)

Premises used: MeasureTheory.SignedMeasure.null_of_totalVariation_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s.totalVariation ≪ μ.ennrealToMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (↑s : Set α → ℝ) S = 0

Tactic:
exact null_of_totalVariation_zero s (h hS₂)

Premises used: MeasureTheory.SignedMeasure.null_of_totalVariation_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
mp : s.totalVariation ≪ μ → s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
mpr : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ → s.totalVariation ≪ μ
⊢ s.totalVariation ≪ μ ↔ s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
mp : s.toJordanDecomposition.posPart ≪ μ
mp₁ : s.toJordanDecomposition.negPart ≪ μ
⊢ s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
⊢ s.toJordanDecomposition.posPart ≪ μ

Tactic:
Measure.AbsolutelyContinuous.mk fun S _ hS₂ => ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
mp :
  ∀ (S : Set α),
    MeasurableSet S →
      ∀ (hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)),
        Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s.toJordanDecomposition.posPart ≪ μ

Tactic:
refine Measure.AbsolutelyContinuous.mk fun S _ hS₂ => ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
h_1 : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have := h hS₂
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
h_1 : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
this : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [totalVariation, Measure.add_apply, add_eq_zero] at this

Premises used: MeasureTheory.SignedMeasure.totalVariation, MeasureTheory.Measure.add_apply, add_eq_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
⊢ s.toJordanDecomposition.negPart ≪ μ

Tactic:
Measure.AbsolutelyContinuous.mk fun S _ hS₂ => ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
mp :
  ∀ (S : Set α),
    MeasurableSet S →
      ∀ (hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)),
        Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s.toJordanDecomposition.negPart ≪ μ

Tactic:
refine Measure.AbsolutelyContinuous.mk fun S _ hS₂ => ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
h_1 : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
this :
  Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
this.1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
h_1 : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
this :
  Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
this.2

Premises used: And.right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.totalVariation ≪ μ
S : Set α
h_1 : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
this :
  Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exacts [this.1, this.2]

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
⊢ s.totalVariation ≪ μ

Tactic:
Measure.AbsolutelyContinuous.mk fun S _ hS₂ => ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
mpr :
  ∀ (S : Set α),
    MeasurableSet S →
      ∀ (hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)),
        Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s.totalVariation ≪ μ

Tactic:
refine Measure.AbsolutelyContinuous.mk fun S _ hS₂ => ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h : s.toJordanDecomposition.posPart ≪ μ ∧ s.toJordanDecomposition.negPart ≪ μ
S : Set α
h_1 : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
mpr :
  Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart + s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞)
    (0 : ℝ≥0∞)
mpr₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞)
      ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) =
    0
mpr₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) = 0
mpr₃ : HAdd.hAdd (α := ℝ≥0∞) 0 0 = 0
mpr₄ mpr₅ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [totalVariation, Measure.add_apply, h.1 hS₂, h.2 hS₂, add_zero]

Premises used: MeasureTheory.SignedMeasure.totalVariation, MeasureTheory.Measure.add_apply, And.right, And.left, add_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : SignedMeasure α
mp : s ⟂ᵥ t → s.totalVariation ⟂ₘ t.totalVariation
mpr : s.totalVariation ⟂ₘ t.totalVariation → s ⟂ᵥ t
⊢ s ⟂ᵥ t ↔ s.totalVariation ⟂ₘ t.totalVariation

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, (↑t : Set α → ℝ) t_1 = 0
mp :
  ∀ (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0)
    (hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂)
    (hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃), s.totalVariation ⟂ₘ t.totalVariation
⊢ s.totalVariation ⟂ₘ t.totalVariation

Tactic:
obtain ⟨i, hi₁, hi₂, hi₃, hipos, hineg⟩ := s.toJordanDecomposition_spec

Premises used: MeasureTheory.SignedMeasure.toJordanDecomposition_spec
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, (↑t : Set α → ℝ) t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
mp :
  ∀ (j : Set α) (hj₁ : MeasurableSet j) (hj₂ : 0 ≤[j] t) (hj₃ : t ≤[jᶜ] 0)
    (hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂)
    (hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃), s.totalVariation ⟂ₘ t.totalVariation
⊢ s.totalVariation ⟂ₘ t.totalVariation

Tactic:
obtain ⟨j, hj₁, hj₂, hj₃, hjpos, hjneg⟩ := t.toJordanDecomposition_spec

Premises used: MeasureTheory.SignedMeasure.toJordanDecomposition_spec
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, (↑t : Set α → ℝ) t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
⊢ s.totalVariation ⟂ₘ t.totalVariation

Tactic:
⟨u, hmeas, ?_, ?_⟩

Premises used: MeasureTheory.Measure.MutuallySingular, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, (↑t : Set α → ℝ) t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
mp : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
mp₁ : Eq (α := ℝ≥0∞) ((t.totalVariation : (a : Set α) → ℝ≥0∞) uᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s.totalVariation ⟂ₘ t.totalVariation

Tactic:
refine ⟨u, hmeas, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, (↑t : Set α → ℝ) t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
mp : (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ u)) ⋯) : ℝ≥0∞) + (↑(NNReal.mk (-(↑s : Set α → ℝ) (iᶜ ∩ u)) ⋯) : ℝ≥0∞) = 0
⊢ Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [totalVariation, Measure.add_apply, hipos, hineg, toMeasureOfZeroLE_apply _ _ _ hmeas,
        toMeasureOfLEZero_apply _ _ _ hmeas]

Premises used: MeasureTheory.SignedMeasure.toMeasureOfZeroLE_apply, MeasureTheory.SignedMeasure.totalVariation, MeasureTheory.Measure.add_apply, MeasureTheory.SignedMeasure.toMeasureOfLEZero_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, (↑t : Set α → ℝ) t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
⊢ (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ u)) ⋯) : ℝ≥0∞) + (↑(NNReal.mk (-(↑s : Set α → ℝ) (iᶜ ∩ u)) ⋯) : ℝ≥0∞) = 0

Tactic:
simp [hu₁ _ Set.inter_subset_right]

Premises used: Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, (↑t : Set α → ℝ) t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
mp : (↑(NNReal.mk ((↑t : Set α → ℝ) (j ∩ uᶜ)) ⋯) : ℝ≥0∞) + (↑(NNReal.mk (-(↑t : Set α → ℝ) (jᶜ ∩ uᶜ)) ⋯) : ℝ≥0∞) = 0
⊢ Eq (α := ℝ≥0∞) ((t.totalVariation : (a : Set α) → ℝ≥0∞) uᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [totalVariation, Measure.add_apply, hjpos, hjneg,
        toMeasureOfZeroLE_apply _ _ _ hmeas.compl,
        toMeasureOfLEZero_apply _ _ _ hmeas.compl]

Premises used: MeasureTheory.SignedMeasure.toMeasureOfZeroLE_apply, MeasureTheory.SignedMeasure.totalVariation, MeasureTheory.Measure.add_apply, MeasurableSet.compl, MeasureTheory.SignedMeasure.toMeasureOfLEZero_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t_1 ⊆ uᶜ, (↑t : Set α → ℝ) t_1 = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hipos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hineg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
j : Set α
hj₁ : MeasurableSet j
hj₂ : 0 ≤[j] t
hj₃ : t ≤[jᶜ] 0
hjpos : t.toJordanDecomposition.posPart = t.toMeasureOfZeroLE j hj₁ hj₂
hjneg : t.toJordanDecomposition.negPart = t.toMeasureOfLEZero jᶜ ⋯ hj₃
⊢ (↑(NNReal.mk ((↑t : Set α → ℝ) (j ∩ uᶜ)) ⋯) : ℝ≥0∞) + (↑(NNReal.mk (-(↑t : Set α → ℝ) (jᶜ ∩ uᶜ)) ⋯) : ℝ≥0∞) = 0

Tactic:
simp [hu₂ _ Set.inter_subset_right]

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

Tactic:
⟨u, hmeas, fun t htu => null_of_totalVariation_zero _ (measure_mono_null htu hu₁),
        fun t htv => null_of_totalVariation_zero _ (measure_mono_null htv hu₂)⟩

Premises used: MeasureTheory.measure_mono_null, And.intro, Exists.intro, MeasureTheory.SignedMeasure.null_of_totalVariation_zero, MeasureTheory.VectorMeasure.MutuallySingular
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s t : SignedMeasure α
u : Set α
hmeas : MeasurableSet u
hu₁ : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
hu₂ : Eq (α := ℝ≥0∞) ((t.totalVariation : (a : Set α) → ℝ≥0∞) uᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s ⟂ᵥ t

Tactic:
exact
      ⟨u, hmeas, fun t htu => null_of_totalVariation_zero _ (measure_mono_null htu hu₁),
        fun t htv => null_of_totalVariation_zero _ (measure_mono_null htv hu₂)⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
mp : s ⟂ᵥ μ → s.totalVariation ⟂ₘ μ.ennrealToMeasure
mpr : s.totalVariation ⟂ₘ μ.ennrealToMeasure → s ⟂ᵥ μ
⊢ s ⟂ᵥ μ ↔ s.totalVariation ⟂ₘ μ.ennrealToMeasure

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑μ : Set α → ℝ≥0∞) t = 0
mp :
  ∀ (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0)
    (hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂)
    (hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃), s.totalVariation ⟂ₘ μ.ennrealToMeasure
⊢ s.totalVariation ⟂ₘ μ.ennrealToMeasure

Tactic:
obtain ⟨i, hi₁, hi₂, hi₃, hpos, hneg⟩ := s.toJordanDecomposition_spec

Premises used: MeasureTheory.SignedMeasure.toJordanDecomposition_spec
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑μ : Set α → ℝ≥0∞) t = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ s.totalVariation ⟂ₘ μ.ennrealToMeasure

Tactic:
⟨u, hmeas, ?_, ?_⟩

Premises used: MeasureTheory.Measure.MutuallySingular, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑μ : Set α → ℝ≥0∞) t = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
mp : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)
mp₁ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) uᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s.totalVariation ⟂ₘ μ.ennrealToMeasure

Tactic:
refine ⟨u, hmeas, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑μ : Set α → ℝ≥0∞) t = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
mp : (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ u)) ⋯) : ℝ≥0∞) + (↑(NNReal.mk (-(↑s : Set α → ℝ) (iᶜ ∩ u)) ⋯) : ℝ≥0∞) = 0
⊢ Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [totalVariation, Measure.add_apply, hpos, hneg, toMeasureOfZeroLE_apply _ _ _ hmeas,
        toMeasureOfLEZero_apply _ _ _ hmeas]

Premises used: MeasureTheory.SignedMeasure.toMeasureOfZeroLE_apply, MeasureTheory.SignedMeasure.totalVariation, MeasureTheory.Measure.add_apply, MeasureTheory.SignedMeasure.toMeasureOfLEZero_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑μ : Set α → ℝ≥0∞) t = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ u)) ⋯) : ℝ≥0∞) + (↑(NNReal.mk (-(↑s : Set α → ℝ) (iᶜ ∩ u)) ⋯) : ℝ≥0∞) = 0

Tactic:
simp [hu₁ _ Set.inter_subset_right]

Premises used: Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑μ : Set α → ℝ≥0∞) t = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
mp : (↑μ : Set α → ℝ≥0∞) uᶜ = 0
⊢ Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) uᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [VectorMeasure.ennrealToMeasure_apply hmeas.compl]

Premises used: MeasureTheory.VectorMeasure.ennrealToMeasure_apply, MeasurableSet.compl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑μ : Set α → ℝ≥0∞) t = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ (↑μ : Set α → ℝ≥0∞) uᶜ = 0

Tactic:
hu₂ _ (Set.Subset.refl _)

Premises used: Set.Subset.refl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
u : Set α
hmeas : MeasurableSet u
hu₁ : ∀ t ⊆ u, (↑s : Set α → ℝ) t = 0
hu₂ : ∀ t ⊆ uᶜ, (↑μ : Set α → ℝ≥0∞) t = 0
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hpos : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hneg : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
⊢ (↑μ : Set α → ℝ≥0∞) uᶜ = 0

Tactic:
exact hu₂ _ (Set.Subset.refl _)

Premises used: Set.Subset.refl
-- 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∞)
⊢ s ⟂ᵥ μ

Tactic:
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