awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' :
  (∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ j → (↑0 : Set α → ℝ) j_1 ≤ (↑s : Set α → ℝ) j_1) ∧
    ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
⊢ MeasurableSet (i ∩ jᶜ)

Tactic:
exact hi.inter hj.compl

Premises used: MeasurableSet.compl, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' :
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) ∧
    ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' : 0 ≤[j] s ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
⊢ MeasurableSet j

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' : 0 ≤[j] s ∧ ∀ ⦃j_1 : Set α⦄, MeasurableSet j_1 → j_1 ⊆ jᶜ → (↑s : Set α → ℝ) j_1 ≤ (↑0 : Set α → ℝ) j_1
⊢ MeasurableSet i

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ iᶜ → (↑s : Set α → ℝ) j ≤ (↑0 : Set α → ℝ) j
hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0
⊢ MeasurableSet jᶜ

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : MeasurableSet i
hj : MeasurableSet j
hi' : 0 ≤[i] s ∧ s ≤[iᶜ] 0
hj' : 0 ≤[j] s ∧ s ≤[jᶜ] 0
⊢ MeasurableSet iᶜ

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := Measure α) (posPart 0) 0

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
⊢ (-j).posPart = j.negPart

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
⊢ (-j).negPart = j.posPart

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
⊢ (r • j).posPart = r • j.posPart

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
⊢ (r • j).negPart = r • j.negPart

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
r : ℝ
j : JordanDecomposition α
⊢ r • j = if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
rw : (if 0 ≤ (↑r : ℝ) then (↑r : ℝ).toNNReal • j else -((-(↑r : ℝ)).toNNReal • j)) = r • j
rw₁ : (↑r : ℝ).toNNReal • j = r • j
rw₂ rw₃ : r • j = r • j
⊢ (↑r : ℝ) • j = r • j

Tactic:
rw [real_smul_def, if_pos (NNReal.coe_nonneg r), Real.toNNReal_coe]

Premises used: if_pos, NNReal.coe_nonneg, Real.toNNReal_coe, MeasureTheory.JordanDecomposition.real_smul_def
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : 0 ≤ r
⊢ r • j = r.toNNReal • j

Tactic:
dif_pos hr

Premises used: dif_pos, dite, ite
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : r < 0
⊢ r • j = -((-r).toNNReal • j)

Tactic:
dif_neg (not_le.2 hr)

Premises used: not_le, Iff.mpr, dif_neg, dite, ite
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : 0 ≤ r
rw : (if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)).posPart = r.toNNReal • j.posPart
rw₁ : (if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)).posPart = (r.toNNReal • j).posPart
rw₂ rw₃ : (r.toNNReal • j).posPart = (r.toNNReal • j).posPart
⊢ (r • j).posPart = r.toNNReal • j.posPart

Tactic:
rw [real_smul_def, ← smul_posPart, if_pos hr]

Premises used: if_pos, MeasureTheory.JordanDecomposition.smul_posPart, MeasureTheory.JordanDecomposition.real_smul_def
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : 0 ≤ r
rw : (if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)).negPart = r.toNNReal • j.negPart
rw₁ : (if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)).negPart = (r.toNNReal • j).negPart
rw₂ rw₃ : (r.toNNReal • j).negPart = (r.toNNReal • j).negPart
⊢ (r • j).negPart = r.toNNReal • j.negPart

Tactic:
rw [real_smul_def, ← smul_negPart, if_pos hr]

Premises used: if_pos, MeasureTheory.JordanDecomposition.smul_negPart, MeasureTheory.JordanDecomposition.real_smul_def
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : r < 0
rw : (if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)).posPart = (-r).toNNReal • j.negPart
rw₁ : (if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)).posPart = ((-r).toNNReal • j).negPart
rw₂ : (-((-r).toNNReal • j)).posPart = ((-r).toNNReal • j).negPart
rw₃ rw₄ : ((-r).toNNReal • j).negPart = ((-r).toNNReal • j).negPart
⊢ (r • j).posPart = (-r).toNNReal • j.negPart

Tactic:
rw [real_smul_def, ← smul_negPart, if_neg (not_le.2 hr), neg_posPart]

Premises used: not_le, Iff.mpr, MeasureTheory.JordanDecomposition.smul_negPart, MeasureTheory.JordanDecomposition.neg_posPart, if_neg, MeasureTheory.JordanDecomposition.real_smul_def
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : r < 0
rw : (if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)).negPart = (-r).toNNReal • j.posPart
rw₁ : (if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)).negPart = ((-r).toNNReal • j).posPart
rw₂ : (-((-r).toNNReal • j)).negPart = ((-r).toNNReal • j).posPart
rw₃ rw₄ : ((-r).toNNReal • j).posPart = ((-r).toNNReal • j).posPart
⊢ (r • j).negPart = (-r).toNNReal • j.posPart

