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∞)
hT₆ : j₁.toSignedMeasure ≤[T] 0
hT₇ : 0 ≤[Tᶜ] j₁.toSignedMeasure
hT₈ : Eq (α := ℝ≥0∞) ((j₂.posPart : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((j₂.negPart : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← hj] at hT₂ hT₃
-- 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∞)
⊢ (↑j₁.toSignedMeasure : Set α → ℝ) (symmDiff Sᶜ Tᶜ) = 0

Tactic:
obtain ⟨hST₁, -⟩ :=
    of_symmDiff_compl_positive_negative hS₁.compl hT₁.compl ⟨hS₃, (compl_compl S).symm ▸ hS₂⟩
      ⟨hT₃, (compl_compl T).symm ▸ hT₂⟩

Premises used: compl_compl, Eq.rec, MeasurableSet.compl, And.intro, MeasureTheory.SignedMeasure.of_symmDiff_compl_positive_negative, Eq.symm
-- 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
⊢ j₁ = j₂

Tactic:
eq_of_posPart_eq_posPart ?_ hj

Premises used: _private.0.MeasureTheory.JordanDecomposition.eq_of_posPart_eq_posPart
-- 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
refine : j₁.posPart = j₂.posPart
⊢ j₁ = j₂

Tactic:
refine eq_of_posPart_eq_posPart ?_ hj

Premises used: _private.0.MeasureTheory.JordanDecomposition.eq_of_posPart_eq_posPart
-- 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
h :
  ∀ (i : Set α) (hi : MeasurableSet i),
    Eq (α := ℝ≥0∞) ((j₁.posPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((j₂.posPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
⊢ j₁.posPart = j₂.posPart

Tactic:
ext1 i hi
-- 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
rw : j₁.posPart.real i = j₁.posPart.real (i ∩ Sᶜ)
⊢ j₁.posPart.real i = (↑j₁.toSignedMeasure : Set α → ℝ) (i ∩ Sᶜ)

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

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure, sub_zero, MeasureTheory.JordanDecomposition.negPart, MeasurableSet.compl, ENNReal.toReal_zero, Iff.mp, MeasureTheory.measureReal_def, MeasureTheory.Measure.toSignedMeasure_sub_apply, nonpos_iff_eq_zero, MeasurableSet.inter
-- 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
rw : j₁.posPart.real (i ∩ S ∪ i ∩ Sᶜ)
| j₁.posPart.real i

Tactic:
rw [← Set.inter_union_compl i S]

Premises used: Set.inter_union_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
conv_lhs : j₁.posPart.real (i ∩ S ∪ i ∩ Sᶜ) = j₁.posPart.real (i ∩ Sᶜ)
⊢ j₁.posPart.real i = j₁.posPart.real (i ∩ Sᶜ)

Tactic:
conv_lhs => rw [← Set.inter_union_compl i S]

Premises used: Set.inter_union_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
hd : Disjoint (i ∩ S) (i ∩ Sᶜ)
h : MeasurableSet (i ∩ Sᶜ)
⊢ j₁.posPart.real (i ∩ S ∪ i ∩ Sᶜ) = j₁.posPart.real (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]

Premises used: zero_add, ENNReal.toReal_zero, MeasureTheory.measureReal_union, Iff.mp, MeasureTheory.measureReal_def, nonpos_iff_eq_zero
-- 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
⊢ Disjoint (i ∩ S) (i ∩ Sᶜ)

Tactic:
Set.disjoint_of_subset_left Set.inter_subset_right
          (Set.disjoint_of_subset_right Set.inter_subset_right disjoint_compl_right)

Premises used: Set.disjoint_of_subset_left, disjoint_compl_right, Set.disjoint_of_subset_right, Set.inter_subset_right
-- 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
⊢ Disjoint (i ∩ S) (i ∩ Sᶜ)

Tactic:
refine
        Set.disjoint_of_subset_left Set.inter_subset_right
          (Set.disjoint_of_subset_right Set.inter_subset_right disjoint_compl_right)

Premises used: Set.disjoint_of_subset_left, disjoint_compl_right, Set.disjoint_of_subset_right, Set.inter_subset_right
-- 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
⊢ MeasurableSet (i ∩ Sᶜ)

Tactic:
hi.inter hS₁.compl

Premises used: MeasurableSet.compl, MeasurableSet.inter
-- 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
⊢ MeasurableSet (i ∩ Sᶜ)

Tactic:
exact hi.inter hS₁.compl

Premises used: MeasurableSet.compl, MeasurableSet.inter
-- 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
⊢ 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
-- 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ᶜ)
rw : j₂.posPart.real i = j₂.posPart.real (i ∩ Tᶜ)
⊢ j₂.posPart.real i = (↑j₂.toSignedMeasure : Set α → ℝ) (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]

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure, sub_zero, MeasureTheory.JordanDecomposition.negPart, MeasurableSet.compl, ENNReal.toReal_zero, Iff.mp, MeasureTheory.measureReal_def, MeasureTheory.Measure.toSignedMeasure_sub_apply, nonpos_iff_eq_zero, MeasurableSet.inter
-- 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ᶜ)
rw : j₂.posPart.real (i ∩ T ∪ i ∩ Tᶜ)
| j₂.posPart.real i

Tactic:
rw [← Set.inter_union_compl i T]

Premises used: Set.inter_union_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ᶜ)
conv_lhs : j₂.posPart.real (i ∩ T ∪ i ∩ Tᶜ) = j₂.posPart.real (i ∩ Tᶜ)
⊢ j₂.posPart.real i = j₂.posPart.real (i ∩ Tᶜ)

Tactic:
conv_lhs => rw [← Set.inter_union_compl i T]

Premises used: Set.inter_union_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ᶜ)
hd : Disjoint (i ∩ T) (i ∩ Tᶜ)
h : MeasurableSet (i ∩ Tᶜ)
⊢ j₂.posPart.real (i ∩ T ∪ i ∩ Tᶜ) = j₂.posPart.real (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]

Premises used: zero_add, ENNReal.toReal_zero, MeasureTheory.measureReal_union, Iff.mp, MeasureTheory.measureReal_def, nonpos_iff_eq_zero
-- 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ᶜ)
⊢ Disjoint (i ∩ T) (i ∩ Tᶜ)

Tactic:
Set.disjoint_of_subset_left Set.inter_subset_right
          (Set.disjoint_of_subset_right Set.inter_subset_right disjoint_compl_right)

Premises used: Set.disjoint_of_subset_left, disjoint_compl_right, Set.disjoint_of_subset_right, Set.inter_subset_right
-- 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ᶜ)
⊢ Disjoint (i ∩ T) (i ∩ Tᶜ)

Tactic:
exact
        Set.disjoint_of_subset_left Set.inter_subset_right
          (Set.disjoint_of_subset_right Set.inter_subset_right disjoint_compl_right)

Premises used: Set.disjoint_of_subset_left, disjoint_compl_right, Set.disjoint_of_subset_right, Set.inter_subset_right
-- 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ᶜ)
⊢ MeasurableSet (i ∩ Tᶜ)

Tactic:
hi.inter hT₁.compl

Premises used: MeasurableSet.compl, MeasurableSet.inter
-- 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ᶜ)
⊢ MeasurableSet (i ∩ Tᶜ)

Tactic:
exact hi.inter hT₁.compl

Premises used: MeasurableSet.compl, MeasurableSet.inter