awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (r • j).posPart = r.toNNReal • j.posPart
have rw₁ : (if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)).posPart = (r.toNNReal • j).posPart
Tactic: rw [real_smul_def, ← smul_posPart, if_pos hr]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (r • j).posPart = r.toNNReal • j.posPart
have rw₂ : (r.toNNReal • j).posPart = (r.toNNReal • j).posPart
Tactic: rw [real_smul_def, ← smul_posPart, if_pos hr]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : 0 ≤ r
⊢ (r • j).negPart = r.toNNReal • j.negPart
have rw : (if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)).negPart = r.toNNReal • j.negPart
Tactic: rw [real_smul_def, ← smul_negPart, if_pos hr]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (r • j).negPart = r.toNNReal • j.negPart
have rw₁ : (if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)).negPart = (r.toNNReal • j).negPart
Tactic: rw [real_smul_def, ← smul_negPart, if_pos hr]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (r • j).negPart = r.toNNReal • j.negPart
have rw₂ : (r.toNNReal • j).negPart = (r.toNNReal • j).negPart
Tactic: rw [real_smul_def, ← smul_negPart, if_pos hr]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : r < 0
⊢ (r • j).posPart = (-r).toNNReal • j.negPart
have rw : (if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)).posPart = (-r).toNNReal • j.negPart
Tactic: rw [real_smul_def, ← smul_negPart, if_neg (not_le.2 hr), neg_posPart]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (r • j).posPart = (-r).toNNReal • j.negPart
have rw₁ : (if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)).posPart = ((-r).toNNReal • j).negPart
Tactic: rw [real_smul_def, ← smul_negPart, if_neg (not_le.2 hr), neg_posPart]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (r • j).posPart = (-r).toNNReal • j.negPart
have rw₂ : (-((-r).toNNReal • j)).posPart = ((-r).toNNReal • j).negPart
Tactic: rw [real_smul_def, ← smul_negPart, if_neg (not_le.2 hr), neg_posPart]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (r • j).posPart = (-r).toNNReal • j.negPart
have rw₃ : ((-r).toNNReal • j).negPart = ((-r).toNNReal • j).negPart
Tactic: rw [real_smul_def, ← smul_negPart, if_neg (not_le.2 hr), neg_posPart]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : r < 0
⊢ (r • j).negPart = (-r).toNNReal • j.posPart
have rw : (if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)).negPart = (-r).toNNReal • j.posPart
Tactic: rw [real_smul_def, ← smul_posPart, if_neg (not_le.2 hr), neg_negPart]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (r • j).negPart = (-r).toNNReal • j.posPart
have rw₁ : (if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)).negPart = ((-r).toNNReal • j).posPart
Tactic: rw [real_smul_def, ← smul_posPart, if_neg (not_le.2 hr), neg_negPart]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (r • j).negPart = (-r).toNNReal • j.posPart
have rw₂ : (-((-r).toNNReal • j)).negPart = ((-r).toNNReal • j).posPart
Tactic: rw [real_smul_def, ← smul_posPart, if_neg (not_le.2 hr), neg_negPart]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (r • j).negPart = (-r).toNNReal • j.posPart
have rw₃ : ((-r).toNNReal • j).posPart = ((-r).toNNReal • j).posPart
Tactic: rw [real_smul_def, ← smul_posPart, if_neg (not_le.2 hr), neg_negPart]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := SignedMeasure α) (toSignedMeasure 0) 0
have h : ∀ (i : Set α) (hi : MeasurableSet i), (↑(toSignedMeasure 0) : Set α → ℝ) i = (↑0 : Set α → ℝ) i
Tactic: ext1 i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
i : Set α
hi : MeasurableSet i
⊢ (↑(toSignedMeasure 0) : Set α → ℝ) i = (↑0 : Set α → ℝ) i
have h : (↑(HSub.hSub (α := SignedMeasure α) (Measure.toSignedMeasure (posPart 0)) (Measure.toSignedMeasure (negPart 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (↑(toSignedMeasure 0) : Set α → ℝ) i = (↑0 : Set α → ℝ) i
have h₁ : Measure.real (m := inst) (posPart 0) i - Measure.real (m := inst) (negPart 0) i = (↑0 : Set α → ℝ) i
Tactic: rw [toSignedMeasure, toSignedMeasure_sub_apply hi, zero_posPart, zero_negPart, sub_self,
    VectorMeasure.coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (↑(toSignedMeasure 0) : Set α → ℝ) i = (↑0 : Set α → ℝ) i
have h₂ : Measure.real (m := inst) 0 i - Measure.real (m := inst) (negPart 0) i = (↑0 : Set α → ℝ) i
Tactic: rw [toSignedMeasure, toSignedMeasure_sub_apply hi, zero_posPart, zero_negPart, sub_self,
    VectorMeasure.coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (↑(toSignedMeasure 0) : Set α → ℝ) i = (↑0 : Set α → ℝ) i
have h₃ : Measure.real (m := inst) 0 i - Measure.real (m := inst) 0 i = (↑0 : Set α → ℝ) i
Tactic: rw [toSignedMeasure, toSignedMeasure_sub_apply hi, zero_posPart, zero_negPart, sub_self,
    VectorMeasure.coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (↑(toSignedMeasure 0) : Set α → ℝ) i = (↑0 : Set α → ℝ) i
have h₄ : Eq (α := ℝ) 0 ((↑0 : Set α → ℝ) i)
Tactic: rw [toSignedMeasure, toSignedMeasure_sub_apply hi, zero_posPart, zero_negPart, sub_self,
    VectorMeasure.coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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)
⊢ (↑(toSignedMeasure 0) : Set α → ℝ) i = (↑0 : Set α → ℝ) i
have h₅ : Eq (α := ℝ) 0 (0 i)
Tactic: rw [toSignedMeasure, toSignedMeasure_sub_apply hi, zero_posPart, zero_negPart, sub_self,
    VectorMeasure.coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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)
⊢ (↑(toSignedMeasure 0) : Set α → ℝ) i = (↑0 : Set α → ℝ) i
have h₆ : Eq (α := ℝ) 0 0
Tactic: rw [toSignedMeasure, toSignedMeasure_sub_apply hi, zero_posPart, zero_negPart, sub_self,
    VectorMeasure.coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
⊢ (-j).toSignedMeasure = -j.toSignedMeasure
have h : ∀ (i : Set α) (hi : MeasurableSet i), (↑(-j).toSignedMeasure : Set α → ℝ) i = (↑(-j.toSignedMeasure) : Set α → ℝ) i
Tactic: ext1 i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
i : Set α
hi : MeasurableSet i
⊢ (↑(-j).toSignedMeasure : Set α → ℝ) i = (↑(-j.toSignedMeasure) : Set α → ℝ) i
have h : (↑(-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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
i : Set α
hi : MeasurableSet i
h : (↑(-j).toSignedMeasure : Set α → ℝ) i = -(↑j.toSignedMeasure : Set α → ℝ) i
⊢ (↑(-j).toSignedMeasure : Set α → ℝ) i = (↑(-j.toSignedMeasure) : Set α → ℝ) i
have h₁ : (↑((-j).posPart.toSignedMeasure - (-j).negPart.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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (↑(-j).toSignedMeasure : Set α → ℝ) i = (↑(-j.toSignedMeasure) : Set α → ℝ) i
have h₂ : (↑((-j).posPart.toSignedMeasure - (-j).negPart.toSignedMeasure) : Set α → ℝ) i =
  -(↑(j.posPart.toSignedMeasure - j.negPart.toSignedMeasure) : Set α → ℝ) i
Tactic: rw [neg_apply, toSignedMeasure, toSignedMeasure, toSignedMeasure_sub_apply hi,
    toSignedMeasure_sub_apply hi, neg_sub, neg_posPart, neg_negPart]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (↑(-j).toSignedMeasure : Set α → ℝ) i = (↑(-j.toSignedMeasure) : Set α → ℝ) i
have h₃ : (-j).posPart.real i - (-j).negPart.real i = -(↑(j.posPart.toSignedMeasure - j.negPart.toSignedMeasure) : Set α → ℝ) i
Tactic: rw [neg_apply, toSignedMeasure, toSignedMeasure, toSignedMeasure_sub_apply hi,
    toSignedMeasure_sub_apply hi, neg_sub, neg_posPart, neg_negPart]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (↑(-j).toSignedMeasure : Set α → ℝ) i = (↑(-j.toSignedMeasure) : Set α → ℝ) i
have h₄ : (-j).posPart.real i - (-j).negPart.real i = -(j.posPart.real i - j.negPart.real i)
Tactic: rw [neg_apply, toSignedMeasure, toSignedMeasure, toSignedMeasure_sub_apply hi,
    toSignedMeasure_sub_apply hi, neg_sub, neg_posPart, neg_negPart]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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)
⊢ (↑(-j).toSignedMeasure : Set α → ℝ) i = (↑(-j.toSignedMeasure) : Set α → ℝ) i
have h₅ : (-j).posPart.real i - (-j).negPart.real i = j.negPart.real i - j.posPart.real i
Tactic: rw [neg_apply, toSignedMeasure, toSignedMeasure, toSignedMeasure_sub_apply hi,
    toSignedMeasure_sub_apply hi, neg_sub, neg_posPart, neg_negPart]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (↑(-j).toSignedMeasure : Set α → ℝ) i = (↑(-j.toSignedMeasure) : Set α → ℝ) i
have h₆ : j.negPart.real i - (-j).negPart.real i = j.negPart.real i - j.posPart.real i
Tactic: rw [neg_apply, toSignedMeasure, toSignedMeasure, toSignedMeasure_sub_apply hi,
    toSignedMeasure_sub_apply hi, neg_sub, neg_posPart, neg_negPart]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (↑(-j).toSignedMeasure : Set α → ℝ) i = (↑(-j.toSignedMeasure) : Set α → ℝ) i
have h₇ : j.negPart.real i - j.posPart.real i = j.negPart.real i - j.posPart.real i
Tactic: rw [neg_apply, toSignedMeasure, toSignedMeasure, toSignedMeasure_sub_apply hi,
    toSignedMeasure_sub_apply hi, neg_sub, neg_posPart, neg_negPart]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
⊢ (r • j).toSignedMeasure = r • j.toSignedMeasure
have h : ∀ (i : Set α) (hi : MeasurableSet i),
  (↑(r • j).toSignedMeasure : Set α → ℝ) i = (↑(r • j.toSignedMeasure) : Set α → ℝ) i
Tactic: ext1 i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ (↑(r • j).toSignedMeasure : Set α → ℝ) i = (↑(r • j.toSignedMeasure) : Set α → ℝ) i
have h : (↑r : ℝ) * j.posPart.real i - (↑r : ℝ) * j.negPart.real i = r • j.posPart.real i - r • j.negPart.real 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
⊢ ∃ (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∞)
have 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∞)
Tactic: obtain ⟨S, hS₁, hS₂, hS₃⟩ := j.mutuallySingular
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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∞)
have refine_1 : j.toSignedMeasure ≤[S] 0
Tactic: refine ⟨S, hS₁, ?_, ?_, hS₂, hS₃⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ ∃ (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∞)
have refine_2 : 0 ≤[Sᶜ] j.toSignedMeasure
Tactic: refine ⟨S, hS₁, ?_, ?_, hS₂, hS₃⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
have refine_1 : ∀ (A : Set α) (hA : MeasurableSet A) (hA₁ : A ⊆ S), (↑j.toSignedMeasure : Set α → ℝ) A ≤ (↑0 : Set α → ℝ) A
Tactic: refine restrict_le_restrict_of_subset_le _ _ fun A hA hA₁ => ?_