awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
case case₁ case₂ : ∃ (c : ℝ), ∀ᶠ (x : ℝ) in atTop, ‖cos (x * π)‖ ≤ c * Norm.norm (E := ℝ) 1
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ cos (x * π)) fun (_x : ℝ) ↦ 1

Tactic:
case cos =>
      rw [isBigO_iff]
      exact ⟨1, Eventually.of_forall fun x => by simp [Real.abs_cos_le_one]⟩

Premises used: Real.cos, Asymptotics.isBigO_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : b < 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atTop (𝓝 0)

Tactic:
case inl => -- b < 0
    simp_rw [Real.rpow_def_of_nonpos hb.le, hb.ne, ite_false]
    rw [← isLittleO_const_iff (c := (1 : ℝ)) one_ne_zero, (one_mul (1 : ℝ)).symm]
    refine IsLittleO.mul_isBigO ?exp ?cos
    case exp =>
      rw [isLittleO_const_iff one_ne_zero]
      refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
      rw [← log_neg_eq_log, log_neg_iff (by linarith)]
      linarith
    case cos =>
      rw [isBigO_iff]
      exact ⟨1, Eventually.of_forall fun x => by simp [Real.abs_cos_le_one]⟩

Premises used: Iff.mpr, Asymptotics.isLittleO_const_iff, Real.log_neg_eq_log, Real.cos, Filter.tendsto_id, ite_false, Asymptotics.isBigO_iff, LT.lt.le, Real.exp, Real.tendsto_exp_atBot, Filter.tendsto_const_mul_atBot_of_neg, Filter.Tendsto.comp, Real.rpow_def_of_nonpos, Asymptotics.IsLittleO.mul_isBigO, one_ne_zero, OfNat.ofNat, Eq.symm, one_mul, LT.lt.ne, Real.log_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
hb₀ : LT.lt (α := ℝ) (-1) 0
hb₁ : LT.lt (α := ℝ) 0 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 0 x) atTop (𝓝 0)

Tactic:
Tendsto.mono_right ?_ (Iff.mpr pure_le_nhds_iff rfl)

Premises used: Iff.mpr, Filter.Tendsto.mono_right, rfl, pure_le_nhds_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
hb₀ : LT.lt (α := ℝ) (-1) 0
hb₁ : LT.lt (α := ℝ) 0 1
refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 0 x) atTop (pure 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 0 x) atTop (𝓝 0)

Tactic:
refine Tendsto.mono_right ?_ (Iff.mpr pure_le_nhds_iff rfl)

Premises used: Iff.mpr, Filter.Tendsto.mono_right, rfl, pure_le_nhds_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
hb₀ : LT.lt (α := ℝ) (-1) 0
hb₁ : LT.lt (α := ℝ) 0 1
rw : ∀ᶠ (x : ℝ) in atTop, HPow.hPow (α := ℝ) 0 x = 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 0 x) atTop (pure 0)

Tactic:
rw [tendsto_pure]

Premises used: Filter.tendsto_pure
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
hb₀ : LT.lt (α := ℝ) (-1) 0
hb₁ : LT.lt (α := ℝ) 0 1
h : ∀ (a : ℝ) (hx : a ≠ 0), HPow.hPow (α := ℝ) 0 a = 0
⊢ ∀ᶠ (x : ℝ) in atTop, HPow.hPow (α := ℝ) 0 x = 0

Tactic:
filter_upwards [eventually_ne_atTop 0] with _ hx

Premises used: Filter.eventually_ne_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
hb₀ : LT.lt (α := ℝ) (-1) 0
hb₁ : LT.lt (α := ℝ) 0 1
a : ℝ
hx : a ≠ 0
⊢ HPow.hPow (α := ℝ) 0 a = 0

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
hb₀ : LT.lt (α := ℝ) (-1) 0
hb₁ : LT.lt (α := ℝ) 0 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (α := ℝ) 0 x) atTop (𝓝 0)

