awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ S
⊢ (↑j.toSignedMeasure : Set α → ℝ) A ≤ (↑0 : Set α → ℝ) A
have refine_1 : 0 ≤ j.negPart.real A
Tactic: rw [toSignedMeasure, toSignedMeasure_sub_apply hA, measureReal_def,
      show j.posPart A = 0 from nonpos_iff_eq_zero.1 (hS₂ ▸ measure_mono hA₁), ENNReal.toReal_zero,
      zero_sub, neg_le, zero_apply, neg_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ 0 ≤[Sᶜ] j.toSignedMeasure
have refine_2 : ∀ (A : Set α) (hA : MeasurableSet A) (hA₁ : A ⊆ Sᶜ), (↑0 : Set α → ℝ) A ≤ (↑j.toSignedMeasure : Set α → ℝ) A
Tactic: refine restrict_le_restrict_of_subset_le _ _ fun A hA hA₁ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((j.posPart : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((j.negPart : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ Sᶜ
⊢ (↑0 : Set α → ℝ) A ≤ (↑j.toSignedMeasure : Set α → ℝ) A
have refine_2 : (↑0 : Set α → ℝ) A ≤ j.posPart.real A
Tactic: rw [toSignedMeasure, toSignedMeasure_sub_apply hA, measureReal_def (μ := j.negPart),
      show j.negPart A = 0 from nonpos_iff_eq_zero.1 (hS₃ ▸ measure_mono hA₁), ENNReal.toReal_zero,
      sub_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ s.toMeasureOfZeroLE i ⋯ ⋯ ⟂ₘ s.toMeasureOfLEZero iᶜ ⋯ ⋯
have refine_1 : Eq (α := ℝ≥0∞) ((s.toMeasureOfZeroLE i sorry sorry : (a : Set α) → ℝ≥0∞) iᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨iᶜ, hi.1.compl, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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_1 : Eq (α := ℝ≥0∞) ((s.toMeasureOfZeroLE i ⋯ ⋯ : (a : Set α) → ℝ≥0∞) iᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s.toMeasureOfZeroLE i ⋯ ⋯ ⟂ₘ s.toMeasureOfLEZero iᶜ ⋯ ⋯
have refine_2 : Eq (α := ℝ≥0∞) ((s.toMeasureOfLEZero iᶜ sorry sorry : (a : Set α) → ℝ≥0∞) iᶜᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨iᶜ, hi.1.compl, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ Eq (α := ℝ≥0∞) ((s.toMeasureOfZeroLE i ⋯ ⋯ : (a : Set α) → ℝ≥0∞) iᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_1 : (↑(NNReal.mk
        ((↑s : Set α → ℝ)
          (sorry.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0) ∩
            (sorry.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0))ᶜ))
        sorry) :
    ℝ≥0∞) =
  0
Tactic: rw [toMeasureOfZeroLE_apply _ _ hi.1 hi.1.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ Eq (α := ℝ≥0∞) ((s.toMeasureOfLEZero iᶜ ⋯ ⋯ : (a : Set α) → ℝ≥0∞) iᶜᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_2 : (↑(NNReal.mk
        (-(↑s : Set α → ℝ)
            ((sorry.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0))ᶜ ∩
              (sorry.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 0))ᶜᶜ))
        sorry) :
    ℝ≥0∞) =
  0
Tactic: rw [toMeasureOfLEZero_apply _ _ hi.1.compl hi.1.compl.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
i : Set α := ⋯.choose (p := fun (i : Set α) ↦ MeasurableSet i ∧ 0 ≤[i] s ∧ s ≤[iᶜ] 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₃
have hi₁ : MeasurableSet (sorry.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
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
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))
⊢ ∃ (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₃
have hi₂ : 0 ≤[sorry.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
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (hypothesis)
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
⊢ ∃ (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₃
have hi₃ : s ≤[(sorry.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
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : SignedMeasure α
⊢ s.toJordanDecomposition.toSignedMeasure = s
have 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ᶜ sorry hi₃), s.toJordanDecomposition.toSignedMeasure = s
Tactic: obtain ⟨i, hi₁, hi₂, hi₃, hμ, hν⟩ := s.toJordanDecomposition_spec
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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₃
⊢ s.toJordanDecomposition.toSignedMeasure = s
have simp : (s.toMeasureOfZeroLE i hi₁ hi₂).toSignedMeasure - (s.toMeasureOfLEZero iᶜ sorry hi₃).toSignedMeasure = s
Tactic: simp only [JordanDecomposition.toSignedMeasure, hμ, hν]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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₃
⊢ (s.toMeasureOfZeroLE i hi₁ hi₂).toSignedMeasure - (s.toMeasureOfLEZero iᶜ ⋯ hi₃).toSignedMeasure = s
have h : ∀ (k : Set α) (hk : MeasurableSet k),
  (↑((s.toMeasureOfZeroLE i hi₁ hi₂).toSignedMeasure - (s.toMeasureOfLEZero iᶜ sorry hi₃).toSignedMeasure) : Set α → ℝ) k =
    (↑s : Set α → ℝ) k
Tactic: ext k hk
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (↑((s.toMeasureOfZeroLE i hi₁ hi₂).toSignedMeasure - (s.toMeasureOfLEZero iᶜ ⋯ hi₃).toSignedMeasure) : Set α → ℝ) k =
    (↑s : Set α → ℝ) k
have h : (↑s : Set α → ℝ) (i ∩ k) - -(↑s : Set α → ℝ) (iᶜ ∩ k) = (↑s : Set α → ℝ) k
Tactic: rw [toSignedMeasure_sub_apply hk, toMeasureOfZeroLE_real_apply _ hi₂ hi₁ hk,
    toMeasureOfLEZero_real_apply _ hi₃ hi₁.compl hk]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (↑s : Set α → ℝ) (i ∩ k) - -(↑s : Set α → ℝ) (iᶜ ∩ k) = (↑s : Set α → ℝ) k
have h : (↑s : Set α → ℝ) (i ∩ k) + (↑s : Set α → ℝ) (iᶜ ∩ k) = (↑s : Set α → ℝ) k
Tactic: simp only [sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan (goal)
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
⊢ (↑s : Set α → ℝ) (i ∩ k) + (↑s : Set α → ℝ) (iᶜ ∩ k) = (↑s : Set α → ℝ) k
have rw : Disjoint (i ∩ k) (iᶜ ∩ 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 _ _]
-- 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
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
⊢ (↑s : Set α → ℝ) v + (↑s : Set α → ℝ) (w \ v) = 0
have rw : (↑s : Set α → ℝ) v + (↑s : Set α → ℝ) (w \ v) = (↑s : Set α → ℝ) w
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]
-- 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
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
rw : (↑s : Set α → ℝ) v + (↑s : Set α → ℝ) (w \ v) = (↑s : Set α → ℝ) w
⊢ (↑s : Set α → ℝ) v + (↑s : Set α → ℝ) (w \ v) = 0
have rw₁ : (↑s : Set α → ℝ) (v ∪ w \ v) = (↑s : Set α → ℝ) w
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]
-- 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
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
⊢ (↑s : Set α → ℝ) v + (↑s : Set α → ℝ) (w \ v) = 0
have rw₂ : (↑s : Set α → ℝ) (v ∪ w) = (↑s : Set α → ℝ) w
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]
-- 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
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
⊢ (↑s : Set α → ℝ) v + (↑s : Set α → ℝ) (w \ v) = 0
have rw₃ : (↑s : Set α → ℝ) w = (↑s : Set α → ℝ) w
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]
-- 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
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
⊢ (↑s : Set α → ℝ) v = 0
have this : (↑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]
-- 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
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
this : (↑s : Set α → ℝ) v + (↑s : Set α → ℝ) (w \ v) = 0
⊢ (↑s : Set α → ℝ) v = 0
have h₁ : 0 ≤ (↑s : Set α → ℝ) v
Tactic: have h₁ := nonneg_of_zero_le_restrict _ (restrict_le_restrict_subset _ _ hu hsu (hwt.trans hw₂))
-- 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
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
⊢ (↑s : Set α → ℝ) v = 0
have h₂ : 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₂))
-- 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
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)
⊢ (↑s : Set α → ℝ) v = 0
have linarith : (↑s : Set α → ℝ) v < 0 → 0 - (↑s : Set α → ℝ) v + ((↑s : Set α → ℝ) 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 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
⊢ (↑s : Set α → ℝ) v = 0
have linarith₁ : 0 < (↑s : Set α → ℝ) v →
  (↑s : Set α → ℝ) v + (↑s : Set α → ℝ) (w \ v) - 0 + (0 - (↑s : Set α → ℝ) (w \ v)) + (0 - (↑s : Set α → ℝ) v) = 0
Tactic: linarith
-- 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
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
⊢ (↑s : Set α → ℝ) v = 0
have hsu₁ : 0 ≤[u] -s
Tactic: rw [← s.neg_le_neg_iff _ hu, neg_zero] at hsu
Cleared hypotheses: hsu, hw₁, hw₂, hwt
-- 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
hw₁ : (↑s : Set α → ℝ) w = 0
hw₂ : w ⊆ u
hwt : v ⊆ w
⊢ (↑s : Set α → ℝ) v = 0
have this : ∀ (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
-- 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
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
have this₁ : ∀ (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
Cleared hypotheses: this
-- 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 : 0 ≤[u] s
hsv : 0 ≤[v] s
hs : (↑s : Set α → ℝ) (u ∆ v) = 0
⊢ (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0
have 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
Tactic: rw [restrict_le_restrict_iff] at hsu hsv
Cleared hypotheses: hsu, hsv, 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 : 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
⊢ (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0
have 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
Tactic: rw [restrict_le_restrict_iff] at hsu hsv
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 : ∀ ⦃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 a : (↑0 : Set α → ℝ) (u \ v) ≤ (↑s : Set α → ℝ) (u \ v)
Tactic: have a := hsu (hu.diff hv) diff_subset
-- 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 : ∀ ⦃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)
⊢ (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0
have b : (↑0 : Set α → ℝ) (v \ u) ≤ (↑s : Set α → ℝ) (v \ u)
Tactic: have b := hsv (hv.diff hu) diff_subset
-- 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 : ∀ ⦃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) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0
have hs₁ : (↑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
Cleared hypotheses: hs, a, b
-- 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 : ∀ ⦃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)
⊢ (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0
have a₁ : 0 ≤ (↑s : Set α → ℝ) (u \ v)
Tactic: rw [zero_apply] at a b
Cleared hypotheses: a, b
-- 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 : ∀ ⦃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)
⊢ (↑s : Set α → ℝ) (u \ v) = 0 ∧ (↑s : Set α → ℝ) (v \ u) = 0
have b₁ : 0 ≤ (↑s : Set α → ℝ) (v \ u)
Tactic: rw [zero_apply] at a b
Cleared hypotheses: a, b
-- 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 ∧ (↑s : Set α → ℝ) (v \ u) = 0
have left : (↑s : Set α → ℝ) (u \ v) = 0
Tactic: constructor