awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2))
    fun (x : ℝ) ↦ p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / HPow.hPow (β := ℕ) (log x) 2
have h : ∀ (x : ℝ) (hx : 0 < x),
  p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) =
    p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / HPow.hPow (β := ℕ) (log x) 2
Tactic: filter_upwards [eventually_gt_atTop 0] with x hx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p x : ℝ
hx : 0 < x
⊢ p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) =
    p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / HPow.hPow (β := ℕ) (log x) 2
have h : p * x ^ (p - 1) * (1 - ε x) + x ^ p * x⁻¹ / HPow.hPow (β := ℕ) (log x) 2 =
  p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / HPow.hPow (β := ℕ) (log x) 2
Tactic: rw [mul_div, ← Real.rpow_neg_one, ← Real.rpow_add (by positivity), sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p x : ℝ
hx : 0 < x
h :
  p * x ^ (p - 1) * (1 - ε x) + x ^ p * x⁻¹ / HPow.hPow (β := ℕ) (log x) 2 =
    p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / HPow.hPow (β := ℕ) (log x) 2
⊢ p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) =
    p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / HPow.hPow (β := ℕ) (log x) 2
have h₁ : p * x ^ (p - 1) * (1 - ε x) + x ^ p * HPow.hPow (β := ℝ) x (-1) / HPow.hPow (β := ℕ) (log x) 2 =
  p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / HPow.hPow (β := ℕ) (log x) 2
Tactic: rw [mul_div, ← Real.rpow_neg_one, ← Real.rpow_add (by positivity), sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p x : ℝ
hx : 0 < x
h :
  p * x ^ (p - 1) * (1 - ε x) + x ^ p * x⁻¹ / HPow.hPow (β := ℕ) (log x) 2 =
    p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / HPow.hPow (β := ℕ) (log x) 2
h₁ :
  p * x ^ (p - 1) * (1 - ε x) + x ^ p * HPow.hPow (β := ℝ) x (-1) / HPow.hPow (β := ℕ) (log x) 2 =
    p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / HPow.hPow (β := ℕ) (log x) 2
⊢ p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) =
    p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / HPow.hPow (β := ℕ) (log x) 2
have h₂ : p * x ^ (p - 1) * (1 - ε x) + x ^ (p + -1) / HPow.hPow (β := ℕ) (log x) 2 =
  p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / HPow.hPow (β := ℕ) (log x) 2
Tactic: rw [mul_div, ← Real.rpow_neg_one, ← Real.rpow_add (by positivity), sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p x : ℝ
hx : 0 < x
h :
  p * x ^ (p - 1) * (1 - ε x) + x ^ p * x⁻¹ / HPow.hPow (β := ℕ) (log x) 2 =
    p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / HPow.hPow (β := ℕ) (log x) 2
h₁ :
  p * x ^ (p - 1) * (1 - ε x) + x ^ p * HPow.hPow (β := ℝ) x (-1) / HPow.hPow (β := ℕ) (log x) 2 =
    p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / HPow.hPow (β := ℕ) (log x) 2
h₂ :
  p * x ^ (p - 1) * (1 - ε x) + x ^ (p + -1) / HPow.hPow (β := ℕ) (log x) 2 =
    p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / HPow.hPow (β := ℕ) (log x) 2
⊢ p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) =
    p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / HPow.hPow (β := ℕ) (log x) 2
have h₃ : p * x ^ (p + -1) * (1 - ε x) + x ^ (p + -1) / HPow.hPow (β := ℕ) (log x) 2 =
  p * x ^ (p + -1) * (1 - ε x) + x ^ (p + -1) / HPow.hPow (β := ℕ) (log x) 2
Tactic: rw [mul_div, ← Real.rpow_neg_one, ← Real.rpow_add (by positivity), sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
⊢ EventuallyEq (β := ℝ) atTop (deriv fun (x : ℝ) ↦ x ^ p * (1 + ε x)) fun (x : ℝ) ↦
    deriv (fun (x : ℝ) ↦ x ^ p) x * (1 + ε x) + x ^ p * deriv (fun (x : ℝ) ↦ 1 + ε x) x
have h : ∀ (x : ℝ) (hx : 1 < x),
  deriv (fun (x : ℝ) ↦ x ^ p * (1 + ε x)) x =
    deriv (fun (x : ℝ) ↦ x ^ p) x * (1 + ε x) + x ^ p * deriv (fun (x : ℝ) ↦ 1 + ε x) x
Tactic: filter_upwards [eventually_gt_atTop 1] with x hx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p x : ℝ
hx : 1 < x
⊢ deriv (fun (x : ℝ) ↦ x ^ p * (1 + ε x)) x =
    deriv (fun (x : ℝ) ↦ x ^ p) x * (1 + ε x) + x ^ p * deriv (fun (x : ℝ) ↦ 1 + ε x) x
have h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ p) x
Tactic: rw [deriv_fun_mul]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p x : ℝ
hx : 1 < x
h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ p) x
⊢ deriv (fun (x : ℝ) ↦ x ^ p * (1 + ε x)) x =
    deriv (fun (x : ℝ) ↦ x ^ p) x * (1 + ε x) + x ^ p * deriv (fun (x : ℝ) ↦ 1 + ε x) x
