α : Type u_1
β : Type ?u.5208
inst✝³ : MeasurableSpace α
M : Type ?u.5214
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ¬restrict s i ≤ restrict 0 i
⊢ Classical.choose
        (_ : MeasureTheory.SignedMeasure.ExistsOneDivLT s i (MeasureTheory.SignedMeasure.findExistsOneDivLT s i)) ⊆
      i ∧
    MeasurableSet
        (Classical.choose
          (_ : MeasureTheory.SignedMeasure.ExistsOneDivLT s i (MeasureTheory.SignedMeasure.findExistsOneDivLT s i))) ∧
      1 / (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s i) + 1) <
        ↑s
          (Classical.choose
            (_ : MeasureTheory.SignedMeasure.ExistsOneDivLT s i (MeasureTheory.SignedMeasure.findExistsOneDivLT s i)))
α : Type u_1
β : Type ?u.5208
inst✝³ : MeasurableSpace α
M : Type ?u.5214
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ¬restrict s i ≤ restrict 0 i
⊢ MeasureTheory.SignedMeasure.someExistsOneDivLT s i ⊆ i ∧
    MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT s i) ∧
      1 / (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s i) + 1) <
        ↑s (MeasureTheory.SignedMeasure.someExistsOneDivLT s i)
rw [someExistsOneDivLT, dif_pos hi]
no goals
α : Type u_1
β : Type ?u.5208
inst✝³ : MeasurableSpace α
M : Type ?u.5214
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ¬restrict s i ≤ restrict 0 i
⊢ Classical.choose
        (_ : MeasureTheory.SignedMeasure.ExistsOneDivLT s i (MeasureTheory.SignedMeasure.findExistsOneDivLT s i)) ⊆
      i ∧
    MeasurableSet
        (Classical.choose
          (_ : MeasureTheory.SignedMeasure.ExistsOneDivLT s i (MeasureTheory.SignedMeasure.findExistsOneDivLT s i))) ∧
      1 / (↑(MeasureTheory.SignedMeasure.findExistsOneDivLT s i) + 1) <
        ↑s
          (Classical.choose
            (_ : MeasureTheory.SignedMeasure.ExistsOneDivLT s i (MeasureTheory.SignedMeasure.findExistsOneDivLT s i)))
exact Classical.choose_spec (findExistsOneDivLT_spec hi)