Tactic:
rw [real_smul_def, ← smul_posPart, if_neg (not_le.2 hr), neg_negPart]

Premises used: not_le, Iff.mpr, MeasureTheory.JordanDecomposition.neg_negPart, MeasureTheory.JordanDecomposition.smul_posPart, if_neg, MeasureTheory.JordanDecomposition.real_smul_def
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
h : ∀ (i : Set α) (hi : MeasurableSet i), (↑(toSignedMeasure 0) : Set α → ℝ) i = (↑0 : Set α → ℝ) i
⊢ Eq.{u_1 + 1} (α := SignedMeasure α) (toSignedMeasure 0) 0

Tactic:
ext1 i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
i : Set α
hi : MeasurableSet i
h :
  (↑(HSub.hSub (α := SignedMeasure α) (Measure.toSignedMeasure (posPart 0)) (Measure.toSignedMeasure (negPart 0))) :
        Set α → ℝ)
      i =
    (↑0 : Set α → ℝ) i
h₁ : Measure.real (m := inst) (posPart 0) i - Measure.real (m := inst) (negPart 0) i = (↑0 : Set α → ℝ) i
h₂ : Measure.real (m := inst) 0 i - Measure.real (m := inst) (negPart 0) i = (↑0 : Set α → ℝ) i
h₃ : Measure.real (m := inst) 0 i - Measure.real (m := inst) 0 i = (↑0 : Set α → ℝ) i
h₄ : Eq (α := ℝ) 0 ((↑0 : Set α → ℝ) i)
h₅ : Eq (α := ℝ) 0 (0 i)
h₆ h₇ : Eq (α := ℝ) 0 0
⊢ (↑(toSignedMeasure 0) : Set α → ℝ) i = (↑0 : Set α → ℝ) i

Tactic:
rw [toSignedMeasure, toSignedMeasure_sub_apply hi, zero_posPart, zero_negPart, sub_self,
    VectorMeasure.coe_zero, Pi.zero_apply]

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure, sub_self, MeasureTheory.VectorMeasure.coe_zero, MeasureTheory.JordanDecomposition.zero_posPart, Pi.zero_apply, MeasureTheory.JordanDecomposition.zero_negPart, MeasureTheory.Measure.toSignedMeasure_sub_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
h : ∀ (i : Set α) (hi : MeasurableSet i), (↑(-j).toSignedMeasure : Set α → ℝ) i = (↑(-j.toSignedMeasure) : Set α → ℝ) i
⊢ (-j).toSignedMeasure = -j.toSignedMeasure

Tactic:
ext1 i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
i : Set α
hi : MeasurableSet i
h : (↑(-j).toSignedMeasure : Set α → ℝ) i = -(↑j.toSignedMeasure : Set α → ℝ) i
h₁ :
  (↑((-j).posPart.toSignedMeasure - (-j).negPart.toSignedMeasure) : Set α → ℝ) i = -(↑j.toSignedMeasure : Set α → ℝ) i
h₂ :
  (↑((-j).posPart.toSignedMeasure - (-j).negPart.toSignedMeasure) : Set α → ℝ) i =
    -(↑(j.posPart.toSignedMeasure - j.negPart.toSignedMeasure) : Set α → ℝ) i
h₃ :
  (-j).posPart.real i - (-j).negPart.real i = -(↑(j.posPart.toSignedMeasure - j.negPart.toSignedMeasure) : Set α → ℝ) i
h₄ : (-j).posPart.real i - (-j).negPart.real i = -(j.posPart.real i - j.negPart.real i)
h₅ : (-j).posPart.real i - (-j).negPart.real i = j.negPart.real i - j.posPart.real i
h₆ : j.negPart.real i - (-j).negPart.real i = j.negPart.real i - j.posPart.real i
h₇ h₈ : j.negPart.real i - j.posPart.real i = j.negPart.real i - j.posPart.real i
⊢ (↑(-j).toSignedMeasure : Set α → ℝ) i = (↑(-j.toSignedMeasure) : Set α → ℝ) i

