awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_2 :
  (↑(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.toMeasureOfLEZero iᶜ ⋯ ⋯ : (a : Set α) → ℝ≥0∞) iᶜᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

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

Premises used: MeasurableSet.compl, MeasureTheory.SignedMeasure.toMeasureOfLEZero_apply, 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
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α := ⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0)
⊢ MeasurableSet (⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0))

Tactic:
obtain ⟨hi₁, hi₂, hi₃⟩ := s.exists_compl_positive_negative.choose_spec

Premises used: Exists.choose_spec, MeasureTheory.SignedMeasure.exists_compl_positive_negative
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
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

Tactic:
obtain ⟨hi₁, hi₂, hi₃⟩ := s.exists_compl_positive_negative.choose_spec

Premises used: Exists.choose_spec, MeasureTheory.SignedMeasure.exists_compl_positive_negative
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
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))
hi₂ : 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

Tactic:
obtain ⟨hi₁, hi₂, hi₃⟩ := s.exists_compl_positive_negative.choose_spec

Premises used: Exists.choose_spec, MeasureTheory.SignedMeasure.exists_compl_positive_negative
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
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))
hi₂ : 0 ≤[⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0)] s
hi₃ : s ≤[(⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0))ᶜ] 0
⊢ ∃ (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0),
    s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ ∧
      s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃

Tactic:
⟨i, hi₁, hi₂, hi₃, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
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))
hi₂ : 0 ≤[⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0)] s
hi₃ : s ≤[(⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0))ᶜ] 0
⊢ ∃ (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0),
    s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ ∧
      s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃

Tactic:
exact ⟨i, hi₁, hi₂, hi₃, rfl, rfl⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
obtain :
  ∀ (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0)
    (hμ : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂)
    (hν : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃), s.toJordanDecomposition.toSignedMeasure = s
⊢ s.toJordanDecomposition.toSignedMeasure = s

Tactic:
obtain ⟨i, hi₁, hi₂, hi₃, hμ, hν⟩ := s.toJordanDecomposition_spec

Premises used: MeasureTheory.SignedMeasure.toJordanDecomposition_spec
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hμ : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hν : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
simp : (s.toMeasureOfZeroLE i hi₁ hi₂).toSignedMeasure - (s.toMeasureOfLEZero iᶜ ⋯ hi₃).toSignedMeasure = s
⊢ s.toJordanDecomposition.toSignedMeasure = s

Tactic:
simp only [JordanDecomposition.toSignedMeasure, hμ, hν]

Premises used: MeasureTheory.JordanDecomposition.toSignedMeasure
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hμ : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hν : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
h :
  ∀ (k : Set α) (hk : MeasurableSet k),
    (↑((s.toMeasureOfZeroLE i hi₁ hi₂).toSignedMeasure - (s.toMeasureOfLEZero iᶜ ⋯ hi₃).toSignedMeasure) : Set α → ℝ)
        k =
      (↑s : Set α → ℝ) k
⊢ (s.toMeasureOfZeroLE i hi₁ hi₂).toSignedMeasure - (s.toMeasureOfLEZero iᶜ ⋯ hi₃).toSignedMeasure = s

Tactic:
ext k hk
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hμ : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hν : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
k : Set α
hk : MeasurableSet k
h : (↑s : Set α → ℝ) (i ∩ k) - -(↑s : Set α → ℝ) (iᶜ ∩ k) = (↑s : Set α → ℝ) k
⊢ (↑((s.toMeasureOfZeroLE i hi₁ hi₂).toSignedMeasure - (s.toMeasureOfLEZero iᶜ ⋯ hi₃).toSignedMeasure) : Set α → ℝ) k =
    (↑s : Set α → ℝ) k

Tactic:
rw [toSignedMeasure_sub_apply hk, toMeasureOfZeroLE_real_apply _ hi₂ hi₁ hk,
    toMeasureOfLEZero_real_apply _ hi₃ hi₁.compl hk]

Premises used: MeasureTheory.SignedMeasure.toMeasureOfZeroLE_real_apply, MeasurableSet.compl, MeasureTheory.SignedMeasure.toMeasureOfLEZero_real_apply, MeasureTheory.Measure.toSignedMeasure_sub_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hμ : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hν : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
k : Set α
hk : MeasurableSet k
h : (↑s : Set α → ℝ) (i ∩ k) + (↑s : Set α → ℝ) (iᶜ ∩ k) = (↑s : Set α → ℝ) k
⊢ (↑s : Set α → ℝ) (i ∩ k) - -(↑s : Set α → ℝ) (iᶜ ∩ k) = (↑s : Set α → ℝ) k