Tactic:
case inr.inl => -- b = 0
    refine Tendsto.mono_right ?_ (Iff.mpr pure_le_nhds_iff rfl)
    rw [tendsto_pure]
    filter_upwards [eventually_ne_atTop 0] with _ hx
    simp [hx]

Premises used: Iff.mpr, Filter.eventually_ne_atTop, Filter.tendsto_pure, Filter.Tendsto.mono_right, OfNat.ofNat, rfl, pure_le_nhds_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
simp_rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atTop (𝓝 0)

Tactic:
simp_rw [Real.rpow_def_of_pos hb]

Premises used: Real.rpow_def_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atTop (𝓝 0)

Tactic:
tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id

Premises used: Iff.mpr, Filter.tendsto_id, Real.exp, Real.tendsto_exp_atBot, Filter.tendsto_const_mul_atBot_of_neg, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
refine : log b < 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atTop (𝓝 0)

Tactic:
refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id

Premises used: Iff.mpr, Filter.tendsto_id, Real.tendsto_exp_atBot, Filter.tendsto_const_mul_atBot_of_neg, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ log b < 0

Tactic:
(log_neg_iff hb).mpr hb₁

Premises used: Iff.mpr, Real.log_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
⊢ log b < 0

Tactic:
exact (log_neg_iff hb).mpr hb₁

Premises used: Iff.mpr, Real.log_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : -1 < b
hb₁ : b < 1
hb : 0 < b
case : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atTop (𝓝 0)
case₁ : log b < 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atTop (𝓝 0)

Tactic:
case inr.inr => -- b > 0
    simp_rw [Real.rpow_def_of_pos hb]
    refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_neg ?_).mpr tendsto_id
    exact (log_neg_iff hb).mpr hb₁

Premises used: Iff.mpr, Real.rpow_def_of_pos, Filter.tendsto_id, Real.tendsto_exp_atBot, Filter.tendsto_const_mul_atBot_of_neg, Filter.Tendsto.comp, Real.log_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ 0 < b

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
simp_rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atBot atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atBot atTop

Tactic:
simp_rw [Real.rpow_def_of_pos (by positivity : 0 < b)]

Premises used: Real.rpow_def_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atBot atTop

Tactic:
tendsto_exp_atTop.comp <| (tendsto_const_mul_atTop_iff_neg <| tendsto_id (α := ℝ)).mpr ?_

Premises used: Iff.mpr, Real.tendsto_exp_atTop, Filter.tendsto_id, Real.exp, Filter.tendsto_const_mul_atTop_iff_neg, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
refine : log b < 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atBot atTop

Tactic:
refine tendsto_exp_atTop.comp <| (tendsto_const_mul_atTop_iff_neg <| tendsto_id (α := ℝ)).mpr ?_

Premises used: Iff.mpr, Real.tendsto_exp_atTop, Filter.tendsto_id, Filter.tendsto_const_mul_atTop_iff_neg, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ log b < 0

Tactic:
(log_neg_iff hb₀).mpr hb₁

Premises used: Iff.mpr, Real.log_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb₀ : 0 < b
hb₁ : b < 1
⊢ log b < 0

Tactic:
exact (log_neg_iff hb₀).mpr hb₁

Premises used: Iff.mpr, Real.log_neg_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb : 1 < b
⊢ 0 < b

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb : 1 < b
simp_rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atBot (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b ^ x) atBot (𝓝 0)

Tactic:
simp_rw [Real.rpow_def_of_pos (by positivity : 0 < b)]

Premises used: Real.rpow_def_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb : 1 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atBot (𝓝 0)

Tactic:
tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_pos ?_).mpr tendsto_id

Premises used: Iff.mpr, Filter.tendsto_id, Real.exp, Real.tendsto_exp_atBot, Filter.Tendsto.comp, Filter.tendsto_const_mul_atBot_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb : 1 < b
refine : 0 < log b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (log b * x)) atBot (𝓝 0)