Tactic:
rw [neg_apply, toSignedMeasure, toSignedMeasure, toSignedMeasure_sub_apply hi,
    toSignedMeasure_sub_apply hi, neg_sub, neg_posPart, neg_negPart]

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure, neg_sub, MeasureTheory.VectorMeasure.neg_apply, MeasureTheory.JordanDecomposition.neg_negPart, MeasureTheory.JordanDecomposition.neg_posPart, MeasureTheory.Measure.toSignedMeasure_sub_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
h :
  ∀ (i : Set α) (hi : MeasurableSet i),
    (↑(r • j).toSignedMeasure : Set α → ℝ) i = (↑(r • j.toSignedMeasure) : Set α → ℝ) i
⊢ (r • j).toSignedMeasure = r • j.toSignedMeasure

Tactic:
ext1 i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
i : Set α
hi : MeasurableSet i
h : (↑r : ℝ) * j.posPart.real i - (↑r : ℝ) * j.negPart.real i = r • j.posPart.real i - r • j.negPart.real i
⊢ (↑(r • j).toSignedMeasure : Set α → ℝ) i = (↑(r • j.toSignedMeasure) : Set α → ℝ) i

Tactic:
rw [VectorMeasure.smul_apply, toSignedMeasure, toSignedMeasure,
    toSignedMeasure_sub_apply hi, toSignedMeasure_sub_apply hi, smul_sub, smul_posPart,
    smul_negPart, measureReal_nnreal_smul_apply, measureReal_nnreal_smul_apply]

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure, MeasureTheory.VectorMeasure.smul_apply, MeasureTheory.JordanDecomposition.smul_posPart, smul_sub, MeasureTheory.JordanDecomposition.smul_negPart, MeasureTheory.Measure.toSignedMeasure_sub_apply, MeasureTheory.measureReal_nnreal_smul_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ (↑r : ℝ) * j.posPart.real i - (↑r : ℝ) * j.negPart.real i = r • j.posPart.real i - r • j.negPart.real i

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
obtain :
  ∀ (S : Set α) (hS₁ : MeasurableSet S) (hS₂ : Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞))
    (hS₃ : Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∃ (S : Set α),
      MeasurableSet S ∧
        j.toSignedMeasure ≤[S] 0 ∧
          0 ≤[Sᶜ] j.toSignedMeasure ∧
            Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞) ∧
              Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (S : Set α),
    MeasurableSet S ∧
      j.toSignedMeasure ≤[S] 0 ∧
        0 ≤[Sᶜ] j.toSignedMeasure ∧
          Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞) ∧
            Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
obtain ⟨S, hS₁, hS₂, hS₃⟩ := j.mutuallySingular

Premises used: MeasureTheory.JordanDecomposition.mutuallySingular
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (S : Set α),
    MeasurableSet S ∧
      j.toSignedMeasure ≤[S] 0 ∧
        0 ≤[Sᶜ] j.toSignedMeasure ∧
          Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞) ∧
            Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
⟨S, hS₁, ?_, ?_, hS₂, hS₃⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
refine_1 : j.toSignedMeasure ≤[S] 0
refine_2 : 0 ≤[Sᶜ] j.toSignedMeasure
⊢ ∃ (S : Set α),
    MeasurableSet S ∧
      j.toSignedMeasure ≤[S] 0 ∧
        0 ≤[Sᶜ] j.toSignedMeasure ∧
          Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞) ∧
            Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine ⟨S, hS₁, ?_, ?_, hS₂, hS₃⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ j.toSignedMeasure ≤[S] 0

Tactic:
restrict_le_restrict_of_subset_le _ _ fun A hA hA₁ => ?_

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
refine_1 : ∀ (A : Set α) (hA : MeasurableSet A) (hA₁ : A ⊆ S), (↑j.toSignedMeasure : Set α → ℝ) A ≤ (↑0 : Set α → ℝ) A
⊢ j.toSignedMeasure ≤[S] 0

Tactic:
refine restrict_le_restrict_of_subset_le _ _ fun A hA hA₁ => ?_

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ S
refine_1 : 0 ≤ j.negPart.real A
⊢ (↑j.toSignedMeasure : Set α → ℝ) A ≤ (↑0 : Set α → ℝ) A

Tactic:
rw [toSignedMeasure, toSignedMeasure_sub_apply hA, measureReal_def,
      show j.posPart A = 0 from nonpos_iff_eq_zero.1 (hS₂ ▸ measure_mono hA₁), ENNReal.toReal_zero,
      zero_sub, neg_le, zero_apply, neg_zero]

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure, neg_le, MeasureTheory.VectorMeasure.zero_apply, ENNReal.toReal_zero, Iff.mp, MeasureTheory.measureReal_def, MeasureTheory.Measure.toSignedMeasure_sub_apply, neg_zero, zero_sub, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ S
⊢ 0 ≤ j.negPart.real A