Tactic:
simp only [sub_neg_eq_add]

Premises used: sub_neg_eq_add
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hμ : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hν : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
k : Set α
hk : MeasurableSet k
rw : Disjoint (i ∩ k) (iᶜ ∩ k)
⊢ (↑s : Set α → ℝ) (i ∩ k) + (↑s : Set α → ℝ) (iᶜ ∩ k) = (↑s : Set α → ℝ) k

Tactic:
rw [← of_union _ (MeasurableSet.inter hi₁ hk) (MeasurableSet.inter hi₁.compl hk),
    Set.inter_comm i, Set.inter_comm iᶜ, Set.inter_union_compl _ _]

Premises used: Compl.compl, MeasureTheory.VectorMeasure.of_union, MeasurableSet.compl, Set.inter_comm, Set.inter_union_compl, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hμ : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hν : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
k : Set α
hk : MeasurableSet k
⊢ Disjoint (i ∩ k) (iᶜ ∩ k)

Tactic:
(disjoint_compl_right.inf_left _).inf_right _

Premises used: disjoint_compl_right, Disjoint.inf_right, Disjoint.inf_left
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
hi₃ : s ≤[iᶜ] 0
hμ : s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂
hν : s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
k : Set α
hk : MeasurableSet k
⊢ Disjoint (i ∩ k) (iᶜ ∩ k)

Tactic:
exact (disjoint_compl_right.inf_left _).inf_right _

Premises used: disjoint_compl_right, Disjoint.inf_right, Disjoint.inf_left
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
rw : (↑s : Set α → ℝ) v + (↑s : Set α → ℝ) (w \ v) = (↑s : Set α → ℝ) w
rw₁ : (↑s : Set α → ℝ) (v ∪ w \ v) = (↑s : Set α → ℝ) w
rw₂ : (↑s : Set α → ℝ) (v ∪ w) = (↑s : Set α → ℝ) w
rw₃ rw₄ : (↑s : Set α → ℝ) w = (↑s : Set α → ℝ) w
⊢ (↑s : Set α → ℝ) v + (↑s : Set α → ℝ) (w \ v) = 0

Tactic:
rw [← hw₁, ← of_union Set.disjoint_sdiff_right hv (hw.diff hv), Set.union_diff_self,
      Set.union_eq_self_of_subset_left hwt]

Premises used: MeasurableSet.diff, MeasureTheory.VectorMeasure.of_union, Set.union_eq_self_of_subset_left, Set.disjoint_sdiff_right, Set.union_diff_self
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
⊢ (↑s : Set α → ℝ) v + (↑s : Set α → ℝ) (w \ v) = 0

Tactic:
have : s v + s (w \ v) = 0 := by
    rw [← hw₁, ← of_union Set.disjoint_sdiff_right hv (hw.diff hv), Set.union_diff_self,
      Set.union_eq_self_of_subset_left hwt]
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : (↑s : Set α → ℝ) v + (↑s : Set α → ℝ) (w \ v) = 0
⊢ 0 ≤ (↑s : Set α → ℝ) v

Tactic:
have h₁ := nonneg_of_zero_le_restrict _ (restrict_le_restrict_subset _ _ hu hsu (hwt.trans hw₂))
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : (↑s : Set α → ℝ) v + (↑s : Set α → ℝ) (w \ v) = 0
h₁ : 0 ≤ (↑s : Set α → ℝ) v
⊢ 0 ≤ (↑s : Set α → ℝ) (w \ v)

Tactic:
have h₂ : 0 ≤ s (w \ v) :=
    nonneg_of_zero_le_restrict _
      (restrict_le_restrict_subset _ _ hu hsu (diff_subset.trans hw₂))
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] s
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : (↑s : Set α → ℝ) v + (↑s : Set α → ℝ) (w \ v) = 0
h₁ : 0 ≤ (↑s : Set α → ℝ) v
h₂ : 0 ≤ (↑s : Set α → ℝ) (w \ v)
linarith : (↑s : Set α → ℝ) v < 0 → 0 - (↑s : Set α → ℝ) v + ((↑s : Set α → ℝ) v - 0) = 0
linarith₁ :
  0 < (↑s : Set α → ℝ) v →
    (↑s : Set α → ℝ) v + (↑s : Set α → ℝ) (w \ v) - 0 + (0 - (↑s : Set α → ℝ) (w \ v)) + (0 - (↑s : Set α → ℝ) v) = 0