Tactic:
refine tendsto_exp_atBot.comp <| (tendsto_const_mul_atBot_of_pos ?_).mpr tendsto_id

Premises used: Iff.mpr, Filter.tendsto_id, Real.tendsto_exp_atBot, Filter.Tendsto.comp, Filter.tendsto_const_mul_atBot_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb : 1 < b
⊢ 0 ≤ b

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb : 1 < b
⊢ 1 < b

Tactic:
aesop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
b : ℝ
hb : 1 < b
⊢ 0 < log b

Tactic:
exact (log_pos_iff (by positivity)).mpr <| by aesop

Premises used: Iff.mpr, Real.log_pos_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a b c : ℝ
hb : 0 ≠ b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ a * (x / (b * rexp x + c))) atTop (𝓝 0)

Tactic:
simpa only [mul_zero, pow_one] using
                (tendsto_const_nhds (x := a)).mul
                  (tendsto_div_pow_mul_exp_add_atTop b c 1 hb)

Premises used: tendsto_const_nhds, MulZeroClass.mul_zero, Filter.Tendsto.mul, pow_one, Real.tendsto_div_pow_mul_exp_add_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a b c : ℝ
hb : 0 ≠ b
simpa : (rexp ∘ fun (x : ℝ) ↦ a * (x / (b * rexp x + c))) ∘ log =ᶠ[atTop] fun (x : ℝ) ↦ x ^ (a / (b * x + c))
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ (a / (b * x + c))) atTop (𝓝 1)

Tactic:
refine
    Tendsto.congr' ?_
      ((tendsto_exp_nhds_zero_nhds_one.comp
            (by
              simpa only [mul_zero, pow_one] using
                (tendsto_const_nhds (x := a)).mul
                  (tendsto_div_pow_mul_exp_add_atTop b c 1 hb))).comp
        tendsto_log_atTop)

Premises used: Real.tendsto_exp_nhds_zero_nhds_one, Real.tendsto_log_atTop, Filter.Tendsto.comp, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a b c : ℝ
hb : 0 ≠ b
apply : EqOn ((rexp ∘ fun (x : ℝ) ↦ a * (x / (b * rexp x + c))) ∘ log) (fun (x : ℝ) ↦ x ^ (a / (b * x + c))) (Set.Ioi 0)
⊢ (rexp ∘ fun (x : ℝ) ↦ a * (x / (b * rexp x + c))) ∘ log =ᶠ[atTop] fun (x : ℝ) ↦ x ^ (a / (b * x + c))

Tactic:
apply eventuallyEq_of_mem (Ioi_mem_atTop (0 : ℝ))

Premises used: Filter.eventuallyEq_of_mem, Filter.Ioi_mem_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioi 0) x
⊢ 0 < x

Tactic:
simp only [Set.mem_Ioi, Function.comp_apply] at hx ⊢

Premises used: Set.mem_Ioi, Function.comp_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
rw : rexp (a * (log x / (b * x + c))) = rexp (a / (b * x + c) * log x)
⊢ rexp (a * (log x / (b * rexp (log x) + c))) = x ^ (a / (b * x + c))

Tactic:
rw [exp_log hx, ← exp_log (rpow_pos_of_pos hx (a / (b * x + c))), log_rpow hx (a / (b * x + c))]

Premises used: Real.rpow_pos_of_pos, HMul.hMul, Real.log_rpow, HDiv.hDiv, Real.exp_log, HAdd.hAdd
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
a b c : ℝ
hb : 0 ≠ b
x : ℝ
hx : 0 < x
⊢ rexp (a * (log x / (b * x + c))) = rexp (a / (b * x + c) * log x)

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ (1 / (1 * x + 0))) atTop (𝓝 1)

Tactic:
tendsto_rpow_div_mul_add (1 : ℝ) _ (0 : ℝ) zero_ne_one

