-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem exists_compl_positive_negative :
    ∃ S : Set α,
      MeasurableSet S ∧
        j.toSignedMeasure ≤[S] 0 ∧
          0 ≤[Sᶜ] j.toSignedMeasure ∧ j.posPart S = 0 ∧ j.negPart Sᶜ = 0

Proof state:
case intro.intro.intro.refine_2
α : Type u_1
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 ≤ (j.posPart A).toReal

Tactic:
exact ENNReal.toReal_nonneg

Result:
no goals

Proof state:
case intro.intro.intro.refine_1
α : Type u_1
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
⊢ ↑j.toSignedMeasure A ≤ ↑0 A

Tactic:
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]

Result:
case intro.intro.intro.refine_1
α : Type u_1
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 ≤ (j.negPart A).toReal

Proof state:
case intro.intro.intro.refine_2
α : Type u_1
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 ≤ ↑j.toSignedMeasure A

Tactic:
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]

Result:
case intro.intro.intro.refine_2
α : Type u_1
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 ≤ (j.posPart A).toReal

Proof state:
case intro.intro.intro.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
⊢ 0 ≤[Sᶜ] j.toSignedMeasure

Tactic:
refine restrict_le_restrict_of_subset_le _ _ fun A hA hA₁ => ?_

Result:
case intro.intro.intro.refine_2
α : Type u_1
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 ≤ ↑j.toSignedMeasure A

Proof state:
case intro.intro.intro.refine_1
α : Type u_1
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 ≤ (j.negPart A).toReal

Tactic:
exact ENNReal.toReal_nonneg

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
⊢ ∃ S, MeasurableSet S ∧ j.toSignedMeasure ≤[S] 0 ∧ 0 ≤[Sᶜ] j.toSignedMeasure ∧ j.posPart S = 0 ∧ j.negPart Sᶜ = 0

Tactic:
refine ⟨S, hS₁, ?_, ?_, hS₂, hS₃⟩

Result:
case intro.intro.intro.refine_1
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
⊢ j.toSignedMeasure ≤[S] 0

case intro.intro.intro.refine_2
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
⊢ 0 ≤[Sᶜ] j.toSignedMeasure

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
⊢ ∃ S, MeasurableSet S ∧ j.toSignedMeasure ≤[S] 0 ∧ 0 ≤[Sᶜ] j.toSignedMeasure ∧ j.posPart S = 0 ∧ j.negPart Sᶜ = 0

Tactic:
obtain ⟨S, hS₁, hS₂, hS₃⟩ := j.mutuallySingular

Result:
case intro.intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
⊢ ∃ S, MeasurableSet S ∧ j.toSignedMeasure ≤[S] 0 ∧ 0 ≤[Sᶜ] j.toSignedMeasure ∧ j.posPart S = 0 ∧ j.negPart Sᶜ = 0

Proof state:
case intro.intro.intro.refine_1
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
S : Set α
hS₁ : MeasurableSet S
hS₂ : j.posPart S = 0
hS₃ : j.negPart Sᶜ = 0
⊢ j.toSignedMeasure ≤[S] 0

Tactic:
refine restrict_le_restrict_of_subset_le _ _ fun A hA hA₁ => ?_

Result:
case intro.intro.intro.refine_1
α : Type u_1
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
⊢ ↑j.toSignedMeasure A ≤ ↑0 A