awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : Eq (α := ℝ≥0∞) ((j₁.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₅ : Eq (α := ℝ≥0∞) ((j₁.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : Eq (α := ℝ≥0∞) ((j₂.posPart : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₅ : Eq (α := ℝ≥0∞) ((j₂.negPart : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hST₁ : (↑j₁.toSignedMeasure : Set α → ℝ) (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : j₁.posPart.real i = (↑j₁.toSignedMeasure : Set α → ℝ) (i ∩ Sᶜ)
⊢ j₂.posPart.real i = (↑j₂.toSignedMeasure : Set α → ℝ) (i ∩ Tᶜ)

Tactic:
have hμ₂ : j₂.posPart.real i = j₂.toSignedMeasure (i ∩ Tᶜ) := by
    rw [toSignedMeasure, toSignedMeasure_sub_apply (hi.inter hT₁.compl),
      measureReal_def (μ := j₂.negPart),
      show j₂.negPart (i ∩ Tᶜ) = 0 from
        nonpos_iff_eq_zero.1 (hT₅ ▸ measure_mono Set.inter_subset_right),
      ENNReal.toReal_zero, sub_zero]
    conv_lhs => rw [← Set.inter_union_compl i T]
    rw [measureReal_union, measureReal_def,
      show j₂.posPart (i ∩ T) = 0 from
        nonpos_iff_eq_zero.1 (hT₄ ▸ measure_mono Set.inter_subset_right),
      ENNReal.toReal_zero, zero_add]
    · exact
        Set.disjoint_of_subset_left Set.inter_subset_right
          (Set.disjoint_of_subset_right Set.inter_subset_right disjoint_compl_right)
    · exact hi.inter hT₁.compl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : Eq (α := ℝ≥0∞) ((j₁.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₅ : Eq (α := ℝ≥0∞) ((j₁.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : Eq (α := ℝ≥0∞) ((j₂.posPart : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₅ : Eq (α := ℝ≥0∞) ((j₂.negPart : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hST₁ : (↑j₁.toSignedMeasure : Set α → ℝ) (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : j₁.posPart.real i = (↑j₁.toSignedMeasure : Set α → ℝ) (i ∩ Sᶜ)
hμ₂ : j₂.posPart.real i = (↑j₂.toSignedMeasure : Set α → ℝ) (i ∩ Tᶜ)
h : (↑j₁.toSignedMeasure : Set α → ℝ) (i ∩ Sᶜ) = (↑j₁.toSignedMeasure : Set α → ℝ) (i ∩ Tᶜ)
⊢ Eq (α := ℝ≥0∞) ((j₁.posPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((j₂.posPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)

Tactic:
rw [← measureReal_eq_measureReal_iff, hμ₁, hμ₂, ← hj]

Premises used: MeasureTheory.measureReal_eq_measureReal_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : Eq (α := ℝ≥0∞) ((j₁.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₅ : Eq (α := ℝ≥0∞) ((j₁.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : Eq (α := ℝ≥0∞) ((j₂.posPart : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₅ : Eq (α := ℝ≥0∞) ((j₂.negPart : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hST₁ : (↑j₁.toSignedMeasure : Set α → ℝ) (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : j₁.posPart.real i = (↑j₁.toSignedMeasure : Set α → ℝ) (i ∩ Sᶜ)
hμ₂ : j₂.posPart.real i = (↑j₂.toSignedMeasure : Set α → ℝ) (i ∩ Tᶜ)
⊢ (↑j₁.toSignedMeasure : Set α → ℝ) (i ∩ Sᶜ) = (↑j₁.toSignedMeasure : Set α → ℝ) (i ∩ Tᶜ)

Tactic:
of_inter_eq_of_symmDiff_eq_zero_positive hS₁.compl hT₁.compl hi hS₃ hT₃ hST₁

Premises used: MeasurableSet.compl, MeasureTheory.SignedMeasure.of_inter_eq_of_symmDiff_eq_zero_positive
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
S : Set α
hS₁ : MeasurableSet S
hS₂ : j₁.toSignedMeasure ≤[S] 0
hS₃ : 0 ≤[Sᶜ] j₁.toSignedMeasure
hS₄ : Eq (α := ℝ≥0∞) ((j₁.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₅ : Eq (α := ℝ≥0∞) ((j₁.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : j₁.toSignedMeasure ≤[T] 0
hT₃ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₄ : Eq (α := ℝ≥0∞) ((j₂.posPart : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₅ : Eq (α := ℝ≥0∞) ((j₂.negPart : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hST₁ : (↑j₁.toSignedMeasure : Set α → ℝ) (symmDiff Sᶜ Tᶜ) = 0
i : Set α
hi : MeasurableSet i
hμ₁ : j₁.posPart.real i = (↑j₁.toSignedMeasure : Set α → ℝ) (i ∩ Sᶜ)
hμ₂ : j₂.posPart.real i = (↑j₂.toSignedMeasure : Set α → ℝ) (i ∩ Tᶜ)
⊢ (↑j₁.toSignedMeasure : Set α → ℝ) (i ∩ Sᶜ) = (↑j₁.toSignedMeasure : Set α → ℝ) (i ∩ Tᶜ)

Tactic:
exact of_inter_eq_of_symmDiff_eq_zero_positive hS₁.compl hT₁.compl hi hS₃ hT₃ hST₁

Premises used: MeasurableSet.compl, MeasureTheory.SignedMeasure.of_inter_eq_of_symmDiff_eq_zero_positive
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
⊢ j.toSignedMeasure = j.toSignedMeasure.toJordanDecomposition.toSignedMeasure

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
a : Eq.{u_1 + 1} (α := SignedMeasure α) (toSignedMeasure (toJordanDecomposition 0)) (toSignedMeasure 0)
⊢ Eq.{u_1 + 1} (α := JordanDecomposition α) (toJordanDecomposition 0) 0

Tactic:
apply toSignedMeasure_injective

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure_injective
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := SignedMeasure α) (toSignedMeasure (toJordanDecomposition 0)) (toSignedMeasure 0)

Tactic:
simp [toSignedMeasure_zero]

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
a : (-s).toJordanDecomposition.toSignedMeasure = (-s.toJordanDecomposition).toSignedMeasure
⊢ (-s).toJordanDecomposition = -s.toJordanDecomposition

Tactic:
apply toSignedMeasure_injective

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure_injective
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
⊢ (-s).toJordanDecomposition.toSignedMeasure = (-s.toJordanDecomposition).toSignedMeasure

Tactic:
simp [toSignedMeasure_neg]

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
a : (r • s).toJordanDecomposition.toSignedMeasure = (r • s.toJordanDecomposition).toSignedMeasure
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition

Tactic:
apply toSignedMeasure_injective

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure_injective
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ (r • s).toJordanDecomposition.toSignedMeasure = (r • s.toJordanDecomposition).toSignedMeasure

Tactic:
simp [toSignedMeasure_smul]

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure_smul
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ r

Tactic:
hr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : 0 ≤ r
lift : ∀ (r : ℝ≥0), ((↑r : ℝ) • s).toJordanDecomposition = (↑r : ℝ) • s.toJordanDecomposition
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition

Tactic:
lift r to ℝ≥0 using hr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
rw : ((↑r : ℝ) • s).toJordanDecomposition = (r • s).toJordanDecomposition
⊢ ((↑r : ℝ) • s).toJordanDecomposition = (↑r : ℝ) • s.toJordanDecomposition

Tactic:
rw [JordanDecomposition.coe_smul, ← toJordanDecomposition_smul]

Premises used: MeasureTheory.JordanDecomposition.coe_smul, MeasureTheory.SignedMeasure.toJordanDecomposition_smul
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ ((↑r : ℝ) • s).toJordanDecomposition = (r • s).toJordanDecomposition

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
pos : ∀ (hr : 0 ≤ r), (r • s).toJordanDecomposition = r • s.toJordanDecomposition
neg : ∀ (hr : r < 0), (r • s).toJordanDecomposition = r • s.toJordanDecomposition
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition

Tactic:
by_cases! hr : 0 ≤ r
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : 0 ≤ r
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition

Tactic:
toJordanDecomposition_smul_real_nonneg s r hr

Premises used: _private.0.MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real_nonneg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : 0 ≤ r
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition

Tactic:
exact toJordanDecomposition_smul_real_nonneg s r hr

Premises used: _private.0.MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real_nonneg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
neg : (r • s).toJordanDecomposition.posPart = (r • s.toJordanDecomposition).posPart
neg₁ : (r • s).toJordanDecomposition.negPart = (r • s.toJordanDecomposition).negPart
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
rw : r • s = - -(r • s)
rw₁ rw₂ : r • s = r • s
⊢ r • s = -(-r • s)

Tactic:
rw [neg_smul, neg_neg]

Premises used: neg_smul, neg_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
neg neg₁ : 0 ≤ -r
⊢ (r • s).toJordanDecomposition.posPart = (r • s.toJordanDecomposition).posPart

Tactic:
rw [real_smul_posPart_neg _ _ hr,
        show r • s = -(-r • s) by rw [neg_smul, neg_neg], toJordanDecomposition_neg, neg_posPart,
        toJordanDecomposition_smul_real_nonneg, ← smul_negPart, real_smul_nonneg]

Premises used: MeasureTheory.JordanDecomposition.real_smul_nonneg, MeasureTheory.SignedMeasure.toJordanDecomposition_neg, _private.0.MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real_nonneg, MeasureTheory.JordanDecomposition.smul_negPart, MeasureTheory.JordanDecomposition.real_smul_posPart_neg, MeasureTheory.JordanDecomposition.neg_posPart
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
⊢ 0 ≤ -r

Tactic:
Left.nonneg_neg_iff.2 hr.le

Premises used: Iff.mpr, LT.lt.le, Left.nonneg_neg_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
⊢ 0 ≤ -r

Tactic:
exact Left.nonneg_neg_iff.2 hr.le

Premises used: Iff.mpr, LT.lt.le, Left.nonneg_neg_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
neg neg₁ : 0 ≤ -r
⊢ (r • s).toJordanDecomposition.negPart = (r • s.toJordanDecomposition).negPart

Tactic:
rw [real_smul_negPart_neg _ _ hr,
        show r • s = -(-r • s) by rw [neg_smul, neg_neg], toJordanDecomposition_neg, neg_negPart,
        toJordanDecomposition_smul_real_nonneg, ← smul_posPart, real_smul_nonneg]

Premises used: MeasureTheory.JordanDecomposition.real_smul_nonneg, MeasureTheory.JordanDecomposition.neg_negPart, MeasureTheory.SignedMeasure.toJordanDecomposition_neg, MeasureTheory.JordanDecomposition.smul_posPart, _private.0.MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real_nonneg, MeasureTheory.JordanDecomposition.real_smul_negPart_neg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
j : JordanDecomposition α
h : s = j.toSignedMeasure
rw : j.toSignedMeasure.toJordanDecomposition = j
rw₁ rw₂ : j = j
⊢ s.toJordanDecomposition = j

Tactic:
rw [h, toJordanDecomposition_toSignedMeasure]

Premises used: MeasureTheory.JordanDecomposition.toJordanDecomposition_toSignedMeasure
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := Measure α) (totalVariation 0) 0

Tactic:
simp [totalVariation, toJordanDecomposition_zero]

Premises used: MeasureTheory.SignedMeasure.totalVariation, MeasureTheory.SignedMeasure.toJordanDecomposition_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
⊢ (-s).totalVariation = s.totalVariation

Tactic:
simp [totalVariation, toJordanDecomposition_neg, add_comm]

Premises used: MeasureTheory.SignedMeasure.totalVariation, MeasureTheory.SignedMeasure.toJordanDecomposition_neg, add_comm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [totalVariation, Measure.coe_add, Pi.add_apply, add_eq_zero] at hs

Premises used: MeasureTheory.SignedMeasure.totalVariation, MeasureTheory.Measure.coe_add, Pi.add_apply, add_eq_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs :
  Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  ((if MeasurableSet i then s.toJordanDecomposition.posPart.real i else 0) -
      if MeasurableSet i then s.toJordanDecomposition.negPart.real i else 0) =
    0
⊢ (↑s : Set α → ℝ) i = 0

Tactic:
rw [← toSignedMeasure_toJordanDecomposition s, toSignedMeasure, VectorMeasure.coe_sub,
    Pi.sub_apply, Measure.toSignedMeasure_apply, Measure.toSignedMeasure_apply]

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure, MeasureTheory.VectorMeasure.coe_sub, MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition, MeasureTheory.Measure.toSignedMeasure_apply, Pi.sub_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs :
  Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)
pos :
  ∀ (hi : MeasurableSet i),
    ((if MeasurableSet i then s.toJordanDecomposition.posPart.real i else 0) -
        if MeasurableSet i then s.toJordanDecomposition.negPart.real i else 0) =
      0
neg :
  ∀ (hi : ¬MeasurableSet i),
    ((if MeasurableSet i then s.toJordanDecomposition.posPart.real i else 0) -
        if MeasurableSet i then s.toJordanDecomposition.negPart.real i else 0) =
      0
⊢ ((if MeasurableSet i then s.toJordanDecomposition.posPart.real i else 0) -
      if MeasurableSet i then s.toJordanDecomposition.negPart.real i else 0) =
    0

Tactic:
by_cases hi : MeasurableSet i

Premises used: MeasurableSet
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs :
  Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)
hi : MeasurableSet i
⊢ ((if MeasurableSet i then s.toJordanDecomposition.posPart.real i else 0) -
      if MeasurableSet i then s.toJordanDecomposition.negPart.real i else 0) =
    0

Tactic:
simp [hs.1, hs.2, measureReal_def]

Premises used: And.right, And.left, MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs :
  Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.posPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((s.toJordanDecomposition.negPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)
hi : ¬MeasurableSet i
⊢ ((if MeasurableSet i then s.toJordanDecomposition.posPart.real i else 0) -
      if MeasurableSet i then s.toJordanDecomposition.negPart.real i else 0) =
    0

Tactic:
simp [if_neg hi]

Premises used: if_neg
-- 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∞
h : s ≪ᵥ μ
⊢ s.totalVariation ≪ μ.ennrealToMeasure

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

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

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

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥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₃),
    Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)

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∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥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 ∩ S)) ⋯) : ℝ≥0∞) + (↑(NNReal.mk (-(↑s : Set α → ℝ) (iᶜ ∩ S)) ⋯) : ℝ≥0∞) = 0
⊢ Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)

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

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∞
h : s ≪ᵥ μ
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥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 :
  ∀
    (h :
      ∀ ⦃s_1 : Set α⦄,
        Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (0 : ℝ≥0∞) → (↑s : Set α → ℝ) s_1 = 0)
    (S : Set α) (hS₁ : MeasurableSet S)
    (hS₂ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥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 ∩ S)) ⋯) : ℝ≥0∞) + (↑(NNReal.mk (-(↑s : Set α → ℝ) (iᶜ ∩ S)) ⋯) : ℝ≥0∞) = 0
⊢ (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ S)) ⋯) : ℝ≥0∞) + (↑(NNReal.mk (-(↑s : Set α → ℝ) (iᶜ ∩ S)) ⋯) : ℝ≥0∞) = 0

Tactic:
rw [← VectorMeasure.AbsolutelyContinuous.ennrealToMeasure] at h

Premises used: MeasureTheory.VectorMeasure.AbsolutelyContinuous.ennrealToMeasure
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h :
  ∀ ⦃s_1 : Set α⦄,
    Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (0 : ℝ≥0∞) → (↑s : Set α → ℝ) s_1 = 0
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥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 ∩ S)) ⋯) : ℝ≥0∞) + (↑(NNReal.mk (-(↑s : Set α → ℝ) (iᶜ ∩ S)) ⋯) : ℝ≥0∞) = 0

Tactic:
simp [h (measure_mono_null (i.inter_subset_right) hS₂),
      h (measure_mono_null (iᶜ.inter_subset_right) hS₂)]

Premises used: MeasureTheory.measure_mono_null, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s.totalVariation ≪ μ.ennrealToMeasure
⊢ s ≪ᵥ μ

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

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

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

Premises used: MeasureTheory.VectorMeasure.AbsolutelyContinuous.mk
-- 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₂ : (↑μ : Set α → ℝ≥0∞) S = 0
⊢ Eq (α := ℝ≥0∞) ((μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← VectorMeasure.ennrealToMeasure_apply hS₁] at hS₂

Premises used: MeasureTheory.VectorMeasure.ennrealToMeasure_apply