Premises used: zero_ne_one, tendsto_rpow_div_mul_add, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
h : ∀ (x : ℝ), x = 1 * x + 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ (1 / x)) atTop (𝓝 1)

Tactic:
convert! tendsto_rpow_div_mul_add (1 : ℝ) _ (0 : ℝ) zero_ne_one

Premises used: zero_ne_one, tendsto_rpow_div_mul_add, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
x : ℝ
⊢ x = 1 * x + 0

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ (-1 / (1 * x + 0))) atTop (𝓝 1)

Tactic:
tendsto_rpow_div_mul_add (-(1 : ℝ)) _ (0 : ℝ) zero_ne_one

Premises used: zero_ne_one, tendsto_rpow_div_mul_add, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
h : ∀ (x : ℝ), x = 1 * x + 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ (-1 / x)) atTop (𝓝 1)

Tactic:
convert! tendsto_rpow_div_mul_add (-(1 : ℝ)) _ (0 : ℝ) zero_ne_one

Premises used: zero_ne_one, tendsto_rpow_div_mul_add, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s : ℝ
obtain : ∀ (n : ℕ) (hn : s < (↑n : ℝ)), Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp x / x ^ s) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp x / x ^ s) atTop atTop

Tactic:
obtain ⟨n, hn⟩ := archimedean_iff_nat_lt.1 Real.instArchimedean s

Premises used: Real.instArchimedean, archimedean_iff_nat_lt, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s : ℝ
n : ℕ
hn : s < (↑n : ℝ)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp x / x ^ s) atTop atTop

Tactic:
tendsto_atTop_mono' _ ?_ (tendsto_exp_div_pow_atTop n)

Premises used: Real.tendsto_exp_div_pow_atTop, Filter.tendsto_atTop_mono'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s : ℝ
n : ℕ
hn : s < (↑n : ℝ)
refine : EventuallyLE (β := ℝ) atTop (fun (x : ℝ) ↦ rexp x / x ^ n) fun (x : ℝ) ↦ rexp x / x ^ s
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp x / x ^ s) atTop atTop

Tactic:
refine tendsto_atTop_mono' _ ?_ (tendsto_exp_div_pow_atTop n)

Premises used: Real.tendsto_exp_div_pow_atTop, Filter.tendsto_atTop_mono'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s : ℝ
n : ℕ
hn : s < (↑n : ℝ)
h : ∀ (x : ℝ) (hx₀ : 0 < x) (hx₁ : 1 ≤ x), rexp x / x ^ n ≤ rexp x / x ^ s
⊢ EventuallyLE (β := ℝ) atTop (fun (x : ℝ) ↦ rexp x / x ^ n) fun (x : ℝ) ↦ rexp x / x ^ s

Tactic:
filter_upwards [eventually_gt_atTop (0 : ℝ), eventually_ge_atTop (1 : ℝ)] with x hx₀ hx₁

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s : ℝ
n : ℕ
hn : s < (↑n : ℝ)
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
h : x ^ s ≤ x ^ n
⊢ rexp x / x ^ n ≤ rexp x / x ^ s

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s : ℝ
n : ℕ
hn : s < (↑n : ℝ)
x : ℝ
hx₀ : 0 < x
hx₁ : 1 ≤ x
⊢ x ^ s ≤ x ^ n

Tactic:
simpa using rpow_le_rpow_of_exponent_le hx₁ hn.le

Premises used: LT.lt.le, Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s b : ℝ
hb : 0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (b * x) / x ^ s) atTop atTop

Tactic:
((tendsto_rpow_atTop hb).comp (tendsto_exp_div_rpow_atTop (s / b))).congr' ?_

