case inl
α : Type ?u.33412
x y z : ℝ
l : Filter α
b c : ℝ
hb : 0 < b
⊢ Tendsto (fun x => (b * exp x + c) / x ^ 0) atTop atTop

case inr
α : Type ?u.33412
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
⊢ Tendsto (fun x => (b * exp x + c) / x ^ n) atTop atTop
α : Type ?u.33412
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 < b
⊢ Tendsto (fun x => (b * exp x + c) / x ^ n) atTop atTop
rcases eq_or_ne n 0 with (rfl | hn)
case inr
α : Type ?u.33412
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
⊢ Tendsto (fun x => b * (exp x / x ^ n) + c / x ^ n) atTop atTop
case inr
α : Type ?u.33412
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
⊢ Tendsto (fun x => (b * exp x + c) / x ^ n) atTop atTop
simp only [add_div, mul_div_assoc]
no goals
case inr
α : Type ?u.33412
x y z : ℝ
l : Filter α
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
⊢ Tendsto (fun x => b * (exp x / x ^ n) + c / x ^ n) atTop atTop
exact
  ((tendsto_exp_div_pow_atTop n).const_mul_atTop hb).atTop_add
    (tendsto_const_nhds.div_atTop (tendsto_pow_atTop hn))
case inl
α : Type ?u.33412
x y z : ℝ
l : Filter α
b c : ℝ
hb : 0 < b
⊢ Tendsto (fun x => b * exp x + c) atTop atTop
case inl
α : Type ?u.33412
x y z : ℝ
l : Filter α
b c : ℝ
hb : 0 < b
⊢ Tendsto (fun x => (b * exp x + c) / x ^ 0) atTop atTop
simp only [pow_zero, div_one]
no goals
case inl
α : Type ?u.33412
x y z : ℝ
l : Filter α
b c : ℝ
hb : 0 < b
⊢ Tendsto (fun x => b * exp x + c) atTop atTop
exact (tendsto_exp_atTop.const_mul_atTop hb).atTop_add tendsto_const_nhds