α : Type u_1
β : Type ?u.3427
inst✝³ : MeasurableSpace α
M : Type ?u.3433
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ¬restrict s i ≤ restrict 0 i
m : ℕ
hm : m < Nat.find (_ : ∃ n, MeasureTheory.SignedMeasure.ExistsOneDivLT s i n)
⊢ ¬MeasureTheory.SignedMeasure.ExistsOneDivLT s i m
α : Type u_1
β : Type ?u.3427
inst✝³ : MeasurableSpace α
M : Type ?u.3433
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ¬restrict s i ≤ restrict 0 i
m : ℕ
hm : m < MeasureTheory.SignedMeasure.findExistsOneDivLT s i
⊢ ¬MeasureTheory.SignedMeasure.ExistsOneDivLT s i m
rw [findExistsOneDivLT, dif_pos hi] at hm
no goals
α : Type u_1
β : Type ?u.3427
inst✝³ : MeasurableSpace α
M : Type ?u.3433
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ¬restrict s i ≤ restrict 0 i
m : ℕ
hm : m < Nat.find (_ : ∃ n, MeasureTheory.SignedMeasure.ExistsOneDivLT s i n)
⊢ ¬MeasureTheory.SignedMeasure.ExistsOneDivLT s i m
exact Nat.find_min _ hm