awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
left :
  ∀ (hs : (↑s : Set α → ℝ) (u \ v) + (↑s : Set α → ℝ) (v \ u) = 0) (a : 0 ≤ (↑s : Set α → ℝ) (u \ v))
    (b : 0 ≤ (↑s : Set α → ℝ) (v \ u)), (↑s : Set α → ℝ) (u \ v) = 0
right :
  ∀ (hs : (↑s : Set α → ℝ) (u \ v) + (↑s : Set α → ℝ) (v \ u) = 0) (a : 0 ≤ (↑s : Set α → ℝ) (u \ v))
    (b : 0 ≤ (↑s : Set α → ℝ) (v \ u)), (↑s : Set α → ℝ) (v \ u) = 0
⊢ (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0

Tactic:
on_goal 1 =>
    have a := hsu (hu.diff hv) diff_subset
    have b := hsv (hv.diff hu) diff_subset
    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
    rw [zero_apply] at a b
    constructor

Premises used: MeasurableSet.diff, disjoint_sdiff_self_right, Set.diff_subset, Set.symmDiff_def, MeasureTheory.VectorMeasure.zero_apply, 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 ≤ (↑s : Set α → ℝ) (u \ v)
b : 0 ≤ (↑s : Set α → ℝ) (v \ u)
linarith : (↑s : Set α → ℝ) (u \ v) < 0 → 0 - (↑s : Set α → ℝ) (u \ v) + ((↑s : Set α → ℝ) (u \ v) - 0) = 0
linarith₁ :
  0 < (↑s : Set α → ℝ) (u \ v) →
    (↑s : Set α → ℝ) (u \ v) + (↑s : Set α → ℝ) (v \ u) - 0 + (0 - (↑s : Set α → ℝ) (v \ u)) +
        (0 - (↑s : Set α → ℝ) (u \ v)) =
      0
⊢ (↑s : Set α → ℝ) (u \ v) = 0

Tactic:
linarith
-- 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)
linarith : (↑s : Set α → ℝ) (v \ u) < 0 → 0 - (↑s : Set α → ℝ) (v \ u) + ((↑s : Set α → ℝ) (v \ u) - 0) = 0
linarith₁ :
  0 < (↑s : Set α → ℝ) (v \ u) →
    (↑s : Set α → ℝ) (u \ v) + (↑s : Set α → ℝ) (v \ u) - 0 + (0 - (↑s : Set α → ℝ) (u \ v)) +
        (0 - (↑s : Set α → ℝ) (v \ u)) =
      0
⊢ (↑s : Set α → ℝ) (v \ u) = 0

Tactic:
linarith
-- 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 : 0 ≤[v] s
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
⊢ MeasurableSet v

Tactic:
assumption
-- 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
⊢ MeasurableSet u

Tactic:
assumption
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : s ≤[u] 0
hsv : s ≤[v] 0
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
⊢ 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 : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : s ≤[u] 0
hsv : s ≤[v] 0
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
hsu₁ : 0 ≤[u] -s
⊢ s ≤[v] 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 : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : s ≤[u] 0
hsv : s ≤[v] 0
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
hsu₁ : 0 ≤[u] -s
hsv₁ : s ≤[v] 0
⊢ (↑s : Set α → ℝ) (u ∆ v) = 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 : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] -s
hsv : s ≤[v] 0
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
⊢ 0 ≤[v] -s

Tactic:
rw [← s.neg_le_neg_iff _ hv, neg_zero] at hsv

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 : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] -s
hsv : s ≤[v] 0
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
hsv₁ : 0 ≤[v] -s
⊢ (↑s : Set α → ℝ) (u ∆ v) = 0

Tactic:
rw [← s.neg_le_neg_iff _ hv, neg_zero] at hsv

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 : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
⊢ ∀ (hs : (↑(-s) : Set α → ℝ) (u ∆ v) = 0), (↑(-s) : Set α → ℝ) (u \ v) = 0 ∧ (↑(-s) : Set α → ℝ) (v \ u) = 0

