Is Big O res To Imag Axis of is Big O at Im Infty

lemma isBigO_resToImagAxis_of_isBigO_atImInfty {F : ℍ → ℂ} {c : ℝ} (_hc : 0 < c)    (hF : F =O[atImInfty] fun τ => Real.exp (-c * τ.im)) :    F.resToImagAxis =O[atTop] fun t => Real.exp (-c * t) := by  rw [Asymptotics.isBigO_iff] at hF ⊢  obtain ⟨C, hC⟩ := hF; use C  rw [Filter.eventually_atImInfty] at hC; obtain ⟨A, hA⟩ := hC  filter_upwards [Filter.eventually_ge_atTop (max A 1)] with t ht  have ht_pos : 0 < t := lt_of_lt_of_le one_pos (le_of_max_le_right ht)  simp only [Function.resToImagAxis, ResToImagAxis, ht_pos, ↓reduceDIte]  set z : ℍ := ⟨Complex.I * t, by simp [ht_pos]⟩  have him : z.im = t := by change (Complex.I * t).im = t; simp  simpa [him] using hA z (by simpa [him] using le_of_max_le_left ht)