Tactic:
ENNReal.toReal_nonneg

Premises used: MeasureTheory.Measure.real, ENNReal.toReal_nonneg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ S
⊢ 0 ≤ j.negPart.real A

Tactic:
exact ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ 0 ≤[Sᶜ] j.toSignedMeasure

Tactic:
restrict_le_restrict_of_subset_le _ _ fun A hA hA₁ => ?_

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
refine_2 : ∀ (A : Set α) (hA : MeasurableSet A) (hA₁ : A ⊆ Sᶜ), (↑0 : Set α → ℝ) A ≤ (↑j.toSignedMeasure : Set α → ℝ) A
⊢ 0 ≤[Sᶜ] j.toSignedMeasure

Tactic:
refine restrict_le_restrict_of_subset_le _ _ fun A hA hA₁ => ?_

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ Sᶜ
refine_2 : (↑0 : Set α → ℝ) A ≤ j.posPart.real A
⊢ (↑0 : Set α → ℝ) A ≤ (↑j.toSignedMeasure : Set α → ℝ) A

Tactic:
rw [toSignedMeasure, toSignedMeasure_sub_apply hA, measureReal_def (μ := j.negPart),
      show j.negPart A = 0 from nonpos_iff_eq_zero.1 (hS₃ ▸ measure_mono hA₁), ENNReal.toReal_zero,
      sub_zero]

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure, sub_zero, MeasureTheory.JordanDecomposition.negPart, ENNReal.toReal_zero, Iff.mp, MeasureTheory.measureReal_def, MeasureTheory.Measure.toSignedMeasure_sub_apply, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ Sᶜ
⊢ (↑0 : Set α → ℝ) A ≤ j.posPart.real A

Tactic:
ENNReal.toReal_nonneg

Premises used: MeasureTheory.Measure.real, ENNReal.toReal_nonneg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ Sᶜ
⊢ (↑0 : Set α → ℝ) A ≤ j.posPart.real A

Tactic:
exact ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s_1 s : SignedMeasure α
i : Set α := ⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0)
hi :
  MeasurableSet (⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0)) ∧
    0 ≤[⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0)] s ∧
      s ≤[(⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0))ᶜ] 0
⊢ s.toMeasureOfZeroLE i ⋯ ⋯ ⟂ₘ s.toMeasureOfLEZero iᶜ ⋯ ⋯

Tactic:
⟨iᶜ, hi.1.compl, ?_, ?_⟩

Premises used: Compl.compl, MeasurableSet.compl, And.left, MeasureTheory.Measure.MutuallySingular, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s_1 s : SignedMeasure α
i : Set α := ⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0)
hi :
  MeasurableSet (⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0)) ∧
    0 ≤[⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0)] s ∧
      s ≤[(⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0))ᶜ] 0
refine_1 : Eq (α := ℝ≥0∞) ((s.toMeasureOfZeroLE i ⋯ ⋯ : (a : Set α) → ℝ≥0∞) iᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
refine_2 : Eq (α := ℝ≥0∞) ((s.toMeasureOfLEZero iᶜ ⋯ ⋯ : (a : Set α) → ℝ≥0∞) iᶜᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s.toMeasureOfZeroLE i ⋯ ⋯ ⟂ₘ s.toMeasureOfLEZero iᶜ ⋯ ⋯

Tactic:
refine ⟨iᶜ, hi.1.compl, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s_1 s : SignedMeasure α
i : Set α := ⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0)
hi :
  MeasurableSet (⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0)) ∧
    0 ≤[⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0)] s ∧
      s ≤[(⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0))ᶜ] 0
refine_1 :
  (↑(NNReal.mk
          ((↑s : Set α → ℝ)
            (⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0) ∩
              (⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0))ᶜ))
          ⋯) :
      ℝ≥0∞) =
    0
⊢ Eq (α := ℝ≥0∞) ((s.toMeasureOfZeroLE i ⋯ ⋯ : (a : Set α) → ℝ≥0∞) iᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [toMeasureOfZeroLE_apply _ _ hi.1 hi.1.compl]

Premises used: MeasureTheory.SignedMeasure.toMeasureOfZeroLE_apply, MeasurableSet.compl, And.left
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s_1 s : SignedMeasure α
i : Set α := ⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0)
hi :
  MeasurableSet (⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0)) ∧
    0 ≤[⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0)] s ∧
      s ≤[(⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0))ᶜ] 0
⊢ (↑(NNReal.mk
          ((↑s : Set α → ℝ)
            (⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0) ∩
              (⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0))ᶜ))
          ⋯) :
      ℝ≥0∞) =
    0

Tactic:
simp