bound_f_first_term

lemma bound_f_first_term {ε : ℝ} (hε : 0 < ε) (f : ℝ → ℝ)    (hf : Tendsto f atTop (nhds 0)) (δ : ℝ) (hδ : δ > 0) :    ∀ᶠ x: ℝ in atTop, (1 + f ((1 + ε) * 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   have a_pos: 0 < a := by    simp [a]   have pos_mul: ∀ x y z : ℝ, 0 < x → 0 < y → 1 < z → x ≤ y → x < y * z := by    intro x y z _ hy hz hlt    have y_lt: y < y * z := by      exact (lt_mul_iff_one_lt_right hy).mpr hz    linarith   have mul_increase: a ≤ (1 + ε) * b := by    simp only [ a] at hb    have a_le := pos_mul a b (1 + ε) a_pos (by linarith) (by linarith) (by linarith)    linarith   exact bound_one_plus_f ((1 + ε) * b) δ (ha ((1 + ε) * b) mul_increase)