Tactic:
have := of_diff_eq_zero_of_symmDiff_eq_zero_positive hu hv hsu hsv
-- 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
this : ∀ (hs : (↑(-s) : Set α → ℝ) (u ∆ v) = 0), (↑(-s) : Set α → ℝ) (u \ v) = 0 ∧ (↑(-s) : Set α → ℝ) (v \ u) = 0
⊢ ∀ (hs : (↑s : Set α → ℝ) (u ∆ v) = 0), (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 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 : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
this : ∀ (hs : (↑s : Set α → ℝ) (u ∆ v) = 0), (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0
⊢ (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0

Tactic:
this hs
-- 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
this : ∀ (hs : (↑s : Set α → ℝ) (u ∆ v) = 0), (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0
⊢ (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0

Tactic:
exact this hs
-- 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
hsv : 0 ≤[v] s
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
⊢ (↑s : Set α → ℝ) ((w ∩ u) ∆ (w ∩ v)) = 0

Tactic:
subset_positive_null_set (hu.union hv) ((hw.inter hu).symmDiff (hw.inter hv))
        (hu.symmDiff hv) (restrict_le_restrict_union _ _ hu hsu hv hsv) hs
        Set.symmDiff_subset_union ?_

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_union, Set.symmDiff_subset_union, MeasurableSet.symmDiff, MeasurableSet.union, MeasureTheory.SignedMeasure.subset_positive_null_set, MeasurableSet.inter
-- 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
hsv : 0 ≤[v] s
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
subset_positive_null_set : (w ∩ u) ∆ (w ∩ v) ⊆ u ∆ v
⊢ (↑s : Set α → ℝ) ((w ∩ u) ∆ (w ∩ v)) = 0

Tactic:
refine
      subset_positive_null_set (hu.union hv) ((hw.inter hu).symmDiff (hw.inter hv))
        (hu.symmDiff hv) (restrict_le_restrict_union _ _ hu hsu hv hsv) hs
        Set.symmDiff_subset_union ?_

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_union, Set.symmDiff_subset_union, MeasurableSet.symmDiff, MeasurableSet.union, MeasureTheory.SignedMeasure.subset_positive_null_set, MeasurableSet.inter
-- 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
hsv : 0 ≤[v] s
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
rw : w ∩ u ∆ v ⊆ u ∆ v
⊢ (w ∩ u) ∆ (w ∩ v) ⊆ u ∆ v

Tactic:
rw [← Set.inter_symmDiff_distrib_left]

Premises used: Set.inter_symmDiff_distrib_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
hsv : 0 ≤[v] s
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
⊢ w ∩ u ∆ v ⊆ u ∆ v

Tactic:
Set.inter_subset_right

Premises used: Set.inter_subset_right
-- 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
hsv : 0 ≤[v] s
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
⊢ w ∩ u ∆ v ⊆ u ∆ v

Tactic:
exact Set.inter_subset_right

Premises used: Set.inter_subset_right
-- 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
hsv : 0 ≤[v] s
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
⊢ (↑s : Set α → ℝ) ((w ∩ u) ∆ (w ∩ v)) = 0

Tactic:
have hwuv : s ((w ∩ u) ∆ (w ∩ v)) = 0 := by
    refine
      subset_positive_null_set (hu.union hv) ((hw.inter hu).symmDiff (hw.inter hv))
        (hu.symmDiff hv) (restrict_le_restrict_union _ _ hu hsu hv hsv) hs
        Set.symmDiff_subset_union ?_
    rw [← Set.inter_symmDiff_distrib_left]
    exact Set.inter_subset_right
-- 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
hsv : 0 ≤[v] s
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
hwuv : (↑s : Set α → ℝ) ((w ∩ u) ∆ (w ∩ v)) = 0
⊢ (↑s : Set α → ℝ) ((w ∩ u) \ (w ∩ v)) = 0

Tactic:
obtain ⟨huv, hvu⟩ :=
    of_diff_eq_zero_of_symmDiff_eq_zero_positive (hw.inter hu) (hw.inter hv)
      (restrict_le_restrict_subset _ _ hu hsu (w.inter_subset_right))
      (restrict_le_restrict_subset _ _ hv hsv (w.inter_subset_right)) hwuv

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_subset, MeasureTheory.SignedMeasure.of_diff_eq_zero_of_symmDiff_eq_zero_positive, Set.inter_subset_right, MeasurableSet.inter
-- 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
hsv : 0 ≤[v] s
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
hwuv : (↑s : Set α → ℝ) ((w ∩ u) ∆ (w ∩ v)) = 0
huv : (↑s : Set α → ℝ) ((w ∩ u) \ (w ∩ v)) = 0
⊢ (↑s : Set α → ℝ) ((w ∩ v) \ (w ∩ u)) = 0

Tactic:
obtain ⟨huv, hvu⟩ :=
    of_diff_eq_zero_of_symmDiff_eq_zero_positive (hw.inter hu) (hw.inter hv)
      (restrict_le_restrict_subset _ _ hu hsu (w.inter_subset_right))
      (restrict_le_restrict_subset _ _ hv hsv (w.inter_subset_right)) hwuv

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_subset, MeasureTheory.SignedMeasure.of_diff_eq_zero_of_symmDiff_eq_zero_positive, Set.inter_subset_right, MeasurableSet.inter
-- 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
hsv : 0 ≤[v] s
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
hwuv : (↑s : Set α → ℝ) ((w ∩ u) ∆ (w ∩ v)) = 0
huv : (↑s : Set α → ℝ) ((w ∩ u) \ (w ∩ v)) = 0
hvu : (↑s : Set α → ℝ) ((w ∩ v) \ (w ∩ u)) = 0
rw : (↑s : Set α → ℝ) ((w ∩ u) \ (w ∩ v)) + (↑s : Set α → ℝ) (w ∩ v) = (↑s : Set α → ℝ) (w ∩ v)
rw₁ : 0 + (↑s : Set α → ℝ) (w ∩ v) = (↑s : Set α → ℝ) (w ∩ v)
rw₂ rw₃ : (↑s : Set α → ℝ) (w ∩ v) = (↑s : Set α → ℝ) (w ∩ v)
⊢ (↑s : Set α → ℝ) (w ∩ u) = (↑s : Set α → ℝ) (w ∩ v)

Tactic:
rw [← of_diff_of_diff_eq_zero (hw.inter hu) (hw.inter hv) hvu, huv, zero_add]

Premises used: zero_add, MeasureTheory.VectorMeasure.of_diff_of_diff_eq_zero, MeasurableSet.inter
-- 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
hsv : s ≤[v] 0
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
⊢ 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
hsv : s ≤[v] 0
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
hsu₁ : 0 ≤[u] -s
⊢ s ≤[v] 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
hsv : s ≤[v] 0
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
hsu₁ : 0 ≤[u] -s
hsv₁ : s ≤[v] 0
⊢ (↑s : Set α → ℝ) (u ∆ v) = 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 : 0 ≤[u] -s
hsv : s ≤[v] 0
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
⊢ 0 ≤[v] -s

Tactic:
rw [← s.neg_le_neg_iff _ hv, neg_zero] at hsv

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
hsv : s ≤[v] 0
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
hsv₁ : 0 ≤[v] -s
⊢ (↑s : Set α → ℝ) (u ∆ v) = 0

Tactic:
rw [← s.neg_le_neg_iff _ hv, neg_zero] at hsv

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
hsv : 0 ≤[v] -s
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
⊢ ∀ (hs : (↑(-s) : Set α → ℝ) (u ∆ v) = 0), (↑(-s) : Set α → ℝ) (w ∩ u) = (↑(-s) : Set α → ℝ) (w ∩ v)

Tactic:
have := of_inter_eq_of_symmDiff_eq_zero_positive hu hv hw hsu hsv
-- 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
hsv : 0 ≤[v] -s
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
this : ∀ (hs : (↑(-s) : Set α → ℝ) (u ∆ v) = 0), (↑(-s) : Set α → ℝ) (w ∩ u) = (↑(-s) : Set α → ℝ) (w ∩ v)
⊢ ∀ (hs : (↑s : Set α → ℝ) (u ∆ v) = 0), (↑s : Set α → ℝ) (w ∩ u) = (↑s : Set α → ℝ) (w ∩ v)

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

Premises used: MeasureTheory.VectorMeasure.coe_neg, neg_eq_zero, neg_inj, 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
hsv : 0 ≤[v] -s
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
this : ∀ (hs : (↑s : Set α → ℝ) (u ∆ v) = 0), (↑s : Set α → ℝ) (w ∩ u) = (↑s : Set α → ℝ) (w ∩ v)
⊢ (↑s : Set α → ℝ) (w ∩ u) = (↑s : Set α → ℝ) (w ∩ v)

Tactic:
this hs
-- 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
hsv : 0 ≤[v] -s
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
this : ∀ (hs : (↑s : Set α → ℝ) (u ∆ v) = 0), (↑s : Set α → ℝ) (w ∩ u) = (↑s : Set α → ℝ) (w ∩ v)
⊢ (↑s : Set α → ℝ) (w ∩ u) = (↑s : Set α → ℝ) (w ∩ v)

Tactic:
exact this hs
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
posPart : j₁.posPart = j₂.posPart
negPart : j₁.negPart = j₂.negPart
⊢ j₁ = j₂

Tactic:
ext1
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁.posPart = j₂.posPart

Tactic:
hj
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁.posPart = j₂.posPart

Tactic:
exact hj
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
negPart : j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure
⊢ j₁.negPart = j₂.negPart

Tactic:
rw [← toSignedMeasure_eq_toSignedMeasure_iff]

Premises used: MeasureTheory.Measure.toSignedMeasure_eq_toSignedMeasure_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.posPart.toSignedMeasure - j₁.negPart.toSignedMeasure = j₂.posPart.toSignedMeasure - j₂.negPart.toSignedMeasure
⊢ j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure

Tactic:
simp_rw [hj, sub_right_inj] at hj'

Premises used: sub_right_inj
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure
⊢ j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure

Tactic:
hj'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure
⊢ j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure

Tactic:
exact hj'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
Goal:
α : Type u_1
inst : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.toSignedMeasure = j₂.toSignedMeasure
obtain :
  ∀ (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∞)), j₁ = j₂
⊢ j₁ = j₂

Tactic:
obtain ⟨S, hS₁, hS₂, hS₃, hS₄, hS₅⟩ := j₁.exists_compl_positive_negative

Premises used: MeasureTheory.JordanDecomposition.exists_compl_positive_negative
-- 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∞)
obtain :
  ∀ (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₁ = j₂
⊢ j₁ = j₂

Tactic:
obtain ⟨T, hT₁, hT₂, hT₃, hT₄, hT₅⟩ := j₂.exists_compl_positive_negative

Premises used: MeasureTheory.JordanDecomposition.exists_compl_positive_negative
-- 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 ≤[T] 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∞)
hT₆ : j₁.toSignedMeasure ≤[T] 0
⊢ 0 ≤[Tᶜ] j₁.toSignedMeasure

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

Tactic:
rw [← hj] at hT₂ hT₃