L₁₀ div FG tendsto

theorem L₁₀_div_FG_tendsto :    Tendsto (fun t : ℝ ↦ (L₁₀.resToImagAxis t).re /      ((F.resToImagAxis t).re * (G.resToImagAxis t).re))        Filter.atTop (nhds (1 / 2)) := by  have h_wronskian : ∀ z : ℍ, F z ≠ 0 → G z ≠ 0 →      L₁₀ z / (F z * G z) = D F z / F z - D G z / G z := fun z hF hG => by    rw [L₁₀_eq_FD_G_sub_F_DG]; field_simp [hF, hG]  have hF_ne := eventually_ne_zero_of_tendsto_div (by norm_num : (720^2 : ℂ) ≠ 0) F_vanishing_order  have hG_ne := eventually_ne_zero_of_tendsto_div (by norm_num : (20480 : ℂ) ≠ 0) G_vanishing_order  have h_L_over_FG : Tendsto (L₁₀ / (F * G)) atImInfty (nhds (1 / 2)) := by    convert (D_F_div_F_tendsto.sub D_G_div_G_tendsto).congr' (by      filter_upwards [hF_ne, hG_ne] with z hF hG using (h_wronskian z hF hG).symm) using 2    all_goals norm_num  have h_re := Complex.continuous_re.continuousAt.tendsto.comp    (tendsto_resToImagAxis_of_tendsto_atImInfty h_L_over_FG)  simp only [show (1 / 2 : ℂ).re = (1 / 2 : ℝ) by norm_num] at h_re  refine h_re.congr' ?_  filter_upwards with t  simp only [Function.comp_apply]  exact ResToImagAxis.Real.re_div_mul_eq F_imag_axis_real G_imag_axis_real t