-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem exp_neg_mul_rpow_isLittleO_exp_neg {p b : ℝ} (hb : 0 < b) (hp : 1 < p) :
    (fun x : ℝ => exp (- b * x ^ p)) =o[atTop] fun x : ℝ => exp (-x)

Proof state:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (fun x => x * (b * x ^ (p - 1) + -1)) atTop atTop
x : ℝ
hx : x ∈ Ioi 0
⊢ x * (b * x ^ (p - 1) + -1) = -x - -b * x ^ p

Tactic:
rw [mem_Ioi] at hx

Result:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (fun x => x * (b * x ^ (p - 1) + -1)) atTop atTop
x : ℝ
hx : 0 < x
⊢ x * (b * x ^ (p - 1) + -1) = -x - -b * x ^ p

Proof state:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (fun x => x * (b * x ^ (p - 1) + -1)) atTop atTop
x : ℝ
hx : 0 < x
⊢ x * (b * (x ^ p / x) + -1) = -x - -b * x ^ p

Tactic:
field_simp [hx.ne']

Result:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (fun x => x * (b * x ^ (p - 1) + -1)) atTop atTop
x : ℝ
hx : 0 < x
⊢ b * x ^ p + -x = -x + b * x ^ p

Proof state:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (fun x => x * (b * x ^ (p - 1) + -1)) atTop atTop
⊢ (fun x => x * (b * x ^ (p - 1) + -1)) =ᶠ[atTop] fun x => -x - -b * x ^ p

Tactic:
refine eventuallyEq_of_mem (Ioi_mem_atTop (0 : ℝ)) (fun x hx => ?_)

Result:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (fun x => x * (b * x ^ (p - 1) + -1)) atTop atTop
x : ℝ
hx : x ∈ Ioi 0
⊢ x * (b * x ^ (p - 1) + -1) = -x - -b * x ^ p

Proof state:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ Tendsto (fun x => b * x ^ (p - 1) + -1) atTop atTop

Tactic:
refine tendsto_atTop_add_const_right atTop (-1 : ℝ) ?_

Result:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ Tendsto (fun x => b * x ^ (p - 1)) atTop atTop

Proof state:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ Tendsto (fun x => -x - -b * x ^ p) atTop atTop

Tactic:
suffices Tendsto (fun x => x * (b * x ^ (p - 1) + -1)) atTop atTop by
  refine Tendsto.congr' ?_ this
  refine eventuallyEq_of_mem (Ioi_mem_atTop (0 : ℝ)) (fun x hx => ?_)
  rw [mem_Ioi] at hx
  rw [rpow_sub_one hx.ne']
  field_simp [hx.ne']
  ring

Result:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ Tendsto (fun x => x * (b * x ^ (p - 1) + -1)) atTop atTop

Proof state:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ (fun x => rexp (-b * x ^ p)) =o[atTop] fun x => rexp (-x)

Tactic:
rw [isLittleO_exp_comp_exp_comp]

Result:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ Tendsto (fun x => -x - -b * x ^ p) atTop atTop

Proof state:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (fun x => x * (b * x ^ (p - 1) + -1)) atTop atTop
⊢ Tendsto (fun x => -x - -b * x ^ p) atTop atTop

Tactic:
refine Tendsto.congr' ?_ this

Result:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (fun x => x * (b * x ^ (p - 1) + -1)) atTop atTop
⊢ (fun x => x * (b * x ^ (p - 1) + -1)) =ᶠ[atTop] fun x => -x - -b * x ^ p

Proof state:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ Tendsto (fun x => b * x ^ (p - 1)) atTop atTop

Tactic:
exact Tendsto.const_mul_atTop hb (tendsto_rpow_atTop (by linarith))

Result:
no goals

Proof state:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ 0 < p - 1

Tactic:
linarith

Result:
no goals

Proof state:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (fun x => x * (b * x ^ (p - 1) + -1)) atTop atTop
x : ℝ
hx : 0 < x
⊢ b * x ^ p + -x = -x + b * x ^ p

Tactic:
ring

Result:
no goals

Proof state:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ Tendsto (fun x => x * (b * x ^ (p - 1) + -1)) atTop atTop

Tactic:
apply tendsto_id.atTop_mul_atTop₀

Result:
p b : ℝ
hb : 0 < b
hp : 1 < p
⊢ Tendsto (fun x => b * x ^ (p - 1) + -1) atTop atTop

Proof state:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (fun x => x * (b * x ^ (p - 1) + -1)) atTop atTop
x : ℝ
hx : 0 < x
⊢ x * (b * x ^ (p - 1) + -1) = -x - -b * x ^ p

Tactic:
rw [rpow_sub_one hx.ne']

Result:
p b : ℝ
hb : 0 < b
hp : 1 < p
this : Tendsto (fun x => x * (b * x ^ (p - 1) + -1)) atTop atTop
x : ℝ
hx : 0 < x
⊢ x * (b * (x ^ p / x) + -1) = -x - -b * x ^ p