awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℝ
s : Set α
h : ContinuousOn f s
⊢ ContinuousOn (Y := ℝ) (fun (y : α) ↦ rexp (f y)) s

Tactic:
fun x hx ↦ (h x hx).rexp

Premises used: ContinuousWithinAt.rexp, ContinuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
inst : TopologicalSpace α
f : α → ℝ
h : Continuous[inst, _] f
⊢ Continuous[inst, _] fun (y : α) ↦ rexp (f y)

Tactic:
continuous_iff_continuousAt.2 fun _ ↦ h.continuousAt.rexp

Premises used: Iff.mpr, Continuous.continuousAt, ContinuousAt.rexp, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
x : ℝ
hx : 0 ≤ rexp x
hy : 0 ≤ rexp (x / 2)
⊢ rexp (x / 2) = √(rexp x)

Tactic:
rw [eq_comm, sqrt_eq_iff_eq_sq, sq, ← exp_add, add_halves]

Premises used: Real.sqrt_eq_iff_eq_sq, add_halves, sq, eq_comm, Real.exp_add
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
x : ℝ
⊢ 0 ≤ rexp x

Tactic:
(exp_pos _).le

Premises used: LT.lt.le, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
x : ℝ
⊢ 0 ≤ rexp x

Tactic:
exact (exp_pos _).le

Premises used: LT.lt.le, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
x : ℝ
⊢ 0 ≤ rexp (x / 2)

Tactic:
(exp_pos _).le

Premises used: LT.lt.le, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
x : ℝ
⊢ 0 ≤ rexp (x / 2)

Tactic:
exact (exp_pos _).le

Premises used: LT.lt.le, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x + 1) atTop atTop

Tactic:
have A : Tendsto (fun x : ℝ => x + 1) atTop atTop :=
    tendsto_atTop_add_const_right atTop 1 tendsto_id
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
A : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x + 1) atTop atTop
⊢ ∀ᶠ (x : ℝ) in atTop, x + 1 ≤ rexp x

Tactic:
have B : ∀ᶠ x in atTop, x + 1 ≤ exp x := eventually_atTop.2 ⟨0, fun x _ => add_one_le_exp x⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
A : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x + 1) atTop atTop
B : ∀ᶠ (x : ℝ) in atTop, x + 1 ≤ rexp x
⊢ Tendsto rexp atTop atTop

Tactic:
tendsto_atTop_mono' atTop B A

Premises used: Filter.atTop, Filter.tendsto_atTop_mono'
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
A : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x + 1) atTop atTop
B : ∀ᶠ (x : ℝ) in atTop, x + 1 ≤ rexp x
⊢ Tendsto rexp atTop atTop

Tactic:
exact tendsto_atTop_mono' atTop B A

Premises used: Filter.atTop, Filter.tendsto_atTop_mono'
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
y : ℝ
⊢ y ≤ rexp (y - 1)

Tactic:
simpa using add_one_le_exp (y - 1)

Premises used: HSub.hSub, OfNat.ofNat, Real.add_one_le_exp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
y : ℝ
⊢ y ≤ rexp (y - 1)

Tactic:
have h_le : y ≤ exp (y - 1) := by simpa using add_one_le_exp (y - 1)
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
y : ℝ
h_le : y ≤ rexp (y - 1)
ha : 0 ≤ rexp (-y)
⊢ y * rexp (-y) ≤ rexp (y - 1) * rexp (-y)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
y : ℝ
h_le : y ≤ rexp (y - 1)
⊢ y * rexp (-y) ≤ rexp (y - 1) * rexp (-y)

Tactic:
have h_mul_le : y * rexp (-y) ≤ rexp (y - 1) * rexp (-y) := by gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
y : ℝ
h_le : y ≤ rexp (y - 1)
h_mul_le : y * rexp (-y) ≤ rexp (y - 1) * rexp (-y)
⊢ y * rexp (-y) ≤ rexp (-1)

Tactic:
simpa [← exp_add, sub_add_eq_add_sub] using h_mul_le

Premises used: sub_add_eq_add_sub, Real.exp_add
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp (-x)) atTop (𝓝 0)

Tactic:
(tendsto_inv_atTop_zero.comp tendsto_exp_atTop).congr fun x => (exp_neg x).symm