have h₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ 1 + ε x) x
Tactic: rw [deriv_fun_mul]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
⊢ EventuallyEq (β := ℝ) atTop
    (fun (x : ℝ) ↦ deriv (fun (x : ℝ) ↦ x ^ p) x * (1 + ε x) + x ^ p * deriv (fun (x : ℝ) ↦ 1 + ε x) x) fun (x : ℝ) ↦
    p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2)
have h : ∀ (x : ℝ) (hx : 1 < x) (hderiv : deriv (fun (x : ℝ) ↦ 1 + ε x) x = -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2),
  deriv (fun (x : ℝ) ↦ x ^ p) x * (1 + ε x) + x ^ p * deriv (fun (x : ℝ) ↦ 1 + ε x) x =
    p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2)
Tactic: filter_upwards [eventually_gt_atTop 1, eventually_deriv_one_add_smoothingFn]
        with x hx hderiv
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2))
    fun (x : ℝ) ↦ p * x ^ (p - 1) * (1 + ε x) - x ^ (p - 1) / HPow.hPow (β := ℕ) (log x) 2
have h : ∀ (x : ℝ) (hx : 0 < x),
  p * x ^ (p - 1) * (1 + ε x) - x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) =
    p * x ^ (p - 1) * (1 + ε x) - x ^ (p - 1) / HPow.hPow (β := ℕ) (log x) 2
Tactic: filter_upwards [eventually_gt_atTop 0] with x hx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsEquivalent (E' := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1) * (1 - ε z) + z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2)
    fun (z : ℝ) ↦ p * z ^ (p - 1)
have refine : IsEquivalent (E' := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1) * (1 - ε z)) fun (z : ℝ) ↦ p * z ^ (p - 1)
Tactic: refine IsEquivalent.add_isLittleO ?one ?two
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
refine : IsEquivalent (E' := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1) * (1 - ε z)) fun (z : ℝ) ↦ p * z ^ (p - 1)
⊢ IsEquivalent (E' := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1) * (1 - ε z) + z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2)
    fun (z : ℝ) ↦ p * z ^ (p - 1)
have refine₁ : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2) fun (z : ℝ) ↦
  p * z ^ (p - 1)
Tactic: refine IsEquivalent.add_isLittleO ?one ?two
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ Eq (α := (z : ℝ) → ℝ) (fun (z : ℝ) ↦ p * z ^ (p - 1) * 1) fun (z : ℝ) ↦ p * z ^ (p - 1)
have h : ∀ (x : ℝ), p * x ^ (p - 1) * 1 = p * x ^ (p - 1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsEquivalent (E' := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1) * (1 - ε z)) fun (z : ℝ) ↦ p * z ^ (p - 1)
have z : Eq (α := (z : ℝ) → ℝ) (fun (z : ℝ) ↦ p * z ^ (p - 1) * 1) fun (z : ℝ) ↦ p * z ^ (p - 1)
Tactic: calc
        (fun z => p * z ^ (p - 1) * (1 - ε z)) ~[atTop] fun z => p * z ^ (p - 1) * 1 :=
              IsEquivalent.mul IsEquivalent.refl isEquivalent_one_sub_smoothingFn_one
        _ = fun z => p * z ^ (p - 1) := by ext; ring
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ z ^ (p - 1) * (HPow.hPow (β := ℕ) (log z) 2)⁻¹) fun (z : ℝ) ↦
    z ^ (p - 1) * 1⁻¹
have refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ 1) fun (z : ℝ) ↦ HPow.hPow (β := ℕ) (log z) 2
Tactic: refine IsBigO.mul_isLittleO (isBigO_refl _ _)
            (IsLittleO.inv_rev ?_ (by simp))
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ 1) fun (z : ℝ) ↦ HPow.hPow (β := ℕ) (log z) 2
have rw : Eq (α := ℝ) 1 0 ∨
  Tendsto (α := ℝ) (Function.comp (β := ℝ) Norm.norm fun (z : ℝ) ↦ HPow.hPow (β := ℕ) (log z) 2) atTop atTop
Tactic: rw [isLittleO_const_left]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ Eq (α := ℝ) 1 0 ∨
    Tendsto (α := ℝ) (Function.comp (β := ℝ) Norm.norm fun (z : ℝ) ↦ HPow.hPow (β := ℕ) (log z) 2) atTop atTop
have refine : Tendsto (β := ℝ) (fun (z : ℝ) ↦ HPow.hPow (β := ℕ) (log z) 2) atTop atTop
Tactic: refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ Eq (α := (z : ℝ) → ℝ) (fun (z : ℝ) ↦ z ^ (p - 1) / 1) fun (z : ℝ) ↦ z ^ (p - 1)
have h : ∀ (x : ℝ), x ^ (p - 1) / 1 = x ^ (p - 1)
Tactic: ext
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2) fun (z : ℝ) ↦
    p * z ^ (p - 1)
have z : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2) fun (z : ℝ) ↦
  z ^ (p - 1) / 1
