case intro.intro.intro
α : Type u_1
β : Type ?u.26725
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑j.posPart S = 0
hS₃ : ↑↑j.negPart (Sᶜ) = 0
⊢ ∃ S,
    MeasurableSet S ∧
      VectorMeasure.restrict (toSignedMeasure j) S ≤ VectorMeasure.restrict 0 S ∧
        VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j) (Sᶜ) ∧
          ↑↑j.posPart S = 0 ∧ ↑↑j.negPart (Sᶜ) = 0
α : Type u_1
β : Type ?u.26725
inst✝ : MeasurableSpace α
j : JordanDecomposition α
⊢ ∃ S,
    MeasurableSet S ∧
      VectorMeasure.restrict (toSignedMeasure j) S ≤ VectorMeasure.restrict 0 S ∧
        VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j) (Sᶜ) ∧
          ↑↑j.posPart S = 0 ∧ ↑↑j.negPart (Sᶜ) = 0
obtain ⟨S, hS₁, hS₂, hS₃⟩ := j.mutuallySingular
case intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.26725
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑j.posPart S = 0
hS₃ : ↑↑j.negPart (Sᶜ) = 0
⊢ VectorMeasure.restrict (toSignedMeasure j) S ≤ VectorMeasure.restrict 0 S

case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.26725
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑j.posPart S = 0
hS₃ : ↑↑j.negPart (Sᶜ) = 0
⊢ VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j) (Sᶜ)
case intro.intro.intro
α : Type u_1
β : Type ?u.26725
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑j.posPart S = 0
hS₃ : ↑↑j.negPart (Sᶜ) = 0
⊢ ∃ S,
    MeasurableSet S ∧
      VectorMeasure.restrict (toSignedMeasure j) S ≤ VectorMeasure.restrict 0 S ∧
        VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j) (Sᶜ) ∧
          ↑↑j.posPart S = 0 ∧ ↑↑j.negPart (Sᶜ) = 0
refine' ⟨S, hS₁, _, _, hS₂, hS₃⟩
case intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.26725
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑j.posPart S = 0
hS₃ : ↑↑j.negPart (Sᶜ) = 0
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ S
⊢ ↑(toSignedMeasure j) A ≤ ↑0 A
case intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.26725
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑j.posPart S = 0
hS₃ : ↑↑j.negPart (Sᶜ) = 0
⊢ VectorMeasure.restrict (toSignedMeasure j) S ≤ VectorMeasure.restrict 0 S
refine' restrict_le_restrict_of_subset_le _ _ fun A hA hA₁ => _
case intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.26725
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑j.posPart S = 0
hS₃ : ↑↑j.negPart (Sᶜ) = 0
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ S
⊢ 0 ≤ ENNReal.toReal (↑↑j.negPart A)
case intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.26725
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑j.posPart S = 0
hS₃ : ↑↑j.negPart (Sᶜ) = 0
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ S
⊢ ↑(toSignedMeasure j) A ≤ ↑0 A
rw [toSignedMeasure, toSignedMeasure_sub_apply hA,
  show j.posPart A = 0 from nonpos_iff_eq_zero.1 (hS₂ ▸ measure_mono hA₁), ENNReal.zero_toReal,
  zero_sub, neg_le, zero_apply, neg_zero]
no goals
case intro.intro.intro.refine'_1
α : Type u_1
β : Type ?u.26725
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑j.posPart S = 0
hS₃ : ↑↑j.negPart (Sᶜ) = 0
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ S
⊢ 0 ≤ ENNReal.toReal (↑↑j.negPart A)
exact ENNReal.toReal_nonneg
case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.26725
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑j.posPart S = 0
hS₃ : ↑↑j.negPart (Sᶜ) = 0
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ Sᶜ
⊢ ↑0 A ≤ ↑(toSignedMeasure j) A
case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.26725
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑j.posPart S = 0
hS₃ : ↑↑j.negPart (Sᶜ) = 0
⊢ VectorMeasure.restrict 0 (Sᶜ) ≤ VectorMeasure.restrict (toSignedMeasure j) (Sᶜ)
refine' restrict_le_restrict_of_subset_le _ _ fun A hA hA₁ => _
case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.26725
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑j.posPart S = 0
hS₃ : ↑↑j.negPart (Sᶜ) = 0
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ Sᶜ
⊢ ↑0 A ≤ ENNReal.toReal (↑↑j.posPart A)
case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.26725
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑j.posPart S = 0
hS₃ : ↑↑j.negPart (Sᶜ) = 0
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ Sᶜ
⊢ ↑0 A ≤ ↑(toSignedMeasure j) A
rw [toSignedMeasure, toSignedMeasure_sub_apply hA,
  show j.negPart A = 0 from nonpos_iff_eq_zero.1 (hS₃ ▸ measure_mono hA₁), ENNReal.zero_toReal,
  sub_zero]
no goals
case intro.intro.intro.refine'_2
α : Type u_1
β : Type ?u.26725
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : ↑↑j.posPart S = 0
hS₃ : ↑↑j.negPart (Sᶜ) = 0
A : Set α
hA : MeasurableSet A
hA₁ : A ⊆ Sᶜ
⊢ ↑0 A ≤ ENNReal.toReal (↑↑j.posPart A)
exact ENNReal.toReal_nonneg