Premises used: tendsto_inv_atTop_zero, Real.tendsto_exp_atTop, Filter.Tendsto.congr, Filter.Tendsto.comp, Eq.symm, Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
⊢ Tendsto rexp (𝓝 0) (𝓝 (rexp 0))

Tactic:
continuous_exp.tendsto 0

Premises used: Continuous.tendsto, Real.continuous_exp, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
h : 1 = rexp 0
⊢ Tendsto rexp (𝓝 0) (𝓝 1)

Tactic:
convert! continuous_exp.tendsto 0

Premises used: Continuous.tendsto, Real.continuous_exp, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
⊢ 1 = rexp 0

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
⊢ Tendsto rexp atBot (𝓝 0)

Tactic:
(tendsto_exp_neg_atTop_nhds_zero.comp tendsto_neg_atBot_atTop).congr fun x =>
    congr_arg exp <| neg_neg x

Premises used: Filter.tendsto_neg_atBot_atTop, Real.tendsto_exp_neg_atTop_nhds_zero, neg_neg, Real.exp, congr_arg, Filter.Tendsto.congr, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
⊢ Tendsto rexp atBot (𝓝[>] 0)

Tactic:
tendsto_inf.2 ⟨tendsto_exp_atBot, tendsto_principal.2 <| Eventually.of_forall exp_pos⟩

Premises used: Iff.mpr, Filter.tendsto_inf, nhdsWithin, Filter.Eventually.of_forall, Filter.tendsto_principal, Real.tendsto_exp_atBot, And.intro, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) l fun (x : α) ↦ rexp (f x)

Tactic:
isBoundedUnder_of ⟨0, fun _ => (exp_pos _).le⟩

Premises used: LT.lt.le, Exists.intro, OfNat.ofNat, Filter.isBoundedUnder_of, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
l : Filter α
f : α → ℝ
⊢ (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ rexp (f x)) ↔
    IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l f

Tactic:
exp_monotone.isBoundedUnder_le_comp_iff tendsto_exp_atTop

Premises used: Real.tendsto_exp_atTop, Real.exp_monotone, Real.exp, Monotone.isBoundedUnder_le_comp_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp x / x ^ n) atTop atTop

Tactic:
(atTop_basis_Ioi.tendsto_iff (atTop_basis' 1)).2 fun C hC₁ => ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, Filter.atTop_basis_Ioi, Filter.atTop_basis', OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
refine : ∀ (C : ℝ) (hC₁ : 1 ≤ C), ∃ (ia : ℝ), True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp x / x ^ n) atTop atTop

Tactic:
refine (atTop_basis_Ioi.tendsto_iff (atTop_basis' 1)).2 fun C hC₁ => ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_iff, Filter.atTop_basis_Ioi, Filter.atTop_basis', OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
⊢ 0 < C

Tactic:
have hC₀ : 0 < C := zero_lt_one.trans_le hC₁
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
⊢ 0 < (rexp 1 * C)⁻¹

Tactic:
have : 0 < (exp 1 * C)⁻¹ := inv_pos.2 (mul_pos (exp_pos _) hC₀)
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
⊢ ∃ (N : ℕ), ∀ k ≥ N, HPow.hPow (α := ℝ) (↑k : ℝ) n / rexp 1 ^ k < (rexp 1 * C)⁻¹

Tactic:
eventually_atTop.1
      ((tendsto_pow_const_div_const_pow_of_one_lt n (one_lt_exp_iff.2 zero_lt_one)).eventually
        (gt_mem_nhds this))

Premises used: Iff.mpr, gt_mem_nhds, zero_lt_one, Real.one_lt_exp_iff, Filter.Tendsto.eventually, Iff.mp, tendsto_pow_const_div_const_pow_of_one_lt, Filter.eventually_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
obtain :
  ∀ (N : ℕ) (hN : ∀ k ≥ N, HPow.hPow (α := ℝ) (↑k : ℝ) n / rexp 1 ^ k < (rexp 1 * C)⁻¹),
    ∃ (ia : ℝ), True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C
⊢ ∃ (ia : ℝ), True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C

Tactic:
obtain ⟨N, hN⟩ : ∃ N : ℕ, ∀ k ≥ N, (↑k : ℝ) ^ n / exp 1 ^ k < (exp 1 * C)⁻¹ :=
    eventually_atTop.1
      ((tendsto_pow_const_div_const_pow_of_one_lt n (one_lt_exp_iff.2 zero_lt_one)).eventually
        (gt_mem_nhds this))

Premises used: Iff.mpr, gt_mem_nhds, HMul.hMul, Real.exp, zero_lt_one, Real.one_lt_exp_iff, Filter.Tendsto.eventually, Iff.mp, tendsto_pow_const_div_const_pow_of_one_lt, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, HPow.hPow (α := ℝ) (↑k : ℝ) n / rexp 1 ^ k < (rexp 1 * C)⁻¹
⊢ ∀ k ≥ N, HPow.hPow (α := ℝ) (↑k : ℝ) n < rexp (↑k : ℝ) / (rexp 1 * C)

Tactic:
simp only [← exp_nat_mul, mul_one, div_lt_iff₀, exp_pos, ← div_eq_inv_mul] at hN

Premises used: div_lt_iff₀, mul_one, div_eq_inv_mul, Real.exp_nat_mul, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, HPow.hPow (α := ℝ) (↑k : ℝ) n < rexp (↑k : ℝ) / (rexp 1 * C)
⊢ ∃ (ia : ℝ), True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C

Tactic:
⟨N, trivial, fun x hx => ?_⟩

Premises used: trivial, Nat.cast, And.intro, Exists.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, HPow.hPow (α := ℝ) (↑k : ℝ) n < rexp (↑k : ℝ) / (rexp 1 * C)
refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Set.Ioi (↑N : ℝ)) x), rexp x / x ^ n ∈ Set.Ici C
⊢ ∃ (ia : ℝ), True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C

Tactic:
refine ⟨N, trivial, fun x hx => ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, HPow.hPow (α := ℝ) (↑k : ℝ) n < rexp (↑k : ℝ) / (rexp 1 * C)
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Set.Ioi (↑N : ℝ)) x
⊢ (↑N : ℝ) < x