Tactic: calc
        (fun z => z ^ (p - 1) / (log z ^ 2)) =o[atTop] fun z => z ^ (p - 1) / 1 := by
          simp_rw [div_eq_mul_inv]
          refine IsBigO.mul_isLittleO (isBigO_refl _ _)
            (IsLittleO.inv_rev ?_ (by simp))
          rw [isLittleO_const_left]
          refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
          exact Tendsto.comp (g := fun z => z ^ 2)
            (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop
        _ = fun z => z ^ (p - 1) := by ext; simp
        _ =Θ[atTop] fun z => p * z ^ (p - 1) := IsTheta.const_mul_right hp <| isTheta_refl _ _
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
z :
  IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2) fun (z : ℝ) ↦
    z ^ (p - 1) / 1
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2) fun (z : ℝ) ↦
    p * z ^ (p - 1)
have z₁ : Eq (α := (z : ℝ) → ℝ) (fun (z : ℝ) ↦ z ^ (p - 1) / 1) fun (z : ℝ) ↦ z ^ (p - 1)
Tactic: calc
        (fun z => z ^ (p - 1) / (log z ^ 2)) =o[atTop] fun z => z ^ (p - 1) / 1 := by
          simp_rw [div_eq_mul_inv]
          refine IsBigO.mul_isLittleO (isBigO_refl _ _)
            (IsLittleO.inv_rev ?_ (by simp))
          rw [isLittleO_const_left]
          refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
          exact Tendsto.comp (g := fun z => z ^ 2)
            (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop
        _ = fun z => z ^ (p - 1) := by ext; simp
        _ =Θ[atTop] fun z => p * z ^ (p - 1) := IsTheta.const_mul_right hp <| isTheta_refl _ _
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2) fun (z : ℝ) ↦
    p * z ^ (p - 1)
have case : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2) fun (z : ℝ) ↦
  z ^ (p - 1) / 1
Tactic: case two => calc
        (fun z => z ^ (p - 1) / (log z ^ 2)) =o[atTop] fun z => z ^ (p - 1) / 1 := by
          simp_rw [div_eq_mul_inv]
          refine IsBigO.mul_isLittleO (isBigO_refl _ _)
            (IsLittleO.inv_rev ?_ (by simp))
          rw [isLittleO_const_left]
          refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
          exact Tendsto.comp (g := fun z => z ^ 2)
            (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop
        _ = fun z => z ^ (p - 1) := by ext; simp
        _ =Θ[atTop] fun z => p * z ^ (p - 1) := IsTheta.const_mul_right hp <| isTheta_refl _ _
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
case :
  IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2) fun (z : ℝ) ↦
    z ^ (p - 1) / 1
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2) fun (z : ℝ) ↦
    p * z ^ (p - 1)
