∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (i : Set α),
  MeasureTheory.SignedMeasure.findExistsOneDivLT✝ s i =
    if hi : ¬MeasureTheory.VectorMeasure.restrict s i ≤ MeasureTheory.VectorMeasure.restrict 0 i then Nat.find ⋯ else 0