Tactic:
rw [Set.mem_Ioi] at hx

Premises used: Set.mem_Ioi
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, HPow.hPow (α := ℝ) (↑k : ℝ) n < rexp (↑k : ℝ) / (rexp 1 * C)
x : ℝ
hx : (↑N : ℝ) < x
⊢ 0 < x

Tactic:
have hx₀ : 0 < x := (Nat.cast_nonneg N).trans_lt hx
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, HPow.hPow (α := ℝ) (↑k : ℝ) n < rexp (↑k : ℝ) / (rexp 1 * C)
x : ℝ
hx : (↑N : ℝ) < x
hx₀ : 0 < x
rw : x ^ n ≤ rexp x / C
⊢ rexp x / x ^ n ∈ Set.Ici C

Tactic:
rw [Set.mem_Ici, le_div_iff₀ (pow_pos hx₀ _), ← le_div_iff₀' hC₀]

Premises used: pow_pos, le_div_iff₀', Set.mem_Ici, le_div_iff₀
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, HPow.hPow (α := ℝ) (↑k : ℝ) n < rexp (↑k : ℝ) / (rexp 1 * C)
x : ℝ
hx : (↑N : ℝ) < x
hx₀ : 0 < x
hab : x ≤ (↑⌈x⌉₊ : ℝ)
⊢ x ^ n ≤ HPow.hPow (α := ℝ) (↑⌈x⌉₊ : ℝ) n

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, HPow.hPow (α := ℝ) (↑k : ℝ) n < rexp (↑k : ℝ) / (rexp 1 * C)
x : ℝ
hx : (↑N : ℝ) < x
hx₀ : 0 < x
⊢ x ≤ (↑⌈x⌉₊ : ℝ)

Tactic:
Nat.le_ceil _

Premises used: Nat.le_ceil
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, HPow.hPow (α := ℝ) (↑k : ℝ) n < rexp (↑k : ℝ) / (rexp 1 * C)
x : ℝ
hx : (↑N : ℝ) < x
hx₀ : 0 < x
⊢ x ≤ (↑⌈x⌉₊ : ℝ)

Tactic:
exact Nat.le_ceil _

Premises used: Nat.le_ceil
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, HPow.hPow (α := ℝ) (↑k : ℝ) n < rexp (↑k : ℝ) / (rexp 1 * C)
x : ℝ
hx : (↑N : ℝ) < x
hx₀ : 0 < x
⊢ HPow.hPow (α := ℝ) (↑⌈x⌉₊ : ℝ) n ≤ rexp (↑⌈x⌉₊ : ℝ) / (rexp 1 * C)

Tactic:
mod_cast (hN _ (Nat.lt_ceil.2 hx).le).le

Premises used: Iff.mpr, HMul.hMul, congrArg, cast, HDiv.hDiv, LT.lt.le, LE.le, Real.exp, Nat.cast, HPow.hPow, Nat.ceil, Nat.lt_ceil, congrFun', OfNat.ofNat, Eq.symm, Nat.cast_one, Eq.trans, Nat.cast_pow._simp_1
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, HPow.hPow (α := ℝ) (↑k : ℝ) n < rexp (↑k : ℝ) / (rexp 1 * C)
x : ℝ
hx : (↑N : ℝ) < x
hx₀ : 0 < x
hab : (↑⌈x⌉₊ : ℝ) ≤ x + 1
⊢ rexp (↑⌈x⌉₊ : ℝ) / (rexp 1 * C) ≤ rexp (x + 1) / (rexp 1 * C)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, HPow.hPow (α := ℝ) (↑k : ℝ) n < rexp (↑k : ℝ) / (rexp 1 * C)
x : ℝ
hx : (↑N : ℝ) < x
hx₀ : 0 < x
⊢ (↑⌈x⌉₊ : ℝ) ≤ x + 1

Tactic:
(Nat.ceil_lt_add_one hx₀.le).le

Premises used: Nat.ceil_lt_add_one, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, HPow.hPow (α := ℝ) (↑k : ℝ) n < rexp (↑k : ℝ) / (rexp 1 * C)
x : ℝ
hx : (↑N : ℝ) < x
hx₀ : 0 < x
⊢ (↑⌈x⌉₊ : ℝ) ≤ x + 1

Tactic:
exact (Nat.ceil_lt_add_one hx₀.le).le

Premises used: Nat.ceil_lt_add_one, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, HPow.hPow (α := ℝ) (↑k : ℝ) n < rexp (↑k : ℝ) / (rexp 1 * C)
x : ℝ
hx : (↑N : ℝ) < x
hx₀ : 0 < x
rw : rexp (1 + x) / (rexp 1 * C) = rexp x / C
rw₁ : rexp 1 * rexp x / (rexp 1 * C) = rexp x / C
rw₂ rw₃ : rexp x / C = rexp x / C
⊢ rexp (x + 1) / (rexp 1 * C) = rexp x / C

Tactic:
rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']

Premises used: add_comm, LT.lt.ne', mul_div_mul_left, Real.exp_add, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
N : ℕ
hN : ∀ k ≥ N, HPow.hPow (α := ℝ) (↑k : ℝ) n < rexp (↑k : ℝ) / (rexp 1 * C)
x : ℝ
hx : (↑N : ℝ) < x
hx₀ : 0 < x
x₁ : x ^ n ≤ HPow.hPow (α := ℝ) (↑⌈x⌉₊ : ℝ) n
x₂ : rexp (↑⌈x⌉₊ : ℝ) / (rexp 1 * C) ≤ rexp (x + 1) / (rexp 1 * C)
x₃ : rexp (x + 1) / (rexp 1 * C) = rexp x / C
⊢ x ^ n ≤ rexp x / C

Tactic:
calc
    x ^ n ≤ ⌈x⌉₊ ^ n := by gcongr; exact Nat.le_ceil _
    _ ≤ exp ⌈x⌉₊ / (exp 1 * C) := mod_cast (hN _ (Nat.lt_ceil.2 hx).le).le
    _ ≤ exp (x + 1) / (exp 1 * C) := by gcongr; exact (Nat.ceil_lt_add_one hx₀.le).le
    _ = exp x / C := by rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']

Premises used: Iff.mpr, HMul.hMul, LT.lt.le, Real.exp, Nat.cast, HAdd.hAdd, Nat.ceil, Nat.lt_ceil, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
n : ℕ
x : ℝ
rw : (rexp x / x ^ n)⁻¹ = x ^ n * rexp (-x)
rw₁ : 1 / (rexp x / x ^ n) = x ^ n * rexp (-x)
rw₂ : 1 * x ^ n / rexp x = x ^ n * rexp (-x)
rw₃ : x ^ n / rexp x = x ^ n * rexp (-x)
rw₄ : x ^ n * (rexp x)⁻¹ = x ^ n * rexp (-x)
rw₅ rw₆ : x ^ n * (rexp x)⁻¹ = x ^ n * (rexp x)⁻¹
⊢ ((fun (r : ℝ) ↦ r⁻¹) ∘ fun (x : ℝ) ↦ rexp x / x ^ n) x = x ^ n * rexp (-x)

Tactic:
rw [comp_apply, inv_eq_one_div, div_div_eq_mul_div, one_mul, div_eq_mul_inv, exp_neg]

Premises used: div_div_eq_mul_div, inv_eq_one_div, div_eq_mul_inv, Function.comp_apply, Real.exp_neg, one_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
b c : ℝ
n : ℕ
hb : 0 < b
inl : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (b * rexp x + c) / HPow.hPow (β := ℕ) x 0) atTop atTop
inr : ∀ (hn : n ≠ 0), Tendsto (β := ℝ) (fun (x : ℝ) ↦ (b * rexp x + c) / x ^ n) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (b * rexp x + c) / x ^ n) atTop atTop

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
b c : ℝ
hb : 0 < b
inl : Tendsto (β := ℝ) (fun (x : ℝ) ↦ b * rexp x + c) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (b * rexp x + c) / HPow.hPow (β := ℕ) x 0) atTop atTop

