-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem tendsto_div_pow_mul_exp_add_atTop (b c : ℝ) (n : ℕ) (hb : 0 ≠ b) :
    Tendsto (fun x => x ^ n / (b * exp x + c)) atTop (𝓝 0)

Proof state:
b c : ℝ
n : ℕ
hb : 0 ≠ b
⊢ Tendsto (fun x => x ^ n / (b * rexp x + c)) atTop (𝓝 0)

Tactic:
have H : ∀ d e, 0 < d → Tendsto (fun x : ℝ => x ^ n / (d * exp x + e)) atTop (𝓝 0) := by
  intro b' c' h
  convert (tendsto_mul_exp_add_div_pow_atTop b' c' n h).inv_tendsto_atTop using 1
  ext x
  simp

Result:
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * rexp x + e)) atTop (𝓝 0)
⊢ Tendsto (fun x => x ^ n / (b * rexp x + c)) atTop (𝓝 0)

Proof state:
case h.e'_3.h
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : 0 > b
x : ℝ
⊢ x ^ n / (b * rexp x + c) = -(x ^ n / (-b * rexp x + -c))

Tactic:
field_simp

Result:
case h.e'_3.h
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : 0 > b
x : ℝ
⊢ x ^ n / (b * rexp x + c) = -x ^ n / (-(b * rexp x) + -c)

Proof state:
case h.e'_3.h
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : 0 > b
x : ℝ
⊢ x ^ n / (b * rexp x + c) = -x ^ n / (-(b * rexp x) + -c)

Tactic:
rw [← neg_add (b * exp x) c, neg_div_neg_eq]

Result:
no goals

Proof state:
case h.e'_3.h
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
x : ℝ
⊢ x ^ n / (b' * rexp x + c') = (fun x => (b' * rexp x + c') / x ^ n)⁻¹ x

Tactic:
simp

Result:
no goals

Proof state:
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * rexp x + e)) atTop (𝓝 0)
⊢ Tendsto (fun x => x ^ n / (b * rexp x + c)) atTop (𝓝 0)

Tactic:
rcases lt_or_gt_of_ne hb with h | h

Result:
case inl
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : 0 < b
⊢ Tendsto (fun x => x ^ n / (b * rexp x + c)) atTop (𝓝 0)

case inr
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : 0 > b
⊢ Tendsto (fun x => x ^ n / (b * rexp x + c)) atTop (𝓝 0)

Proof state:
case inl
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : 0 < b
⊢ Tendsto (fun x => x ^ n / (b * rexp x + c)) atTop (𝓝 0)

Tactic:
exact H b c h

Result:
no goals

Proof state:
case h.e'_3
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
⊢ (fun x => x ^ n / (b' * rexp x + c')) = (fun x => (b' * rexp x + c') / x ^ n)⁻¹

Tactic:
ext x

Result:
case h.e'_3.h
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
x : ℝ
⊢ x ^ n / (b' * rexp x + c') = (fun x => (b' * rexp x + c') / x ^ n)⁻¹ x

Proof state:
case h.e'_5
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : 0 > b
⊢ 𝓝 0 = 𝓝 (-0)

Tactic:
rw [neg_zero]

Result:
no goals

Proof state:
case inr
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : 0 > b
⊢ Tendsto (fun x => x ^ n / (b * rexp x + c)) atTop (𝓝 0)

Tactic:
convert (H (-b) (-c) (neg_pos.mpr h)).neg using 1

Result:
case h.e'_3
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : 0 > b
⊢ (fun x => x ^ n / (b * rexp x + c)) = fun x => -(x ^ n / (-b * rexp x + -c))

case h.e'_5
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : 0 > b
⊢ 𝓝 0 = 𝓝 (-0)

Proof state:
b c : ℝ
n : ℕ
hb : 0 ≠ b
⊢ ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * rexp x + e)) atTop (𝓝 0)

Tactic:
intro b' c' h

Result:
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
⊢ Tendsto (fun x => x ^ n / (b' * rexp x + c')) atTop (𝓝 0)

Proof state:
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
⊢ Tendsto (fun x => x ^ n / (b' * rexp x + c')) atTop (𝓝 0)

Tactic:
convert (tendsto_mul_exp_add_div_pow_atTop b' c' n h).inv_tendsto_atTop using 1

Result:
case h.e'_3
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
⊢ (fun x => x ^ n / (b' * rexp x + c')) = (fun x => (b' * rexp x + c') / x ^ n)⁻¹

Proof state:
case h.e'_3
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : 0 > b
⊢ (fun x => x ^ n / (b * rexp x + c)) = fun x => -(x ^ n / (-b * rexp x + -c))

Tactic:
ext x

Result:
case h.e'_3.h
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : 0 > b
x : ℝ
⊢ x ^ n / (b * rexp x + c) = -(x ^ n / (-b * rexp x + -c))