Premises used: tendsto_rpow_atTop, HDiv.hDiv, tendsto_exp_div_rpow_atTop, Filter.Tendsto.comp, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s b : ℝ
hb : 0 < b
refine :
  EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ x ^ b) ∘ fun (x : ℝ) ↦ rexp x / x ^ (s / b)) fun (x : ℝ) ↦
    rexp (b * x) / x ^ s
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (b * x) / x ^ s) atTop atTop

Tactic:
refine ((tendsto_rpow_atTop hb).comp (tendsto_exp_div_rpow_atTop (s / b))).congr' ?_

Premises used: tendsto_rpow_atTop, HDiv.hDiv, tendsto_exp_div_rpow_atTop, Filter.Tendsto.comp, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s b : ℝ
hb : 0 < b
h : ∀ (x : ℝ) (hx₀ : 0 ≤ x), ((fun (x : ℝ) ↦ x ^ b) ∘ fun (x : ℝ) ↦ rexp x / x ^ (s / b)) x = rexp (b * x) / x ^ s
⊢ EventuallyEq (β := ℝ) atTop ((fun (x : ℝ) ↦ x ^ b) ∘ fun (x : ℝ) ↦ rexp x / x ^ (s / b)) fun (x : ℝ) ↦
    rexp (b * x) / x ^ s

Tactic:
filter_upwards [eventually_ge_atTop (0 : ℝ)] with x hx₀

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s b : ℝ
hb : 0 < b
x : ℝ
hx₀ : 0 ≤ x
⊢ ((fun (x : ℝ) ↦ x ^ b) ∘ fun (x : ℝ) ↦ rexp x / x ^ (s / b)) x = rexp (b * x) / x ^ s

Tactic:
simp [Real.div_rpow, (exp_pos x).le, rpow_nonneg, ← Real.rpow_mul, ← exp_mul,
    mul_comm x, hb.ne', *]

Premises used: Real.exp_mul, LT.lt.le, Real.div_rpow, LT.lt.ne', mul_comm, Real.rpow_nonneg, Real.rpow_mul, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s b : ℝ
hb : 0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ s * rexp (-b * x)) atTop (𝓝 0)

Tactic:
(tendsto_exp_mul_div_rpow_atTop s b hb).inv_tendsto_atTop.congr' ?_

Premises used: Filter.Tendsto.inv_tendsto_atTop, Filter.Tendsto.congr', tendsto_exp_mul_div_rpow_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s b : ℝ
hb : 0 < b
refine : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ rexp (b * x) / x ^ s)⁻¹ fun (x : ℝ) ↦ x ^ s * rexp (-b * x)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ s * rexp (-b * x)) atTop (𝓝 0)

Tactic:
refine (tendsto_exp_mul_div_rpow_atTop s b hb).inv_tendsto_atTop.congr' ?_

Premises used: Filter.Tendsto.inv_tendsto_atTop, Filter.Tendsto.congr', tendsto_exp_mul_div_rpow_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s b : ℝ
hb : 0 < b
x : ℝ
⊢ (fun (x : ℝ) ↦ rexp (b * x) / x ^ s)⁻¹ x = x ^ s * rexp (-b * x)

Tactic:
simp [exp_neg, inv_div, div_eq_mul_inv _ (exp _)]

Premises used: Real.exp, div_eq_mul_inv, inv_div, Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
s b : ℝ
hb : 0 < b
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        (fun (x : ℝ) ↦ Eq (α := ℝ) ((fun (x : ℝ) ↦ rexp (b * x) / x ^ s)⁻¹ x) ((fun (x : ℝ) ↦ x ^ s * rexp (-b * x)) x))
          x}
      a
h₁ h₂ : ∀ (x : ℝ), (fun (x : ℝ) ↦ rexp (b * x) / x ^ s)⁻¹ x = x ^ s * rexp (-b * x)
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ rexp (b * x) / x ^ s)⁻¹ fun (x : ℝ) ↦ x ^ s * rexp (-b * x)