Tactic:
simp only [pow_zero, div_one]

Premises used: pow_zero, div_one
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
b c : ℝ
hb : 0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b * rexp x + c) atTop atTop

Tactic:
(tendsto_exp_atTop.const_mul_atTop hb).atTop_add tendsto_const_nhds

Premises used: Filter.Tendsto.const_mul_atTop, Real.tendsto_exp_atTop, tendsto_const_nhds, Filter.Tendsto.atTop_add
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
b c : ℝ
hb : 0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b * rexp x + c) atTop atTop

Tactic:
exact (tendsto_exp_atTop.const_mul_atTop hb).atTop_add tendsto_const_nhds

Premises used: Filter.Tendsto.const_mul_atTop, Real.tendsto_exp_atTop, tendsto_const_nhds, Filter.Tendsto.atTop_add
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
inr : Tendsto (β := ℝ) (fun (x : ℝ) ↦ b * (rexp x / x ^ n) + c / x ^ n) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (b * rexp x + c) / x ^ n) atTop atTop

Tactic:
simp only [add_div, mul_div_assoc]

Premises used: mul_div_assoc, add_div
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b * (rexp x / x ^ n) + c / x ^ n) atTop atTop

Tactic:
((tendsto_exp_div_pow_atTop n).const_mul_atTop hb).atTop_add
      (tendsto_const_nhds.div_atTop (tendsto_pow_atTop hn))

