α : Type u_1
β : Type ?u.2701
inst✝³ : MeasurableSpace α
M : Type ?u.2707
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ¬restrict s i ≤ restrict 0 i
⊢ MeasureTheory.SignedMeasure.ExistsOneDivLT s i (Nat.find (_ : ∃ n, MeasureTheory.SignedMeasure.ExistsOneDivLT s i n))
α : Type u_1
β : Type ?u.2701
inst✝³ : MeasurableSpace α
M : Type ?u.2707
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ¬restrict s i ≤ restrict 0 i
⊢ MeasureTheory.SignedMeasure.ExistsOneDivLT s i (MeasureTheory.SignedMeasure.findExistsOneDivLT s i)
rw [findExistsOneDivLT, dif_pos hi]
no goals
α : Type u_1
β : Type ?u.2701
inst✝³ : MeasurableSpace α
M : Type ?u.2707
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ¬restrict s i ≤ restrict 0 i
⊢ MeasureTheory.SignedMeasure.ExistsOneDivLT s i (Nat.find (_ : ∃ n, MeasureTheory.SignedMeasure.ExistsOneDivLT s i n))
convert Nat.find_spec (existsNatOneDivLTMeasure_of_not_negative hi)