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₁ 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
⊢ j₁.posPart.real i = j₁.posPart.real (i ∩ Sᶜ)
have conv_lhs : j₁.posPart.real (i ∩ S ∪ i ∩ Sᶜ) = j₁.posPart.real (i ∩ Sᶜ)
Tactic: conv_lhs => rw [← Set.inter_union_compl i S]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ j₁.posPart.real (i ∩ S ∪ i ∩ Sᶜ) = j₁.posPart.real (i ∩ Sᶜ)
have hd : Disjoint (i ∩ S) (i ∩ Sᶜ)
Tactic: rw [measureReal_union, measureReal_def,
      show j₁.posPart (i ∩ S) = 0 from
        nonpos_iff_eq_zero.1 (hS₄ ▸ measure_mono Set.inter_subset_right),
      ENNReal.toReal_zero, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
hd : Disjoint (i ∩ S) (i ∩ Sᶜ)
⊢ j₁.posPart.real (i ∩ S ∪ i ∩ Sᶜ) = j₁.posPart.real (i ∩ Sᶜ)
have h : MeasurableSet (i ∩ Sᶜ)
Tactic: rw [measureReal_union, measureReal_def,
      show j₁.posPart (i ∩ S) = 0 from
        nonpos_iff_eq_zero.1 (hS₄ ▸ measure_mono Set.inter_subset_right),
      ENNReal.toReal_zero, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
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
⊢ Eq (α := ℝ≥0∞) ((j₁.posPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((j₂.posPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
have hμ₁ : j₁.posPart.real i = (↑j₁.toSignedMeasure : Set α → ℝ) (i ∩ Sᶜ)
Tactic: have hμ₁ : j₁.posPart.real i = j₁.toSignedMeasure (i ∩ Sᶜ) := by
    rw [toSignedMeasure, toSignedMeasure_sub_apply (hi.inter hS₁.compl),
      measureReal_def (μ := j₁.negPart),
      show j₁.negPart (i ∩ Sᶜ) = 0 from
        nonpos_iff_eq_zero.1 (hS₅ ▸ measure_mono Set.inter_subset_right),
      ENNReal.toReal_zero, sub_zero]
    conv_lhs => rw [← Set.inter_union_compl i S]
    rw [measureReal_union, measureReal_def,
      show j₁.posPart (i ∩ S) = 0 from
        nonpos_iff_eq_zero.1 (hS₄ ▸ measure_mono Set.inter_subset_right),
      ENNReal.toReal_zero, zero_add]
    · refine
        Set.disjoint_of_subset_left Set.inter_subset_right
          (Set.disjoint_of_subset_right Set.inter_subset_right disjoint_compl_right)
    · exact hi.inter hS₁.compl
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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ᶜ)
have rw : j₂.posPart.real i = j₂.posPart.real (i ∩ Tᶜ)
Tactic: 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
have rw : j₂.posPart.real (i ∩ T ∪ i ∩ Tᶜ)
Tactic: rw [← Set.inter_union_compl i T]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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₂.posPart.real (i ∩ Tᶜ)
have conv_lhs : j₂.posPart.real (i ∩ T ∪ i ∩ Tᶜ) = j₂.posPart.real (i ∩ Tᶜ)
Tactic: conv_lhs => rw [← Set.inter_union_compl i T]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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 ∩ T ∪ i ∩ Tᶜ) = j₂.posPart.real (i ∩ Tᶜ)
have hd : Disjoint (i ∩ T) (i ∩ Tᶜ)
Tactic: 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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ᶜ)
hd : Disjoint (i ∩ T) (i ∩ Tᶜ)
⊢ j₂.posPart.real (i ∩ T ∪ i ∩ Tᶜ) = j₂.posPart.real (i ∩ Tᶜ)
have h : MeasurableSet (i ∩ Tᶜ)
Tactic: 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
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ᶜ)
⊢ Eq (α := ℝ≥0∞) ((j₁.posPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((j₂.posPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
have hμ₂ : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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ᶜ)
⊢ Eq (α := ℝ≥0∞) ((j₁.posPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((j₂.posPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
have h : (↑j₁.toSignedMeasure : Set α → ℝ) (i ∩ Sᶜ) = (↑j₁.toSignedMeasure : Set α → ℝ) (i ∩ Tᶜ)
Tactic: rw [← measureReal_eq_measureReal_iff, hμ₁, hμ₂, ← hj]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := JordanDecomposition α) (toJordanDecomposition 0) 0
have a : Eq.{u_1 + 1} (α := SignedMeasure α) (toSignedMeasure (toJordanDecomposition 0)) (toSignedMeasure 0)
Tactic: apply toSignedMeasure_injective
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
⊢ (-s).toJordanDecomposition = -s.toJordanDecomposition
have a : (-s).toJordanDecomposition.toSignedMeasure = (-s.toJordanDecomposition).toSignedMeasure
Tactic: apply toSignedMeasure_injective
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition
have a : (r • s).toJordanDecomposition.toSignedMeasure = (r • s.toJordanDecomposition).toSignedMeasure
Tactic: apply toSignedMeasure_injective
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : 0 ≤ r
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition
have lift : ∀ (r : ℝ≥0), ((↑r : ℝ) • s).toJordanDecomposition = (↑r : ℝ) • s.toJordanDecomposition
Tactic: lift r to ℝ≥0 using hr
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ≥0
⊢ ((↑r : ℝ) • s).toJordanDecomposition = (↑r : ℝ) • s.toJordanDecomposition
have rw : ((↑r : ℝ) • s).toJordanDecomposition = (r • s).toJordanDecomposition
Tactic: rw [JordanDecomposition.coe_smul, ← toJordanDecomposition_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition
have pos : ∀ (hr : 0 ≤ r), (r • s).toJordanDecomposition = r • s.toJordanDecomposition
Tactic: by_cases! hr : 0 ≤ r
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
pos : ∀ (hr : 0 ≤ r), (r • s).toJordanDecomposition = r • s.toJordanDecomposition
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition
have neg : ∀ (hr : r < 0), (r • s).toJordanDecomposition = r • s.toJordanDecomposition
Tactic: by_cases! hr : 0 ≤ r
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition
have neg : (r • s).toJordanDecomposition.posPart = (r • s.toJordanDecomposition).posPart
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
neg : (r • s).toJordanDecomposition.posPart = (r • s.toJordanDecomposition).posPart
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition
have neg₁ : (r • s).toJordanDecomposition.negPart = (r • s.toJordanDecomposition).negPart
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
⊢ r • s = -(-r • s)
have rw : r • s = - -(r • s)
Tactic: rw [neg_smul, neg_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
rw : r • s = - -(r • s)
⊢ r • s = -(-r • s)
have rw₁ : r • s = r • s
Tactic: rw [neg_smul, neg_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
⊢ (r • s).toJordanDecomposition.posPart = (r • s.toJordanDecomposition).posPart
have neg : 0 ≤ -r
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : r < 0
⊢ (r • s).toJordanDecomposition.negPart = (r • s.toJordanDecomposition).negPart
have neg : 0 ≤ -r
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
j : JordanDecomposition α
h : s = j.toSignedMeasure
⊢ s.toJordanDecomposition = j
have rw : j.toSignedMeasure.toJordanDecomposition = j
Tactic: rw [h, toJordanDecomposition_toSignedMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
j : JordanDecomposition α
h : s = j.toSignedMeasure
rw : j.toSignedMeasure.toJordanDecomposition = j
⊢ s.toJordanDecomposition = j
have rw₁ : j = j
Tactic: rw [h, toJordanDecomposition_toSignedMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hs : Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (↑s : Set α → ℝ) i = 0
have 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∞)
Tactic: rw [totalVariation, Measure.coe_add, Pi.add_apply, add_eq_zero] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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∞)
⊢ (↑s : Set α → ℝ) i = 0
have rw : ((if MeasurableSet i then s.toJordanDecomposition.posPart.real i else 0) -
    if MeasurableSet i then s.toJordanDecomposition.negPart.real i else 0) =
  0
Tactic: rw [← toSignedMeasure_toJordanDecomposition s, toSignedMeasure, VectorMeasure.coe_sub,
    Pi.sub_apply, Measure.toSignedMeasure_apply, Measure.toSignedMeasure_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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∞)
⊢ ((if MeasurableSet i then s.toJordanDecomposition.posPart.real i else 0) -
      if MeasurableSet i then s.toJordanDecomposition.negPart.real i else 0) =
    0
have 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
Tactic: by_cases hi : MeasurableSet i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ ((if MeasurableSet i then s.toJordanDecomposition.posPart.real i else 0) -
      if MeasurableSet i then s.toJordanDecomposition.negPart.real i else 0) =
    0
have 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
Tactic: by_cases hi : MeasurableSet i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
⊢ s ≪ᵥ μ ↔ s.totalVariation ≪ μ.ennrealToMeasure
have mp : s ≪ᵥ μ → s.totalVariation ≪ μ.ennrealToMeasure
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
mp : s ≪ᵥ μ → s.totalVariation ≪ μ.ennrealToMeasure
⊢ s ≪ᵥ μ ↔ s.totalVariation ≪ μ.ennrealToMeasure
have mpr : s.totalVariation ≪ μ.ennrealToMeasure → s ≪ᵥ μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
μ : VectorMeasure α ℝ≥0∞
h : s ≪ᵥ μ
⊢ s.totalVariation ≪ μ.ennrealToMeasure
have 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∞)
Tactic: refine Measure.AbsolutelyContinuous.mk fun S hS₁ hS₂ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
have 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ᶜ sorry hi₃),
  Eq (α := ℝ≥0∞) ((s.totalVariation : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: obtain ⟨i, hi₁, hi₂, hi₃, hpos, hneg⟩ := s.toJordanDecomposition_spec