Premises used: Filter.Tendsto.div_atTop, Filter.Tendsto.const_mul_atTop, Real.tendsto_exp_div_pow_atTop, tendsto_const_nhds, Filter.Tendsto.atTop_add, Filter.tendsto_pow_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ b * (rexp x / x ^ n) + c / x ^ n) atTop atTop

Tactic:
exact
    ((tendsto_exp_div_pow_atTop n).const_mul_atTop hb).atTop_add
      (tendsto_const_nhds.div_atTop (tendsto_pow_atTop hn))

Premises used: Filter.Tendsto.div_atTop, Filter.Tendsto.const_mul_atTop, Real.tendsto_exp_div_pow_atTop, tendsto_const_nhds, Filter.Tendsto.atTop_add, Filter.tendsto_pow_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
⊢ Tendsto (α := ℝ) (β := ℝ) (fun (x : ℝ) ↦ (b' * rexp x + c') / x ^ n)⁻¹ atTop (𝓝 0)

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

Premises used: Real.tendsto_mul_exp_add_div_pow_atTop, Filter.Tendsto.inv_tendsto_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
h₁ : Eq (α := ℝ → ℝ) (fun (x : ℝ) ↦ x ^ n / (b' * rexp x + c')) (fun (x : ℝ) ↦ (b' * rexp x + c') / x ^ n)⁻¹
⊢ 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

Premises used: Real.tendsto_mul_exp_add_div_pow_atTop, Filter.Tendsto.inv_tendsto_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
h₁ : ∀ (x : ℝ), x ^ n / (b' * rexp x + c') = (fun (x : ℝ) ↦ (b' * rexp x + c') / x ^ n)⁻¹ x
⊢ Eq (α := ℝ → ℝ) (fun (x : ℝ) ↦ x ^ n / (b' * rexp x + c')) (fun (x : ℝ) ↦ (b' * rexp x + c') / x ^ n)⁻¹

