awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
a ε : ℝ
hε : ε > 0
this_1 : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
hδ : δ > 0 ∧ ∀ ⦃y : ℂ⦄, dist y 0 < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
x : ℂ
h : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} x
y : ℂ
hy : Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ a} y
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
hya : ‖cexp y‖ ≤ Real.exp a
⊢ ‖(cexp (x - y) - 1) * cexp y‖ < ε
have simp : ∀ (hε : 0 < ε) (hδ : 0 < δ ∧ ∀ ⦃y : ℂ⦄, ‖y‖ < δ → dist (cexp y) 1 < ε / (2 * Real.exp a))
  (hya : Real.exp y.re ≤ Real.exp a), ‖cexp (x - y) - 1‖ * Real.exp y.re < ε
Tactic: simp only [gt_iff_lt, dist_zero_right, Set.mem_setOf_eq, norm_mul, Complex.norm_exp] at *
Cleared hypotheses: hε, hδ, hya
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
a ε : ℝ
this_1 : ∀ (a : ℂ) (ε : ℝ), 0 < ε → ∀ᶠ (x : ℂ) in 𝓝 a, dist (cexp x) (cexp a) < ε
ha : 0 < ε / (2 * Real.exp a)
δ : ℝ
x : ℂ
h : x.re ≤ a
y : ℂ
hy : y.re ≤ a
hxy : ‖x - y‖ < δ
h3 : ‖cexp (x - y) - 1‖ < ε / (2 * Real.exp a)
this : cexp x - cexp y = cexp y * (cexp (x - y) - 1)
hε : 0 < ε
hδ : 0 < δ ∧ ∀ ⦃y : ℂ⦄, ‖y‖ < δ → dist (cexp y) 1 < ε / (2 * Real.exp a)
hya : Real.exp y.re ≤ Real.exp a
⊢ ‖cexp (x - y) - 1‖ * Real.exp y.re < ε
have apply : ε / (2 * Real.exp a) * Real.exp a < ε
Tactic: apply lt_of_le_of_lt (mul_le_mul h3.le hya (Real.exp_nonneg y.re) ha.le)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
Goal:
n : ℕ
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : ℝ) ↦ rexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℝ)) fun (x : ℝ) ↦ x ^ n
have this : IsBigO (E := ℂ) (F := ℂ) (𝓝 0)
  ((fun (x : ℂ) ↦ Complex.exp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℂ)) ∘ Complex.ofReal)
  ((fun (x : ℂ) ↦ x ^ n) ∘ Complex.ofReal)
Tactic: have := (Complex.exp_sub_sum_range_isBigO_pow n).comp_tendsto
    (Complex.continuous_ofReal.tendsto' 0 0 rfl)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
n : ℕ
this :
  IsBigO (E := ℂ) (F := ℂ) (𝓝 0) (fun (x : ℝ) ↦ Complex.exp (↑x : ℂ) - ∑ i ∈ Finset.range n, (↑x : ℂ) ^ i / (↑i ! : ℂ))
    fun (x : ℝ) ↦ (↑x : ℂ) ^ n
⊢ IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : ℝ) ↦ rexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℝ)) fun (x : ℝ) ↦ x ^ n
have norm_cast : ∀
  (this :
    IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : ℝ) ↦ rexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℝ)) fun (x : ℝ) ↦
      x ^ n),
  IsBigO (E := ℝ) (F := ℝ) (𝓝 0) (fun (x : ℝ) ↦ rexp x - ∑ i ∈ Finset.range n, x ^ i / (↑i ! : ℝ)) fun (x : ℝ) ↦ x ^ n
