case pos
α : Type u_1
β : Type ?u.7479
inst✝³ : MeasurableSpace α
M : Type ?u.7485
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ¬restrict s i ≤ restrict 0 i
⊢ MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT s i)

case neg
α : Type u_1
β : Type ?u.7479
inst✝³ : MeasurableSpace α
M : Type ?u.7485
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ¬¬restrict s i ≤ restrict 0 i
⊢ MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT s i)
α : Type u_1
β : Type ?u.7479
inst✝³ : MeasurableSpace α
M : Type ?u.7485
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
⊢ MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT s i)
by_cases hi : ¬s ≤[i] 0
no goals
case pos
α : Type u_1
β : Type ?u.7479
inst✝³ : MeasurableSpace α
M : Type ?u.7485
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ¬restrict s i ≤ restrict 0 i
⊢ MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT s i)
exact
  let ⟨_, h, _⟩ := someExistsOneDivLT_spec hi
  h
case neg
α : Type u_1
β : Type ?u.7479
inst✝³ : MeasurableSpace α
M : Type ?u.7485
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ¬¬restrict s i ≤ restrict 0 i
⊢ MeasurableSet ∅
case neg
α : Type u_1
β : Type ?u.7479
inst✝³ : MeasurableSpace α
M : Type ?u.7485
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ¬¬restrict s i ≤ restrict 0 i
⊢ MeasurableSet (MeasureTheory.SignedMeasure.someExistsOneDivLT s i)
rw [someExistsOneDivLT, dif_neg hi]
no goals
case neg
α : Type u_1
β : Type ?u.7479
inst✝³ : MeasurableSpace α
M : Type ?u.7485
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : OrderedAddCommMonoid M
s : SignedMeasure α
i j : Set α
hi : ¬¬restrict s i ≤ restrict 0 i
⊢ MeasurableSet ∅
exact MeasurableSet.empty