Tactic:
ext x
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
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
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
b c : ℝ
n : ℕ
hb : 0 ≠ b
⊢ ∀ (d e : ℝ), 0 < d → Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (d * rexp x + e)) 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
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
inl : ∀ (h : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (b * rexp x + c)) atTop (𝓝 0)
inr : ∀ (h : b < 0), Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (b * rexp x + c)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (b * rexp x + c)) atTop (𝓝 0)

Tactic:
rcases lt_or_gt_of_ne hb with h | h

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
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:
H b c h
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
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
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ -(x ^ n / (-b * rexp x + -c))) atTop (𝓝 (-0))

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

Premises used: Iff.mpr, Filter.Tendsto.neg, neg_pos, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
h₁ : Eq (α := ℝ → ℝ) (fun (x : ℝ) ↦ x ^ n / (b * rexp x + c)) fun (x : ℝ) ↦ -(x ^ n / (-b * rexp x + -c))
h₂ : Eq (α := Filter ℝ) (𝓝 0) (𝓝 (-0))
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (b * rexp x + c)) atTop (𝓝 0)

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

Premises used: Iff.mpr, Filter.Tendsto.neg, neg_pos, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
h₁ : ∀ (x : ℝ), x ^ n / (b * rexp x + c) = -(x ^ n / (-b * rexp x + -c))
⊢ Eq (α := ℝ → ℝ) (fun (x : ℝ) ↦ x ^ n / (b * rexp x + c)) fun (x : ℝ) ↦ -(x ^ n / (-b * rexp x + -c))

Tactic:
ext x
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
x : ℝ
h₁ : x ^ n / (b * rexp x + c) = -(x ^ n / (-(b * rexp x) + -c))
⊢ x ^ n / (b * rexp x + c) = -(x ^ n / (-b * rexp x + -c))

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
x : ℝ
h₁ : x ^ n / (b * rexp x + c) = -(x ^ n / -(b * rexp x + c))
h₂ : x ^ n / (b * rexp x + c) = - -(x ^ n / (b * rexp x + c))
h₃ h₄ : x ^ n / (b * rexp x + c) = x ^ n / (b * rexp x + c)
⊢ x ^ n / (b * rexp x + c) = -(x ^ n / (-(b * rexp x) + -c))

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

Premises used: HMul.hMul, neg_add, neg_neg, Real.exp, div_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
h : b < 0
h₁ h₂ : Eq (α := Filter ℝ) (𝓝 0) (𝓝 0)
⊢ Eq (α := Filter ℝ) (𝓝 0) (𝓝 (-0))

Tactic:
rw [neg_zero]

Premises used: neg_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
x y z : ℝ
l : Filter α
rw :
  Tendsto (β := ℝ)
    (fun (x : ℝ) ↦ (↑(Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) (rexp x) ⋯) : ℝ)) atTop
    atTop
⊢ Tendsto (β := { x : ℝ // Membership.mem (γ := Set ℝ) (Set.Ioi 0) x })
    (fun (x : ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) (rexp x) ⋯) atTop atTop

Tactic:
rw [tendsto_Ioi_atTop]

Premises used: Filter.tendsto_Ioi_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Tendsto (β := ℝ)
    (fun (x : ℝ) ↦ (↑(Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) (rexp x) ⋯) : ℝ)) atTop
    atTop

Tactic:
simp only [tendsto_exp_atTop]

Premises used: Real.tendsto_exp_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
α : Type u_1
x y z : ℝ
l : Filter α
⊢ Tendsto (β := { x : ℝ // Membership.mem (γ := Set ℝ) (Set.Ioi 0) x })
    (fun (x : ℝ) ↦ Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) (rexp x) ⋯) atBot atBot

Tactic:
simp [tendsto_exp_atBot_nhdsGT]

Premises used: Real.tendsto_exp_atBot_nhdsGT
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
x : ℝ
⊢ (↑((expOrderIso : (a : ℝ) → (↑(Set.Ioi 0) : Type)) x) : ℝ) = rexp x

Tactic:
rfl

Premises used: Real.exp, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Exp
Goal:
⊢ comp (β := (↑(Set.Ioi 0) : Type)) (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x))
      (⇑expOrderIso : (a : ℝ) → (↑(Set.Ioi 0) : Type)) =
    rexp

Tactic:
rfl

Premises used: Real.exp, rfl