Tactic: norm_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
x : ℝ
⊢ rexp (x / 2) = √(rexp x)
have hx : 0 ≤ rexp x
Tactic: rw [eq_comm, sqrt_eq_iff_eq_sq, sq, ← exp_add, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
x : ℝ
hx : 0 ≤ rexp x
⊢ rexp (x / 2) = √(rexp x)
have hy : 0 ≤ rexp (x / 2)
Tactic: rw [eq_comm, sqrt_eq_iff_eq_sq, sq, ← exp_add, add_halves]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
Goal:
⊢ Tendsto rexp atTop atTop
have A : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
Goal:
A : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x + 1) atTop atTop
⊢ Tendsto rexp atTop atTop
have B : ∀ᶠ (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⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
Goal:
y : ℝ
⊢ y * rexp (-y) ≤ rexp (-1)
have h_le : y ≤ rexp (y - 1)
Tactic: have h_le : y ≤ exp (y - 1) := by simpa using add_one_le_exp (y - 1)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
y : ℝ
h_le : y ≤ rexp (y - 1)
⊢ y * rexp (-y) ≤ rexp (y - 1) * rexp (-y)
have ha : 0 ≤ rexp (-y)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
Goal:
y : ℝ
h_le : y ≤ rexp (y - 1)
⊢ y * rexp (-y) ≤ rexp (-1)
have h_mul_le : y * rexp (-y) ≤ rexp (y - 1) * rexp (-y)
Tactic: have h_mul_le : y * rexp (-y) ≤ rexp (y - 1) * rexp (-y) := by gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
⊢ Tendsto rexp (𝓝 0) (𝓝 1)
have h : 1 = rexp 0
Tactic: convert! continuous_exp.tendsto 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
n : ℕ
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ rexp x / x ^ n) atTop atTop
have refine : ∀ (C : ℝ) (hC₁ : 1 ≤ C), ∃ (ia : ℝ), True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C
Tactic: refine (atTop_basis_Ioi.tendsto_iff (atTop_basis' 1)).2 fun C hC₁ => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
⊢ ∃ (ia : ℝ), True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C
have hC₀ : 0 < C
Tactic: have hC₀ : 0 < C := zero_lt_one.trans_le hC₁
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
⊢ ∃ (ia : ℝ), True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C
have this : 0 < (rexp 1 * C)⁻¹
Tactic: have : 0 < (exp 1 * C)⁻¹ := inv_pos.2 (mul_pos (exp_pos _) hC₀)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
n : ℕ
C : ℝ
hC₁ : 1 ≤ C
hC₀ : 0 < C
this : 0 < (rexp 1 * C)⁻¹
⊢ ∃ (ia : ℝ), True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C
have 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
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))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
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)⁻¹
⊢ ∃ (ia : ℝ), True ∧ ∀ x ∈ Set.Ioi ia, rexp x / x ^ n ∈ Set.Ici C
have hN₁ : ∀ 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
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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
have refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Set.Ioi (↑N : ℝ)) x), rexp x / x ^ n ∈ Set.Ici C
Tactic: refine ⟨N, trivial, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
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
⊢ rexp x / x ^ n ∈ Set.Ici C
have hx₁ : (↑N : ℝ) < x
Tactic: rw [Set.mem_Ioi] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
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
⊢ rexp x / x ^ n ∈ Set.Ici C
have hx₀ : 0 < x
Tactic: have hx₀ : 0 < x := (Nat.cast_nonneg N).trans_lt hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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
⊢ rexp x / x ^ n ∈ Set.Ici C
have rw : x ^ n ≤ rexp x / C
Tactic: rw [Set.mem_Ici, le_div_iff₀ (pow_pos hx₀ _), ← le_div_iff₀' hC₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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 ^ n ≤ HPow.hPow (α := ℝ) (↑⌈x⌉₊ : ℝ) n
have hab : x ≤ (↑⌈x⌉₊ : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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
⊢ rexp (↑⌈x⌉₊ : ℝ) / (rexp 1 * C) ≤ rexp (x + 1) / (rexp 1 * C)
have hab : (↑⌈x⌉₊ : ℝ) ≤ x + 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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
⊢ rexp (x + 1) / (rexp 1 * C) = rexp x / C
have rw : rexp (1 + x) / (rexp 1 * C) = rexp x / C
Tactic: rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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
⊢ rexp (x + 1) / (rexp 1 * C) = rexp x / C
have rw₁ : rexp 1 * rexp x / (rexp 1 * C) = rexp x / C
Tactic: rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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
⊢ rexp (x + 1) / (rexp 1 * C) = rexp x / C
have rw₂ : rexp x / C = rexp x / C
Tactic: rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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 ^ n ≤ rexp x / C
have x₁ : x ^ n ≤ HPow.hPow (α := ℝ) (↑⌈x⌉₊ : ℝ) n
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']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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 ^ n ≤ rexp x / C
have x₂ : rexp (↑⌈x⌉₊ : ℝ) / (rexp 1 * C) ≤ rexp (x + 1) / (rexp 1 * 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']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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 ^ n ≤ rexp x / C
have x₃ : rexp (x + 1) / (rexp 1 * C) = 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']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
n : ℕ
x : ℝ
⊢ ((fun (r : ℝ) ↦ r⁻¹) ∘ fun (x : ℝ) ↦ rexp x / x ^ n) x = x ^ n * rexp (-x)
have rw : (rexp x / x ^ n)⁻¹ = 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
n : ℕ
x : ℝ
rw : (rexp x / x ^ n)⁻¹ = x ^ n * rexp (-x)
⊢ ((fun (r : ℝ) ↦ r⁻¹) ∘ fun (x : ℝ) ↦ rexp x / x ^ n) x = x ^ n * rexp (-x)
have rw₁ : 1 / (rexp x / x ^ n) = 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
n : ℕ
x : ℝ
rw : (rexp x / x ^ n)⁻¹ = x ^ n * rexp (-x)
rw₁ : 1 / (rexp x / x ^ n) = x ^ n * rexp (-x)
⊢ ((fun (r : ℝ) ↦ r⁻¹) ∘ fun (x : ℝ) ↦ rexp x / x ^ n) x = x ^ n * rexp (-x)
have rw₂ : 1 * x ^ n / rexp 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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)
⊢ ((fun (r : ℝ) ↦ r⁻¹) ∘ fun (x : ℝ) ↦ rexp x / x ^ n) x = x ^ n * rexp (-x)
have rw₃ : x ^ n / rexp 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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)
⊢ ((fun (r : ℝ) ↦ r⁻¹) ∘ fun (x : ℝ) ↦ rexp x / x ^ n) x = x ^ n * rexp (-x)
have rw₄ : x ^ n * (rexp 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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)
⊢ ((fun (r : ℝ) ↦ r⁻¹) ∘ fun (x : ℝ) ↦ rexp x / x ^ n) x = x ^ n * rexp (-x)
have rw₅ : x ^ n * (rexp 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
b c : ℝ
n : ℕ
hb : 0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (b * rexp x + c) / x ^ n) atTop atTop
have inl : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (b * rexp x + c) / HPow.hPow (β := ℕ) x 0) atTop atTop
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
b c : ℝ
n : ℕ
hb : 0 < b
inl : Tendsto (β := ℝ) (fun (x : ℝ) ↦ (b * rexp x + c) / HPow.hPow (β := ℕ) x 0) atTop atTop
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (b * rexp x + c) / x ^ n) atTop atTop
have inr : ∀ (hn : n ≠ 0), Tendsto (β := ℝ) (fun (x : ℝ) ↦ (b * rexp x + c) / x ^ n) atTop atTop
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
b c : ℝ
hb : 0 < b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (b * rexp x + c) / HPow.hPow (β := ℕ) x 0) atTop atTop
have inl : Tendsto (β := ℝ) (fun (x : ℝ) ↦ b * rexp x + c) atTop atTop
Tactic: simp only [pow_zero, div_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
b c : ℝ
n : ℕ
hb : 0 < b
hn : n ≠ 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ (b * rexp x + c) / x ^ n) atTop atTop
have inr : Tendsto (β := ℝ) (fun (x : ℝ) ↦ b * (rexp x / x ^ n) + c / x ^ n) atTop atTop
Tactic: simp only [add_div, mul_div_assoc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (b' * rexp x + c')) atTop (𝓝 0)
have h₁ : Eq (α := ℝ → ℝ) (fun (x : ℝ) ↦ x ^ n / (b' * rexp x + c')) (fun (x : ℝ) ↦ (b' * rexp x + c') / x ^ n)⁻¹
Tactic: convert! (tendsto_mul_exp_add_div_pow_atTop b' c' n h).inv_tendsto_atTop using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
b c : ℝ
n : ℕ
hb : 0 ≠ b
b' c' : ℝ
h : 0 < b'
⊢ Eq (α := ℝ → ℝ) (fun (x : ℝ) ↦ x ^ n / (b' * rexp x + c')) (fun (x : ℝ) ↦ (b' * rexp x + c') / x ^ n)⁻¹
have h₁ : ∀ (x : ℝ), x ^ n / (b' * rexp x + c') = (fun (x : ℝ) ↦ (b' * rexp x + c') / x ^ n)⁻¹ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (hypothesis)
Goal:
b c : ℝ
n : ℕ
hb : 0 ≠ b
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (b * rexp x + c)) atTop (𝓝 0)
have H : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
b c : ℝ
n : ℕ
hb : 0 ≠ b
H : ∀ (d e : ℝ), 0 < d → Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (d * rexp x + e)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (b * rexp x + c)) atTop (𝓝 0)
have inl : ∀ (h : 0 < b), Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (b * rexp x + c)) atTop (𝓝 0)
Tactic: rcases lt_or_gt_of_ne hb with h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (b * rexp x + c)) atTop (𝓝 0)
have inr : ∀ (h : b < 0), Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (b * rexp x + c)) atTop (𝓝 0)
Tactic: rcases lt_or_gt_of_ne hb with h | h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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)
have h₁ : Eq (α := ℝ → ℝ) (fun (x : ℝ) ↦ x ^ n / (b * rexp x + c)) fun (x : ℝ) ↦ -(x ^ n / (-b * rexp x + -c))
Tactic: convert! (H (-b) (-c) (neg_pos.mpr h)).neg using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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))
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x ^ n / (b * rexp x + c)) atTop (𝓝 0)
have h₂ : Eq (α := Filter ℝ) (𝓝 0) (𝓝 (-0))
Tactic: convert! (H (-b) (-c) (neg_pos.mpr h)).neg using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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
⊢ Eq (α := ℝ → ℝ) (fun (x : ℝ) ↦ x ^ n / (b * rexp x + c)) fun (x : ℝ) ↦ -(x ^ n / (-b * rexp x + -c))
have h₁ : ∀ (x : ℝ), x ^ n / (b * rexp x + c) = -(x ^ n / (-b * rexp x + -c))
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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 : ℝ
⊢ x ^ n / (b * rexp x + c) = -(x ^ n / (-b * rexp x + -c))
have h₁ : x ^ n / (b * rexp x + c) = -(x ^ n / (-(b * rexp x) + -c))
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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 : ℝ
⊢ x ^ n / (b * rexp x + c) = -(x ^ n / (-(b * rexp x) + -c))
have h₁ : x ^ n / (b * rexp x + c) = -(x ^ n / -(b * rexp x + c))
Tactic: rw [← neg_add (b * exp x) c, div_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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))
have h₂ : x ^ n / (b * rexp x + c) = - -(x ^ n / (b * rexp x + c))
Tactic: rw [← neg_add (b * exp x) c, div_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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))
⊢ x ^ n / (b * rexp x + c) = -(x ^ n / (-(b * rexp x) + -c))
have h₃ : x ^ n / (b * rexp x + c) = x ^ n / (b * rexp x + c)
Tactic: rw [← neg_add (b * exp x) c, div_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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
⊢ Eq (α := Filter ℝ) (𝓝 0) (𝓝 (-0))
have h₁ : Eq (α := Filter ℝ) (𝓝 0) (𝓝 0)
Tactic: rw [neg_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
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) ⋯) atTop atTop
have rw : Tendsto (β := ℝ)
  (fun (x : ℝ) ↦ (↑(Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x) (rexp x) sorry) : ℝ)) atTop
  atTop
