Fmod G right Limit At zero

theorem FmodG_rightLimitAt_zero :    Tendsto FmodGReal (nhdsWithin 0 (Set.Ioi 0)) (nhds (18 * (π ^ (-2 : ℤ)))) := by  let rhs : ℝ → ℝ := fun s ↦    (s ^ 2 * FReal s - 12 * π ^ (-1 : ℤ) * (s * ((F₁ * E₄.toFun).resToImagAxis s).re)      + 36 * π ^ (-2 : ℤ) * (E₄.toFun.resToImagAxis s).re ^ 2) /    ((H₄.resToImagAxis s).re ^ 3 *      (2 * (H₄.resToImagAxis s).re ^ 2 + 5 * (H₂.resToImagAxis s).re * (H₄.resToImagAxis s).re        + 5 * (H₂.resToImagAxis s).re ^ 2))  have hEq : ∀ᶠ s in atTop, FmodGReal (1 / s) = rhs s := by    filter_upwards [eventually_gt_atTop 0] with s hs    have hF := F_functional_equation' hs    rw [(F₁_imag_axis_real.mul E₄_imag_axis_real).eq_real_part s,      E₄_imag_axis_real.eq_real_part s] at hF    have hF' : FReal (1 / s) = s ^ 10 *        (s ^ 2 * FReal s - 12 * π ^ (-1 : ℤ) * (s * ((F₁ * E₄.toFun).resToImagAxis s).re)          + 36 * π ^ (-2 : ℤ) * (E₄.toFun.resToImagAxis s).re ^ 2) := by      push_cast [← Complex.ofReal_inj]      linear_combination hF    unfold FmodGReal    rw [G_functional_eq_real hs, hF', mul_assoc (s ^ 10)]    exact mul_div_mul_left _ _ (pow_ne_zero 10 hs.ne')  have hlim : Tendsto rhs atTop (nhds (18 * π ^ (-2 : ℤ))) := by    convert numerator_tendsto_at_infty.div denominator_tendsto_at_infty (by norm_num) using 2    · rfl    · ring  exact (hlim.comp tendsto_inv_nhdsGT_zero).congr' <|    (tendsto_inv_nhdsGT_zero.eventually hEq).mono fun t ht => by      simpa [one_div, inv_inv] using ht.symm