Tactic:
filter_upwards with x using by simp [exp_neg, inv_div, div_eq_mul_inv _ (exp _)]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
rw : ∀ (b : ℝ≥0), ∃ (i : ℝ≥0), ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y
⊢ Tendsto (β := ℝ≥0) (fun (x : ℝ≥0) ↦ x ^ y) atTop atTop

Tactic:
rw [Filter.tendsto_atTop_atTop]

Premises used: Filter.tendsto_atTop_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
b : ℝ≥0
obtain : ∀ (c : ℝ) (hc : ∀ (a : ℝ), c ≤ a → (↑b : ℝ) ≤ a ^ y), ∃ (i : ℝ≥0), ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y
⊢ ∃ (i : ℝ≥0), ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y

Tactic:
obtain ⟨c, hc⟩ := tendsto_atTop_atTop.mp (tendsto_rpow_atTop hy) b

Premises used: NNReal.tendsto_rpow_atTop, Filter.tendsto_atTop_atTop, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
b : ℝ≥0
c : ℝ
hc : ∀ (a : ℝ), c ≤ a → (↑b : ℝ) ≤ a ^ y
h : ∀ (a : ℝ≥0), c.toNNReal ≤ a → b ≤ a ^ y
⊢ ∃ (i : ℝ≥0), ∀ (a : ℝ≥0), i ≤ a → b ≤ a ^ y

Tactic:
use c.toNNReal

Premises used: Real.toNNReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
b : ℝ≥0
c : ℝ
hc : ∀ (a : ℝ), c ≤ a → (↑b : ℝ) ≤ a ^ y
a : ℝ≥0
ha : c.toNNReal ≤ a
⊢ b ≤ a ^ y

Tactic:
mod_cast hc a (Real.toNNReal_le_iff_le_coe.mp ha)

Premises used: NNReal.coe_le_coe._simp_1, cast, Iff.mp, Real.toNNReal_le_iff_le_coe, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
b : ℝ≥0
c : ℝ
hc : ∀ (a : ℝ), c ≤ a → (↑b : ℝ) ≤ a ^ y
a : ℝ≥0
ha : c.toNNReal ≤ a
⊢ b ≤ a ^ y

Tactic:
exact mod_cast hc a (Real.toNNReal_le_iff_le_coe.mp ha)

Premises used: Iff.mp, Real.toNNReal_le_iff_le_coe, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
rw : ∀ (x : ℝ≥0), ∀ᶠ (a : ℝ≥0∞) in 𝓝 ∞, (↑x : ℝ≥0∞) < a ^ y
⊢ Tendsto (β := ℝ≥0∞) (fun (x : ℝ≥0∞) ↦ x ^ y) (𝓝 ∞) (𝓝 ∞)

Tactic:
rw [ENNReal.tendsto_nhds_top_iff_nnreal]

Premises used: ENNReal.tendsto_nhds_top_iff_nnreal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
x : ℝ≥0
obtain : ∀ (c : ℝ≥0), True → ∀ (hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x), ∀ᶠ (a : ℝ≥0∞) in 𝓝 ∞, (↑x : ℝ≥0∞) < a ^ y
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ∞, (↑x : ℝ≥0∞) < a ^ y

Tactic:
obtain ⟨c, _, hc⟩ :=
    (atTop_basis_Ioi.tendsto_iff atTop_basis_Ioi).mp (NNReal.tendsto_rpow_atTop hy) x trivial

Premises used: trivial, Filter.HasBasis.tendsto_iff, Filter.atTop_basis_Ioi, NNReal.tendsto_rpow_atTop, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
⊢ Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))

Tactic:
have hc' : Set.Ioi ↑c ∈ 𝓝 (⊤ : ℝ≥0∞) := Ioi_mem_nhds ENNReal.coe_lt_top
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))
h : ∀ (a : ℝ≥0∞) (ha : a ∈ Set.Ioi (↑c : ℝ≥0∞)), (↑x : ℝ≥0∞) < a ^ y
⊢ ∀ᶠ (a : ℝ≥0∞) in 𝓝 ∞, (↑x : ℝ≥0∞) < a ^ y

