-- Mathlib/Analysis/SpecificLimits/RCLike.lean
theorem RCLike.tendsto_add_mul_div_add_mul_atTop_nhds (a b c : 𝕜) {d : 𝕜} (hd : d ≠ 0) :
    Tendsto (fun k : ℕ ↦ (a + c * k) / (b + d * k)) atTop (𝓝 (c / d))

Proof state:
case hl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ ?f₁ =ᶠ[atTop] fun k => (a + c * ↑k) / (b + d * ↑k)

case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto ?f₁ atTop (𝓝 (c / d))

case f₁
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ ℕ → 𝕜

Tactic:
case f₁ => exact fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)

Result:
case hl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ (fun k => (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) =ᶠ[atTop] fun k => (a + c * ↑k) / (b + d * ↑k)

case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto (fun k => (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) atTop (𝓝 (c / d))

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto (fun k => b * (↑k)⁻¹) atTop (𝓝 0)

Tactic:
apply mul_zero (_ : 𝕜) ▸ Filter.Tendsto.const_mul _ _

Result:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto (fun k => (↑k)⁻¹) atTop (𝓝 0)

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ ℕ → 𝕜

Tactic:
exact fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto (fun k => b * (↑k)⁻¹ + d) atTop (𝓝 d)

Tactic:
apply zero_add (_ : 𝕜) ▸ Filter.Tendsto.add_const _ _

Result:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto (fun k => b * (↑k)⁻¹) atTop (𝓝 0)

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto (fun k => (a + c * ↑k) / (b + d * ↑k)) atTop (𝓝 (c / d))

Tactic:
apply Filter.Tendsto.congr'

Result:
case hl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ ?f₁ =ᶠ[atTop] fun k => (a + c * ↑k) / (b + d * ↑k)

case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto ?f₁ atTop (𝓝 (c / d))

case f₁
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ ℕ → 𝕜

Proof state:
case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto (fun k => (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) atTop (𝓝 (c / d))

Tactic:
apply Filter.Tendsto.div _ _ hd

Result:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto (fun k => a * (↑k)⁻¹ + c) atTop (𝓝 c)

𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto (fun k => b * (↑k)⁻¹ + d) atTop (𝓝 d)

Proof state:
case hl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ ∀ (x : ℕ), x ≠ 0 → (fun k => (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) x = (fun k => (a + c * ↑k) / (b + d * ↑k)) x

Tactic:
intro h hx

Result:
case hl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
h : ℕ
hx : h ≠ 0
⊢ (fun k => (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) h = (fun k => (a + c * ↑k) / (b + d * ↑k)) h

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto (fun k => a * (↑k)⁻¹ + c) atTop (𝓝 c)

𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto (fun k => b * (↑k)⁻¹ + d) atTop (𝓝 d)

Tactic:
all_goals
  apply zero_add (_ : 𝕜) ▸ Filter.Tendsto.add_const _ _
  apply mul_zero (_ : 𝕜) ▸ Filter.Tendsto.const_mul _ _
  exact RCLike.tendsto_inverse_atTop_nhds_zero_nat 𝕜

Result:
no goals

Proof state:
case hl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
h : ℕ
hx : h ≠ 0
⊢ (fun k => (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) h = (fun k => (a + c * ↑k) / (b + d * ↑k)) h

Tactic:
field_simp [hx]

Result:
no goals

Proof state:
case hl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ (fun k => (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) =ᶠ[atTop] fun k => (a + c * ↑k) / (b + d * ↑k)

Tactic:
refine (eventually_ne_atTop 0).mp (Eventually.of_forall ?_)

Result:
case hl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ ∀ (x : ℕ), x ≠ 0 → (fun k => (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)) x = (fun k => (a + c * ↑k) / (b + d * ↑k)) x

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a b c d : 𝕜
hd : d ≠ 0
⊢ Tendsto (fun k => (↑k)⁻¹) atTop (𝓝 0)

Tactic:
exact RCLike.tendsto_inverse_atTop_nhds_zero_nat 𝕜

Result:
no goals