⊢ (↑s : Set α → ℝ) v = 0

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : s ≤[u] 0
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
⊢ 0 ≤[u] -s

Tactic:
rw [← s.neg_le_neg_iff _ hu, neg_zero] at hsu

Premises used: MeasureTheory.VectorMeasure.neg_le_neg_iff, neg_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : s ≤[u] 0
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
hsu₁ : 0 ≤[u] -s
⊢ (↑s : Set α → ℝ) w = 0

Tactic:
rw [← s.neg_le_neg_iff _ hu, neg_zero] at hsu

Premises used: MeasureTheory.VectorMeasure.neg_le_neg_iff, neg_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : s ≤[u] 0
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
hsu₁ : 0 ≤[u] -s
hw₃ : (↑s : Set α → ℝ) w = 0
⊢ w ⊆ u

Tactic:
rw [← s.neg_le_neg_iff _ hu, neg_zero] at hsu

Premises used: MeasureTheory.VectorMeasure.neg_le_neg_iff, neg_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : s ≤[u] 0
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
hsu₁ : 0 ≤[u] -s
hw₃ : (↑s : Set α → ℝ) w = 0
hw₄ : w ⊆ u
⊢ v ⊆ w

Tactic:
rw [← s.neg_le_neg_iff _ hu, neg_zero] at hsu

Premises used: MeasureTheory.VectorMeasure.neg_le_neg_iff, neg_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
⊢ ∀ (hw₁ : (↑(-s) : Set α → ℝ) w = 0) (hw₂ : w ⊆ u) (hwt : v ⊆ w), (↑(-s) : Set α → ℝ) v = 0

Tactic:
have := subset_positive_null_set hu hv hw hsu
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : ∀ (hw₁ : (↑(-s) : Set α → ℝ) w = 0) (hw₂ : w ⊆ u) (hwt : v ⊆ w), (↑(-s) : Set α → ℝ) v = 0
⊢ ∀ (hw₁ : (↑s : Set α → ℝ) w = 0) (hw₂ : w ⊆ u) (hwt : v ⊆ w), (↑s : Set α → ℝ) v = 0

Tactic:
simp only [Pi.neg_apply, neg_eq_zero, coe_neg] at this

Premises used: MeasureTheory.VectorMeasure.coe_neg, neg_eq_zero, Pi.neg_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : ∀ (hw₁ : (↑s : Set α → ℝ) w = 0) (hw₂ : w ⊆ u) (hwt : v ⊆ w), (↑s : Set α → ℝ) v = 0
⊢ (↑s : Set α → ℝ) v = 0

Tactic:
this hw₁ hw₂ hwt
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v w : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hw : MeasurableSet w
hsu : 0 ≤[u] -s
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : ∀ (hw₁ : (↑s : Set α → ℝ) w = 0) (hw₂ : w ⊆ u) (hwt : v ⊆ w), (↑s : Set α → ℝ) v = 0
⊢ (↑s : Set α → ℝ) v = 0