Tactic:
filter_upwards [hc'] with a ha
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))
a : ℝ≥0∞
ha : a ∈ Set.Ioi (↑c : ℝ≥0∞)
pos : ∀ (ha' : a = ∞), (↑x : ℝ≥0∞) < a ^ y
neg : ∀ (ha' : ¬a = ∞), (↑x : ℝ≥0∞) < a ^ y
⊢ (↑x : ℝ≥0∞) < a ^ y

Tactic:
by_cases ha' : a = ⊤
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))
a : ℝ≥0∞
ha : a ∈ Set.Ioi (↑c : ℝ≥0∞)
ha' : a = ∞
⊢ (↑x : ℝ≥0∞) < a ^ y

Tactic:
simp [ha', hy]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))
a : ℝ≥0∞
ha : a ∈ Set.Ioi (↑c : ℝ≥0∞)
ha' : ¬a = ∞
⊢ a ≠ ∞

Tactic:
ha'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))
a : ℝ≥0∞
ha : a ∈ Set.Ioi (↑c : ℝ≥0∞)
ha' : ¬a = ∞
neg : ∀ (a : ℝ≥0) (ha : (↑a : ℝ≥0∞) ∈ Set.Ioi (↑c : ℝ≥0∞)), (↑x : ℝ≥0∞) < (↑a : ℝ≥0∞) ^ y
⊢ (↑x : ℝ≥0∞) < a ^ y

Tactic:
lift a to ℝ≥0 using ha'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))
a : ℝ≥0
ha : (↑a : ℝ≥0∞) ∈ Set.Ioi (↑c : ℝ≥0∞)
⊢ c < a

Tactic:
simp only [Set.mem_Ioi, coe_lt_coe] at ha hc

Premises used: ENNReal.coe_lt_coe, Set.mem_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc : ∀ x_1 ∈ Set.Ioi c, x_1 ^ y ∈ Set.Ioi x
hc' : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))
a : ℝ≥0
ha : (↑a : ℝ≥0∞) ∈ Set.Ioi (↑c : ℝ≥0∞)
ha₁ : c < a
⊢ ∀ (x_1 : ℝ≥0), c < x_1 → x < x_1 ^ y

Tactic:
simp only [Set.mem_Ioi, coe_lt_coe] at ha hc

Premises used: ENNReal.coe_lt_coe, Set.mem_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc' : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))
a : ℝ≥0
ha : c < a
hc : ∀ (x_1 : ℝ≥0), c < x_1 → x < x_1 ^ y
neg : (↑x : ℝ≥0∞) < (↑(a ^ y) : ℝ≥0∞)
⊢ (↑x : ℝ≥0∞) < (↑a : ℝ≥0∞) ^ y

Tactic:
rw [← ENNReal.coe_rpow_of_nonneg _ hy.le]

Premises used: ENNReal.coe_rpow_of_nonneg, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc' : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))
a : ℝ≥0
ha : c < a
hc : ∀ (x_1 : ℝ≥0), c < x_1 → x < x_1 ^ y
⊢ (↑x : ℝ≥0∞) < (↑(a ^ y) : ℝ≥0∞)

Tactic:
mod_cast hc a ha

Premises used: cast, ENNReal.coe_lt_coe._simp_1, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Goal:
y : ℝ
hy : 0 < y
x c : ℝ≥0
left : True
hc' : Membership.mem (γ := Filter ℝ≥0∞) (𝓝 ∞) (Set.Ioi (↑c : ℝ≥0∞))
a : ℝ≥0
ha : c < a
hc : ∀ (x_1 : ℝ≥0), c < x_1 → x < x_1 ^ y
⊢ (↑x : ℝ≥0∞) < (↑(a ^ y) : ℝ≥0∞)

Tactic:
exact mod_cast hc a ha