α : Type ?u.34915
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
⊢ Tendsto (fun x => x ^ n / (b * exp x + c)) atTop (𝓝 0)
α : Type ?u.34915
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
⊢ Tendsto (fun x => x ^ n / (b * exp x + c)) atTop (𝓝 0)
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
case inl
α : Type ?u.34915
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 < b
⊢ Tendsto (fun x => x ^ n / (b * exp x + c)) atTop (𝓝 0)

case inr
α : Type ?u.34915
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
⊢ Tendsto (fun x => x ^ n / (b * exp x + c)) atTop (𝓝 0)
α : Type ?u.34915
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
⊢ Tendsto (fun x => x ^ n / (b * exp x + c)) atTop (𝓝 0)
cases' lt_or_gt_of_ne hb with h h
α : Type ?u.34915
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
⊢ Tendsto (fun x => x ^ n / (b' * exp x + c')) atTop (𝓝 0)
α : Type ?u.34915
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
⊢ ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
intro b' c' h
case h.e'_3
α : Type ?u.34915
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
⊢ (fun x => x ^ n / (b' * exp x + c')) = (fun x => (b' * exp x + c') / x ^ n)⁻¹
α : Type ?u.34915
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
⊢ Tendsto (fun x => x ^ n / (b' * exp x + c')) atTop (𝓝 0)
convert(tendsto_mul_exp_add_div_pow_atTop b' c' n h).inv_tendsto_atTop using 1
case h.e'_3.h
α : Type ?u.34915
x✝ y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
x : ℝ
⊢ x ^ n / (b' * exp x + c') = (fun x => (b' * exp x + c') / x ^ n)⁻¹ x
case h.e'_3
α : Type ?u.34915
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
⊢ (fun x => x ^ n / (b' * exp x + c')) = (fun x => (b' * exp x + c') / x ^ n)⁻¹
ext x
no goals
case h.e'_3.h
α : Type ?u.34915
x✝ y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
x : ℝ
⊢ x ^ n / (b' * exp x + c') = (fun x => (b' * exp x + c') / x ^ n)⁻¹ x
simp
no goals
case inl
α : Type ?u.34915
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 < b
⊢ Tendsto (fun x => x ^ n / (b * exp x + c)) atTop (𝓝 0)
exact H b c h
case h.e'_3
α : Type ?u.34915
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
⊢ (fun x => x ^ n / (b * exp x + c)) = fun x => -(x ^ n / (-b * exp x + -c))

case h.e'_5
α : Type ?u.34915
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
⊢ 𝓝 0 = 𝓝 (-0)
case inr
α : Type ?u.34915
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
⊢ Tendsto (fun x => x ^ n / (b * exp x + c)) atTop (𝓝 0)
convert(H (-b) (-c) (neg_pos.mpr h)).neg using 1
case h.e'_3.h
α : Type ?u.34915
x✝ y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
x : ℝ
⊢ x ^ n / (b * exp x + c) = -(x ^ n / (-b * exp x + -c))
case h.e'_3
α : Type ?u.34915
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
⊢ (fun x => x ^ n / (b * exp x + c)) = fun x => -(x ^ n / (-b * exp x + -c))
ext x
case h.e'_3.h
α : Type ?u.34915
x✝ y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
x : ℝ
⊢ x ^ n / (b * exp x + c) = -x ^ n / (-(b * exp x) + -c)
case h.e'_3.h
α : Type ?u.34915
x✝ y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
x : ℝ
⊢ x ^ n / (b * exp x + c) = -(x ^ n / (-b * exp x + -c))
field_simp
no goals
case h.e'_3.h
α : Type ?u.34915
x✝ y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
x : ℝ
⊢ x ^ n / (b * exp x + c) = -x ^ n / (-(b * exp x) + -c)
rw [← neg_add (b * exp x) c, neg_div_neg_eq]
no goals
case h.e'_5
α : Type ?u.34915
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (fun x => x ^ n / (d * exp x + e)) atTop (𝓝 0)
h : 0 > b
⊢ 𝓝 0 = 𝓝 (-0)
rw [neg_zero]