Tactic:
exact this hw₁ hw₂ hwt
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] s
hsv : 0 ≤[v] s
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
rw :
  ∀ (hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j)
    (hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j)
    (hs : (↑s : Set α → ℝ) (u ∆ v) = 0), (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0
hi :
  ∀ (hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j) (hsv : 0 ≤[v] s)
    (hs : (↑s : Set α → ℝ) (u ∆ v) = 0), MeasurableSet v
hi₁ : MeasurableSet u
⊢ (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0

Tactic:
rw [restrict_le_restrict_iff] at hsu hsv

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
⊢ (↑0 : Set α → ℝ) (u \ v) ≤ (↑s : Set α → ℝ) (u \ v)

Tactic:
have a := hsu (hu.diff hv) diff_subset
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
a : (↑0 : Set α → ℝ) (u \ v) ≤ (↑s : Set α → ℝ) (u \ v)
⊢ (↑0 : Set α → ℝ) (v \ u) ≤ (↑s : Set α → ℝ) (v \ u)

Tactic:
have b := hsv (hv.diff hu) diff_subset
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
a : (↑0 : Set α → ℝ) (u \ v) ≤ (↑s : Set α → ℝ) (u \ v)
b : (↑0 : Set α → ℝ) (v \ u) ≤ (↑s : Set α → ℝ) (v \ u)
⊢ (↑s : Set α → ℝ) (u \ v) + (↑s : Set α → ℝ) (v \ u) = 0

Tactic:
rw [Set.symmDiff_def,
      of_union (v := s) (Set.disjoint_of_subset_left diff_subset disjoint_sdiff_self_right)
        (hu.diff hv) (hv.diff hu)] at hs

Premises used: MeasurableSet.diff, disjoint_sdiff_self_right, Set.diff_subset, Set.symmDiff_def, Set.disjoint_of_subset_left, MeasureTheory.VectorMeasure.of_union
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
a : (↑0 : Set α → ℝ) (u \ v) ≤ (↑s : Set α → ℝ) (u \ v)
b : (↑0 : Set α → ℝ) (v \ u) ≤ (↑s : Set α → ℝ) (v \ u)
hs₁ : (↑s : Set α → ℝ) (u \ v) + (↑s : Set α → ℝ) (v \ u) = 0
⊢ (↑0 : Set α → ℝ) (u \ v) ≤ (↑s : Set α → ℝ) (u \ v)

Tactic:
rw [Set.symmDiff_def,
      of_union (v := s) (Set.disjoint_of_subset_left diff_subset disjoint_sdiff_self_right)
        (hu.diff hv) (hv.diff hu)] at hs

Premises used: MeasurableSet.diff, disjoint_sdiff_self_right, Set.diff_subset, Set.symmDiff_def, Set.disjoint_of_subset_left, MeasureTheory.VectorMeasure.of_union
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
a : (↑0 : Set α → ℝ) (u \ v) ≤ (↑s : Set α → ℝ) (u \ v)
b : (↑0 : Set α → ℝ) (v \ u) ≤ (↑s : Set α → ℝ) (v \ u)
hs₁ : (↑s : Set α → ℝ) (u \ v) + (↑s : Set α → ℝ) (v \ u) = 0
a₁ : (↑0 : Set α → ℝ) (u \ v) ≤ (↑s : Set α → ℝ) (u \ v)
⊢ (↑0 : Set α → ℝ) (v \ u) ≤ (↑s : Set α → ℝ) (v \ u)

Tactic:
rw [Set.symmDiff_def,
      of_union (v := s) (Set.disjoint_of_subset_left diff_subset disjoint_sdiff_self_right)
        (hu.diff hv) (hv.diff hu)] at hs

Premises used: MeasurableSet.diff, disjoint_sdiff_self_right, Set.diff_subset, Set.symmDiff_def, Set.disjoint_of_subset_left, MeasureTheory.VectorMeasure.of_union
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j
hs : (↑s : Set α → ℝ) (u \ v) + (↑s : Set α → ℝ) (v \ u) = 0
a : (↑0 : Set α → ℝ) (u \ v) ≤ (↑s : Set α → ℝ) (u \ v)
b : (↑0 : Set α → ℝ) (v \ u) ≤ (↑s : Set α → ℝ) (v \ u)
⊢ 0 ≤ (↑s : Set α → ℝ) (u \ v)

Tactic:
rw [zero_apply] at a b

Premises used: MeasureTheory.VectorMeasure.zero_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j
hs : (↑s : Set α → ℝ) (u \ v) + (↑s : Set α → ℝ) (v \ u) = 0
a : (↑0 : Set α → ℝ) (u \ v) ≤ (↑s : Set α → ℝ) (u \ v)
b : (↑0 : Set α → ℝ) (v \ u) ≤ (↑s : Set α → ℝ) (v \ u)
a₁ : 0 ≤ (↑s : Set α → ℝ) (u \ v)
⊢ 0 ≤ (↑s : Set α → ℝ) (v \ u)

Tactic:
rw [zero_apply] at a b

Premises used: MeasureTheory.VectorMeasure.zero_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ u → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j
hsv : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ v → (↑0 : Set α → ℝ) j ≤ (↑s : Set α → ℝ) j
hs : (↑s : Set α → ℝ) (u \ v) + (↑s : Set α → ℝ) (v \ u) = 0
a : 0 ≤ (↑s : Set α → ℝ) (u \ v)
b : 0 ≤ (↑s : Set α → ℝ) (v \ u)
left : (↑s : Set α → ℝ) (u \ v) = 0
right : (↑s : Set α → ℝ) (v \ u) = 0
⊢ (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0

Tactic:
constructor