awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0
have right : (↑s : Set α → ℝ) (v \ u) = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0
have 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
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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0
have 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
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
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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)
⊢ (↑s : Set α → ℝ) (u \ v) = 0
have linarith : (↑s : Set α → ℝ) (u \ v) < 0 → 0 - (↑s : Set α → ℝ) (u \ v) + ((↑s : Set α → ℝ) (u \ v) - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (↑s : Set α → ℝ) (u \ v) = 0
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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)
⊢ (↑s : Set α → ℝ) (v \ u) = 0
have linarith : (↑s : Set α → ℝ) (v \ u) < 0 → 0 - (↑s : Set α → ℝ) (v \ u) + ((↑s : Set α → ℝ) (v \ u) - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (↑s : Set α → ℝ) (v \ u) = 0
have 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
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
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
⊢ (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0
have hsu₁ : 0 ≤[u] -s
Tactic: rw [← s.neg_le_neg_iff _ hu, neg_zero] at hsu
Cleared hypotheses: hsu, hsv, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
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
⊢ (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0
have hsv₁ : 0 ≤[v] -s
Tactic: rw [← s.neg_le_neg_iff _ hv, neg_zero] at hsv
Cleared hypotheses: hsv, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
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
⊢ (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0
have this : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
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
have this₁ : ∀ (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
have subset_positive_null_set : (w ∩ u) ∆ (w ∩ v) ⊆ u ∆ v
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 ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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) ∆ (w ∩ v) ⊆ u ∆ v
have rw : w ∩ u ∆ v ⊆ u ∆ v
Tactic: rw [← Set.inter_symmDiff_distrib_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
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) = (↑s : Set α → ℝ) (w ∩ v)
have hwuv : (↑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
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
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) = (↑s : Set α → ℝ) (w ∩ v)
have huv : (↑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
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
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 ∩ u) = (↑s : Set α → ℝ) (w ∩ v)
have hvu : (↑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
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (↑s : Set α → ℝ) (w ∩ u) = (↑s : Set α → ℝ) (w ∩ v)
have rw : (↑s : Set α → ℝ) ((w ∩ u) \ (w ∩ v)) + (↑s : Set α → ℝ) (w ∩ v) = (↑s : Set α → ℝ) (w ∩ v)
Tactic: rw [← of_diff_of_diff_eq_zero (hw.inter hu) (hw.inter hv) hvu, huv, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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)
⊢ (↑s : Set α → ℝ) (w ∩ u) = (↑s : Set α → ℝ) (w ∩ v)
have rw₁ : 0 + (↑s : Set α → ℝ) (w ∩ v) = (↑s : Set α → ℝ) (w ∩ v)
Tactic: rw [← of_diff_of_diff_eq_zero (hw.inter hu) (hw.inter hv) hvu, huv, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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)
⊢ (↑s : Set α → ℝ) (w ∩ u) = (↑s : Set α → ℝ) (w ∩ v)
have rw₂ : (↑s : Set α → ℝ) (w ∩ v) = (↑s : Set α → ℝ) (w ∩ v)
Tactic: rw [← of_diff_of_diff_eq_zero (hw.inter hu) (hw.inter hv) hvu, huv, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
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
⊢ (↑s : Set α → ℝ) (w ∩ u) = (↑s : Set α → ℝ) (w ∩ v)
have hsu₁ : 0 ≤[u] -s
Tactic: rw [← s.neg_le_neg_iff _ hu, neg_zero] at hsu
Cleared hypotheses: hsu, hsv, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
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
⊢ (↑s : Set α → ℝ) (w ∩ u) = (↑s : Set α → ℝ) (w ∩ v)
have hsv₁ : 0 ≤[v] -s
Tactic: rw [← s.neg_le_neg_iff _ hv, neg_zero] at hsv
Cleared hypotheses: hsv, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
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) = (↑s : Set α → ℝ) (w ∩ v)
have this : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
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)
have this₁ : ∀ (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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
posPart : j₁.posPart = j₂.posPart
⊢ j₁ = j₂
have negPart : j₁.negPart = j₂.negPart
Tactic: ext1
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
j₁ j₂ : JordanDecomposition α
hj : j₁.posPart = j₂.posPart
hj' : j₁.toSignedMeasure = j₂.toSignedMeasure
⊢ j₁.negPart = j₂.negPart
have negPart : j₁.negPart.toSignedMeasure = j₂.negPart.toSignedMeasure
Tactic: rw [← toSignedMeasure_eq_toSignedMeasure_iff]
-- 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
⊢ j₁ = j₂
have 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₂
Tactic: obtain ⟨S, hS₁, hS₂, hS₃, hS₄, hS₅⟩ := j₁.exists_compl_positive_negative
-- 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∞)
⊢ j₁ = j₂
have 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₂
Tactic: obtain ⟨T, hT₁, hT₂, hT₃, hT₄, hT₅⟩ := j₂.exists_compl_positive_negative
-- 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∞)
⊢ j₁ = j₂
have hT₆ : j₁.toSignedMeasure ≤[T] 0
Tactic: rw [← hj] at hT₂ hT₃
Cleared hypotheses: hT₂, hT₃, hT₄, hT₅
-- 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∞)
hT₆ : j₁.toSignedMeasure ≤[T] 0
⊢ j₁ = j₂
have hT₇ : 0 ≤[Tᶜ] j₁.toSignedMeasure
Tactic: rw [← hj] at hT₂ hT₃
Cleared hypotheses: hT₂, hT₃, hT₄, hT₅
-- 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∞)
⊢ j₁ = j₂
have hST₁ : (↑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₂⟩
-- 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
⊢ j₁ = j₂
have refine : j₁.posPart = j₂.posPart
Tactic: refine eq_of_posPart_eq_posPart ?_ hj
-- 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
⊢ j₁.posPart = j₂.posPart
have h : ∀ (i : Set α) (hi : MeasurableSet i),
  Eq (α := ℝ≥0∞) ((j₁.posPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((j₂.posPart : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
Tactic: ext1 i hi
-- 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₁.toSignedMeasure : Set α → ℝ) (i ∩ Sᶜ)
have rw : j₁.posPart.real i = j₁.posPart.real (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]
-- 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
have rw : j₁.posPart.real (i ∩ S ∪ i ∩ Sᶜ)
Tactic: rw [← Set.inter_union_compl i S]