α : Type u_1
β : Type ?u.37523
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
i : Set α :=
  choose
    (_ :
      ∃ i,
        MeasurableSet i ∧
          VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i ∧
            VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ))
⊢ ∃ i hi₁ hi₂ hi₃,
    (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂ ∧
      (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
α : Type u_1
β : Type ?u.37523
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
⊢ ∃ i hi₁ hi₂ hi₃,
    (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂ ∧
      (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
set i := choose s.exists_compl_positive_negative
case intro.intro
α : Type u_1
β : Type ?u.37523
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
i : Set α :=
  choose
    (_ :
      ∃ i,
        MeasurableSet i ∧
          VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i ∧
            VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ))
hi₁ :
  MeasurableSet
    (choose
      (_ :
        ∃ i,
          MeasurableSet i ∧
            VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i ∧
              VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)))
hi₂ :
  VectorMeasure.restrict 0
      (choose
        (_ :
          ∃ i,
            MeasurableSet i ∧
              VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i ∧
                VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ))) ≤
    VectorMeasure.restrict s
      (choose
        (_ :
          ∃ i,
            MeasurableSet i ∧
              VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i ∧
                VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)))
hi₃ :
  VectorMeasure.restrict s
      (choose
          (_ :
            ∃ i,
              MeasurableSet i ∧
                VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i ∧
                  VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ))ᶜ) ≤
    VectorMeasure.restrict 0
      (choose
          (_ :
            ∃ i,
              MeasurableSet i ∧
                VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i ∧
                  VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ))ᶜ)
⊢ ∃ i hi₁ hi₂ hi₃,
    (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂ ∧
      (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
α : Type u_1
β : Type ?u.37523
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
i : Set α :=
  choose
    (_ :
      ∃ i,
        MeasurableSet i ∧
          VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i ∧
            VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ))
⊢ ∃ i hi₁ hi₂ hi₃,
    (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂ ∧
      (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
obtain ⟨hi₁, hi₂, hi₃⟩ := choose_spec s.exists_compl_positive_negative
no goals
case intro.intro
α : Type u_1
β : Type ?u.37523
inst✝² : MeasurableSpace α
s✝ : SignedMeasure α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
s : SignedMeasure α
i : Set α :=
  choose
    (_ :
      ∃ i,
        MeasurableSet i ∧
          VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i ∧
            VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ))
hi₁ :
  MeasurableSet
    (choose
      (_ :
        ∃ i,
          MeasurableSet i ∧
            VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i ∧
              VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)))
hi₂ :
  VectorMeasure.restrict 0
      (choose
        (_ :
          ∃ i,
            MeasurableSet i ∧
              VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i ∧
                VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ))) ≤
    VectorMeasure.restrict s
      (choose
        (_ :
          ∃ i,
            MeasurableSet i ∧
              VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i ∧
                VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ)))
hi₃ :
  VectorMeasure.restrict s
      (choose
          (_ :
            ∃ i,
              MeasurableSet i ∧
                VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i ∧
                  VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ))ᶜ) ≤
    VectorMeasure.restrict 0
      (choose
          (_ :
            ∃ i,
              MeasurableSet i ∧
                VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i ∧
                  VectorMeasure.restrict s (iᶜ) ≤ VectorMeasure.restrict 0 (iᶜ))ᶜ)
⊢ ∃ i hi₁ hi₂ hi₃,
    (toJordanDecomposition s).posPart = toMeasureOfZeroLE s i hi₁ hi₂ ∧
      (toJordanDecomposition s).negPart = toMeasureOfLEZero s (iᶜ) (_ : MeasurableSet (iᶜ)) hi₃
exact ⟨i, hi₁, hi₂, hi₃, rfl, rfl⟩