bound_f_second_term

lemma bound_f_second_term (f : ℝ → ℝ) (hf : Tendsto f atTop (nhds 0)) (δ : ℝ) (hδ : δ > 0) :    ∀ᶠ x : ℝ in atTop, (1 + f x) < (1 + δ) := by  have bound_one_plus_f: ∀ y: ℝ, ∀ z: ℝ, |f y| < z → 1 + (f y) < 1 + z := by    intro y z hf    by_cases f_pos: 0 < f y    · rw [abs_of_pos f_pos] at hf      linarith    · rw [not_lt] at f_pos      rw [abs_of_nonpos f_pos] at hf      linarith   have f_small := NormedAddGroup.tendsto_nhds_zero.mp hf δ hδ  simp only [norm_eq_abs, eventually_atTop] at f_small  obtain ⟨p, hp⟩ := f_small   let a := ((max 1 p) : ℝ)  have ha: ∀ b: ℝ, a ≤ b → |f b| < δ := by    intro b hb    have b_ge_p: p ≤ b := by      have a_ge_p: p ≤ a := by simp [a]      linarith    exact hp b b_ge_p   rw [Filter.eventually_atTop]   use a  intro b hb  exact bound_one_plus_f b δ (ha b (by linarith))