have case₁ : Eq (α := (z : ℝ) → ℝ) (fun (z : ℝ) ↦ z ^ (p - 1) / 1) fun (z : ℝ) ↦ z ^ (p - 1)
Tactic: case two => calc
        (fun z => z ^ (p - 1) / (log z ^ 2)) =o[atTop] fun z => z ^ (p - 1) / 1 := by
          simp_rw [div_eq_mul_inv]
          refine IsBigO.mul_isLittleO (isBigO_refl _ _)
            (IsLittleO.inv_rev ?_ (by simp))
          rw [isLittleO_const_left]
          refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
          exact Tendsto.comp (g := fun z => z ^ 2)
            (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop
        _ = fun z => z ^ (p - 1) := by ext; simp
        _ =Θ[atTop] fun z => p * z ^ (p - 1) := IsTheta.const_mul_right hp <| isTheta_refl _ _
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsEquivalent (E' := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1) * (1 + ε z) - z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2)
    fun (z : ℝ) ↦ p * z ^ (p - 1)
have refine : IsEquivalent (E' := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1) * (1 + ε z)) fun (z : ℝ) ↦ p * z ^ (p - 1)
Tactic: refine IsEquivalent.add_isLittleO ?one ?two
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
refine : IsEquivalent (E' := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1) * (1 + ε z)) fun (z : ℝ) ↦ p * z ^ (p - 1)
⊢ IsEquivalent (E' := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1) * (1 + ε z) - z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2)
    fun (z : ℝ) ↦ p * z ^ (p - 1)
have refine₁ : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ -(z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2)) fun (z : ℝ) ↦
  p * z ^ (p - 1)
Tactic: refine IsEquivalent.add_isLittleO ?one ?two
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsEquivalent (E' := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1) * (1 + ε z)) fun (z : ℝ) ↦ p * z ^ (p - 1)
have z : Eq (α := (z : ℝ) → ℝ) (fun (z : ℝ) ↦ p * z ^ (p - 1) * 1) fun (z : ℝ) ↦ p * z ^ (p - 1)
Tactic: calc
        (fun z => p * z ^ (p - 1) * (1 + ε z)) ~[atTop] fun z => p * z ^ (p - 1) * 1 :=
              IsEquivalent.mul IsEquivalent.refl isEquivalent_one_add_smoothingFn_one
        _ = fun z => p * z ^ (p - 1) := by ext; ring
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ -(z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2)) fun (z : ℝ) ↦
    z ^ (p - 1) / 1
have simp_rw : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x ^ (p - 1) * (HPow.hPow (β := ℕ) (log x) 2)⁻¹) fun (z : ℝ) ↦
  z ^ (p - 1) * 1⁻¹
Tactic: simp_rw [isLittleO_neg_left, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x ^ (p - 1) * (HPow.hPow (β := ℕ) (log x) 2)⁻¹) fun (z : ℝ) ↦
    z ^ (p - 1) * 1⁻¹
have refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ 1) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2
Tactic: refine IsBigO.mul_isLittleO (isBigO_refl _ _)
              (IsLittleO.inv_rev ?_ (by simp))
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ 1) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2
have rw : Eq (α := ℝ) 1 0 ∨
  Tendsto (α := ℝ) (Function.comp (β := ℝ) Norm.norm fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2) atTop atTop
Tactic: rw [isLittleO_const_left]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ Eq (α := ℝ) 1 0 ∨
    Tendsto (α := ℝ) (Function.comp (β := ℝ) Norm.norm fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2) atTop atTop
have refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2) atTop atTop
Tactic: refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ -(z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2)) fun (z : ℝ) ↦
    p * z ^ (p - 1)
have z : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ -(z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2)) fun (z : ℝ) ↦
  z ^ (p - 1) / 1
Tactic: calc
        (fun z => -(z ^ (p - 1) / (log z ^ 2))) =o[atTop] fun z => z ^ (p - 1) / 1 := by
            simp_rw [isLittleO_neg_left, div_eq_mul_inv]
            refine IsBigO.mul_isLittleO (isBigO_refl _ _)
              (IsLittleO.inv_rev ?_ (by simp))
            rw [isLittleO_const_left]
            refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
            exact Tendsto.comp (g := fun z => z ^ 2)
              (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop
        _ = fun z => z ^ (p - 1) := by ext; simp
        _ =Θ[atTop] fun z => p * z ^ (p - 1) := IsTheta.const_mul_right hp <| isTheta_refl _ _
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
z :
  IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ -(z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2)) fun (z : ℝ) ↦
    z ^ (p - 1) / 1
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ -(z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2)) fun (z : ℝ) ↦
    p * z ^ (p - 1)
have z₁ : Eq (α := (z : ℝ) → ℝ) (fun (z : ℝ) ↦ z ^ (p - 1) / 1) fun (z : ℝ) ↦ z ^ (p - 1)
Tactic: calc
        (fun z => -(z ^ (p - 1) / (log z ^ 2))) =o[atTop] fun z => z ^ (p - 1) / 1 := by
            simp_rw [isLittleO_neg_left, div_eq_mul_inv]
            refine IsBigO.mul_isLittleO (isBigO_refl _ _)
              (IsLittleO.inv_rev ?_ (by simp))
            rw [isLittleO_const_left]
            refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
            exact Tendsto.comp (g := fun z => z ^ 2)
              (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop
        _ = fun z => z ^ (p - 1) := by ext; simp
        _ =Θ[atTop] fun z => p * z ^ (p - 1) := IsTheta.const_mul_right hp <| isTheta_refl _ _
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ -(z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2)) fun (z : ℝ) ↦
    p * z ^ (p - 1)
