apply suggestion

TestingLowerBounds/CurvatureMeasure.lean

@@ -44,36 +44,36 @@ lemma measure_Ioi {l : ℝ} (hf : Tendsto f atTop (𝓝 l)) (x : ℝ) :
 
 --PR this and the following lemmas to mathlib, just after `StieltjesFunction.measure_univ`
 lemma measure_Ioi_of_tendsto_atTop_atTop (hf : Tendsto f atTop atTop) (x : ℝ) :
-    f.measure (Ioi x) = ⊤ := by
+    f.measure (Ioi x) = ∞ := by
   refine ENNReal.eq_top_of_forall_nnreal_le fun r ↦ ?_
   obtain ⟨N, hN⟩ := eventually_atTop.mp (tendsto_atTop.mp hf (r + f x))
   exact (f.measure_Ioc x (max x N) ▸ ENNReal.coe_nnreal_eq r ▸ (ENNReal.ofReal_le_ofReal <|
     le_tsub_of_add_le_right <| hN _ (le_max_right x N))).trans (measure_mono Ioc_subset_Ioi_self)
 
 lemma measure_Ici_of_tendsto_atTop_atTop (hf : Tendsto f atTop atTop) (x : ℝ) :
-    f.measure (Ici x) = ⊤ := by
+    f.measure (Ici x) = ∞ := by
   rw [← top_le_iff, ← f.measure_Ioi_of_tendsto_atTop_atTop hf x]
   exact measure_mono Ioi_subset_Ici_self
 
 lemma measure_Iic_of_tendsto_atBot_atBot (hf : Tendsto f atBot atBot) (x : ℝ) :
-    f.measure (Iic x) = ⊤ := by
+    f.measure (Iic x) = ∞ := by
   refine ENNReal.eq_top_of_forall_nnreal_le fun r ↦ ?_
   obtain ⟨N, hN⟩ := eventually_atBot.mp (tendsto_atBot.mp hf (f x - r))
   exact (f.measure_Ioc (min x N) x ▸ ENNReal.coe_nnreal_eq r ▸ (ENNReal.ofReal_le_ofReal <|
     le_sub_comm.mp <| hN _ (min_le_right x N))).trans (measure_mono Ioc_subset_Iic_self)
 
 lemma measure_Iio_of_tendsto_atBot_atBot (hf : Tendsto f atBot atBot) (x : ℝ) :
-    f.measure (Iio x) = ⊤ := by
+    f.measure (Iio x) = ∞ := by
   rw [← top_le_iff, ← f.measure_Iic_of_tendsto_atBot_atBot hf (x - 1)]
   exact measure_mono <| Set.Iic_subset_Iio.mpr <| sub_one_lt x
 
 lemma measure_univ_of_tendsto_atTop_atTop (hf : Tendsto f atTop atTop) :
-    f.measure univ = ⊤ := by
+    f.measure univ = ∞ := by
   rw [← top_le_iff, ← f.measure_Ioi_of_tendsto_atTop_atTop hf 0]
   exact measure_mono fun _ _ ↦ trivial
 
 lemma measure_univ_of_tendsto_atBot_atBot (hf : Tendsto f atBot atBot) :
-    f.measure univ = ⊤ := by
+    f.measure univ = ∞ := by
   rw [← top_le_iff, ← f.measure_Iio_of_tendsto_atBot_atBot hf 0]
   exact measure_mono fun _ _ ↦ trivial