Tactic: rw [tendsto_Ioi_atTop]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
⊢ Set.range rexp = Set.Ioi 0
have rw : Eq (α := Set ℝ)
  (Set.range (ι := ℝ)
    (comp (β := (↑(Set.Ioi 0) : Type)) (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x))
      (⇑expOrderIso : (a : ℝ) → (↑(Set.Ioi 0) : Type))))
  (Set.Ioi 0)
Tactic: rw [← coe_comp_expOrderIso, range_comp, expOrderIso.range_eq, image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
rw :
  Eq (α := Set ℝ)
    (Set.range (ι := ℝ)
      (comp (β := (↑(Set.Ioi 0) : Type)) (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x))
        (⇑expOrderIso : (a : ℝ) → (↑(Set.Ioi 0) : Type))))
    (Set.Ioi 0)
⊢ Set.range rexp = Set.Ioi 0
have rw₁ : Eq (α := Set ℝ)
  (Set.image (α := (↑(Set.Ioi 0) : Type)) (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x))
    (Set.range (ι := ℝ) (⇑expOrderIso : (a : ℝ) → (↑(Set.Ioi 0) : Type))))
  (Set.Ioi 0)
Tactic: rw [← coe_comp_expOrderIso, range_comp, expOrderIso.range_eq, image_univ, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exp (goal)
Goal:
rw :
  Eq (α := Set ℝ)
    (Set.range (ι := ℝ)
      (comp (β := (↑(Set.Ioi 0) : Type)) (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x))
        (⇑expOrderIso : (a : ℝ) → (↑(Set.Ioi 0) : Type))))
    (Set.Ioi 0)
rw₁ :
  Eq (α := Set ℝ)
    (Set.image (α := (↑(Set.Ioi 0) : Type)) (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x))
      (Set.range (ι := ℝ) (⇑expOrderIso : (a : ℝ) → (↑(Set.Ioi 0) : Type))))
    (Set.Ioi 0)
⊢ Set.range rexp = Set.Ioi 0
have rw₂ : Eq (α := Set ℝ)
  (Set.image (α := (↑(Set.Ioi 0) : Type)) (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x))
    Set.univ)
  (Set.Ioi 0)
Tactic: rw [← coe_comp_expOrderIso, range_comp, expOrderIso.range_eq, image_univ, Subtype.range_coe]