∀ {𝕜 : Type u_4} [inst : Semifield 𝕜] [inst_1 : CharZero 𝕜] [inst_2 : TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜]
  [IsTopologicalSemiring 𝕜] [ContinuousInv₀ 𝕜] (a b c : 𝕜) {d : 𝕜},
  d ≠ 0 → Filter.Tendsto (fun k => (a + c * ↑k) / (b + d * ↑k)) Filter.atTop (nhds (c / d))