have case : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ -(z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2)) fun (z : ℝ) ↦
  z ^ (p - 1) / 1
Tactic: case two => calc
        (fun z => -(z ^ (p - 1) / (log z ^ 2))) =o[atTop] fun z => z ^ (p - 1) / 1 := by
            simp_rw [isLittleO_neg_left, div_eq_mul_inv]
            refine IsBigO.mul_isLittleO (isBigO_refl _ _)
              (IsLittleO.inv_rev ?_ (by simp))
            rw [isLittleO_const_left]
            refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
            exact Tendsto.comp (g := fun z => z ^ 2)
              (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop
        _ = fun z => z ^ (p - 1) := by ext; simp
        _ =Θ[atTop] fun z => p * z ^ (p - 1) := IsTheta.const_mul_right hp <| isTheta_refl _ _
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
case :
  IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ -(z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2)) fun (z : ℝ) ↦
    z ^ (p - 1) / 1
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ -(z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2)) fun (z : ℝ) ↦
    p * z ^ (p - 1)
have case₁ : Eq (α := (z : ℝ) → ℝ) (fun (z : ℝ) ↦ z ^ (p - 1) / 1) fun (z : ℝ) ↦ z ^ (p - 1)
Tactic: case two => calc
        (fun z => -(z ^ (p - 1) / (log z ^ 2))) =o[atTop] fun z => z ^ (p - 1) / 1 := by
            simp_rw [isLittleO_neg_left, div_eq_mul_inv]
            refine IsBigO.mul_isLittleO (isBigO_refl _ _)
              (IsLittleO.inv_rev ?_ (by simp))
            rw [isLittleO_const_left]
            refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
            exact Tendsto.comp (g := fun z => z ^ 2)
              (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop
        _ = fun z => z ^ (p - 1) := by ext; simp
        _ =Θ[atTop] fun z => p * z ^ (p - 1) := IsTheta.const_mul_right hp <| isTheta_refl _ _
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ Norm.norm (E := ℝ) (deriv (fun (z : ℝ) ↦ z ^ p * (1 - ε z)) x))
    fun (z : ℝ) ↦ z ^ (p - 1)
have refine : IsTheta (E := ℝ) (F := ℝ) atTop (deriv fun (z : ℝ) ↦ z ^ p * (1 - ε z)) fun (z : ℝ) ↦ z ^ (p - 1)
Tactic: refine IsTheta.norm_left ?_
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ Norm.norm (E := ℝ) (deriv (fun (z : ℝ) ↦ z ^ p * (1 + ε z)) x))
    fun (z : ℝ) ↦ z ^ (p - 1)
have refine : IsTheta (E := ℝ) (F := ℝ) atTop (deriv fun (z : ℝ) ↦ z ^ p * (1 + ε z)) fun (z : ℝ) ↦ z ^ (p - 1)
Tactic: refine IsTheta.norm_left ?_
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (hypothesis)
Goal:
f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
have hg' : ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
Tactic: have hg' := hg b hb
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
hg' : ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
have obtain : ∀ (c₁ : ℝ) (hc₁_mem : c₁ > 0) (c₂ : ℝ) (hc₂_mem : c₂ > 0)
  (hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)),
  ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
Tactic: obtain ⟨c₁, hc₁_mem, c₂, hc₂_mem, hg'⟩ := hg'
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
⊢ ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
have refine : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
Tactic: refine ⟨c₁, hc₁_mem, c₂, hc₂_mem, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.GrowsPolynomially (goal)
Goal:
f g : ℝ → ℝ
hfg : f =ᶠ[atTop] g
hg : GrowsPolynomially g
b : ℝ
hb : Membership.mem (γ := Set ℝ) (Set.Ioo 0 1) b
c₁ : ℝ
hc₁_mem : c₁ > 0
c₂ : ℝ
hc₂_mem : c₂ > 0
hg' : ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x)
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
have h : ∀ (x : ℝ) (hx₁ : ∀ u ∈ Set.Icc (b * x) x, g u ∈ Set.Icc (c₁ * g x) (c₂ * g x))
  (hx₂ : ∀ (y : ℝ), b * id x ≤ y → f y = g y) (hx₃ : f x = g x),
  ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)
Tactic: filter_upwards [hg', (tendsto_id.const_mul_atTop hb.1).eventually_forall_ge_atTop hfg, hfg]
    with x hx₁ hx₂ hx₃