awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
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)
⊢ 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)

Tactic:
filter_upwards [eventually_gt_atTop 1, eventually_deriv_one_sub_smoothingFn]
      with x hx hderiv

Premises used: AkraBazziRecurrence.eventually_deriv_one_sub_smoothingFn, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p x : ℝ
hx : 1 < x
hderiv : deriv (fun (x : ℝ) ↦ 1 - ε x) x = x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
h :
  deriv (fun (x : ℝ) ↦ x ^ p) x * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) =
    p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2)
h₁ h₂ :
  p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) =
    p * x ^ (p - 1) * (1 - ε x) + x ^ p * (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:
rw [hderiv, Real.deriv_rpow_const]

Premises used: Real.deriv_rpow_const
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
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
⊢ 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

Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p x : ℝ
hx : 0 < x
⊢ 0 < x

Tactic:
positivity
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
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
h₃ 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

Tactic:
rw [mul_div, ← Real.rpow_neg_one, ← Real.rpow_add (by positivity), sub_eq_add_neg]

Premises used: mul_div, Real.rpow_neg_one, sub_eq_add_neg, Real.rpow_add
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
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
⊢ 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

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p x : ℝ
hx : 1 < x
h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ p) x
h₁ : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ 1 + ε x) 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:
rw [deriv_fun_mul]

Premises used: deriv_fun_mul
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ p) x

Tactic:
exact differentiableAt_rpow_const_of_ne _ (by positivity)

Premises used: Real.differentiableAt_rpow_const_of_ne
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ 1 + ε x) x

Tactic:
differentiableAt_one_add_smoothingFn hx

Premises used: AkraBazziRecurrence.differentiableAt_one_add_smoothingFn
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ 1 + ε x) x

Tactic:
exact differentiableAt_one_add_smoothingFn hx

Premises used: AkraBazziRecurrence.differentiableAt_one_add_smoothingFn
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
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)
⊢ 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)

Tactic:
filter_upwards [eventually_gt_atTop 1, eventually_deriv_one_add_smoothingFn]
        with x hx hderiv

Premises used: AkraBazziRecurrence.eventually_deriv_one_add_smoothingFn, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p 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:
simp [hderiv, Real.deriv_rpow_const, neg_div, sub_eq_add_neg]

Premises used: neg_div, Real.deriv_rpow_const, sub_eq_add_neg
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
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
⊢ 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

Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
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

Tactic:
simp [mul_div, ← Real.rpow_neg_one, ← Real.rpow_add (by positivity), sub_eq_add_neg]

Premises used: mul_div, Real.rpow_neg_one, sub_eq_add_neg, Real.rpow_add
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
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)

Tactic:
IsEquivalent.add_isLittleO ?one ?two

Premises used: Asymptotics.IsEquivalent.add_isLittleO
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
refine : IsEquivalent (E' := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1) * (1 - ε z)) fun (z : ℝ) ↦ p * z ^ (p - 1)
refine₁ :
  IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2) 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)

Tactic:
refine IsEquivalent.add_isLittleO ?one ?two

Premises used: Asymptotics.IsEquivalent.add_isLittleO
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsEquivalent (E' := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1) * (1 - ε z)) fun (z : ℝ) ↦ p * z ^ (p - 1) * 1

Tactic:
IsEquivalent.mul IsEquivalent.refl isEquivalent_one_sub_smoothingFn_one

Premises used: Asymptotics.IsEquivalent.mul, AkraBazziRecurrence.isEquivalent_one_sub_smoothingFn_one, Asymptotics.IsEquivalent.refl
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
h : ∀ (x : ℝ), p * x ^ (p - 1) * 1 = p * x ^ (p - 1)
⊢ Eq (α := (z : ℝ) → ℝ) (fun (z : ℝ) ↦ p * z ^ (p - 1) * 1) fun (z : ℝ) ↦ p * z ^ (p - 1)

Tactic:
ext
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
x : ℝ
⊢ p * x ^ (p - 1) * 1 = p * x ^ (p - 1)

Tactic:
ring
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
z : Eq (α := (z : ℝ) → ℝ) (fun (z : ℝ) ↦ p * z ^ (p - 1) * 1) fun (z : ℝ) ↦ p * z ^ (p - 1)
⊢ IsEquivalent (E' := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1) * (1 - ε z)) 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

Premises used: HMul.hMul, Asymptotics.IsEquivalent.mul, HSub.hSub, Filter.atTop, AkraBazziRecurrence.smoothingFn, AkraBazziRecurrence.isEquivalent_one_sub_smoothingFn_one, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsEquivalent (E' := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1) * (1 - ε z)) fun (z : ℝ) ↦ p * z ^ (p - 1)

Tactic:
case one => 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

Premises used: HMul.hMul, Asymptotics.IsEquivalent.mul, HSub.hSub, Filter.atTop, AkraBazziRecurrence.smoothingFn, AkraBazziRecurrence.isEquivalent_one_sub_smoothingFn_one, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
⊢ ∀ᶠ (x : ℝ) in atTop, Eq (α := ℝ) 1 0 → HPow.hPow (β := ℕ) (log x) 2 = 0

Tactic:
simp
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ 1) fun (z : ℝ) ↦ HPow.hPow (β := ℕ) (log z) 2
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ z ^ (p - 1) * (HPow.hPow (β := ℕ) (log z) 2)⁻¹) fun (z : ℝ) ↦
    z ^ (p - 1) * 1⁻¹

Tactic:
refine IsBigO.mul_isLittleO (isBigO_refl _ _)
            (IsLittleO.inv_rev ?_ (by simp))

Premises used: Asymptotics.IsBigO.mul_isLittleO
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
rw :
  Eq (α := ℝ) 1 0 ∨
    Tendsto (α := ℝ) (Function.comp (β := ℝ) Norm.norm fun (z : ℝ) ↦ HPow.hPow (β := ℕ) (log z) 2) atTop atTop
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ 1) fun (z : ℝ) ↦ HPow.hPow (β := ℕ) (log z) 2

Tactic:
rw [isLittleO_const_left]

Premises used: Asymptotics.isLittleO_const_left
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
⊢ Eq (α := ℝ) 1 0 ∨
    Tendsto (α := ℝ) (Function.comp (β := ℝ) Norm.norm fun (z : ℝ) ↦ HPow.hPow (β := ℕ) (log z) 2) atTop atTop

Tactic:
Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_

Premises used: tendsto_norm_atTop_atTop, Filter.Tendsto.comp, Or.inr
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
refine : Tendsto (β := ℝ) (fun (z : ℝ) ↦ HPow.hPow (β := ℕ) (log z) 2) atTop atTop
⊢ Eq (α := ℝ) 1 0 ∨
    Tendsto (α := ℝ) (Function.comp (β := ℝ) Norm.norm fun (z : ℝ) ↦ HPow.hPow (β := ℕ) (log z) 2) atTop atTop

Tactic:
refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_

Premises used: tendsto_norm_atTop_atTop, Filter.Tendsto.comp, Or.inr
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
⊢ Ne (α := ℕ) 2 0

Tactic:
norm_num
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
⊢ Tendsto (β := ℝ) (fun (z : ℝ) ↦ HPow.hPow (β := ℕ) (log z) 2) atTop atTop

Tactic:
exact Tendsto.comp (g := fun z => z ^ 2)
            (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop

Premises used: Real.tendsto_log_atTop, Filter.Tendsto.comp, Filter.tendsto_pow_atTop
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
h : ∀ (x : ℝ), x ^ (p - 1) / 1 = x ^ (p - 1)
⊢ Eq (α := (z : ℝ) → ℝ) (fun (z : ℝ) ↦ z ^ (p - 1) / 1) fun (z : ℝ) ↦ z ^ (p - 1)

Tactic:
ext
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
x : ℝ
⊢ x ^ (p - 1) / 1 = x ^ (p - 1)

Tactic:
simp
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ z ^ (p - 1)) fun (z : ℝ) ↦ p * z ^ (p - 1)

Tactic:
IsTheta.const_mul_right hp <| isTheta_refl _ _

Premises used: Asymptotics.isTheta_refl, Asymptotics.IsTheta.const_mul_right
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
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
z₁ : Eq (α := (z : ℝ) → ℝ) (fun (z : ℝ) ↦ z ^ (p - 1) / 1) fun (z : ℝ) ↦ z ^ (p - 1)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2) fun (z : ℝ) ↦
    p * 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 _ _

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Real.log, Filter.atTop, HPow.hPow, Asymptotics.isTheta_refl, OfNat.ofNat, Asymptotics.IsTheta.const_mul_right
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
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
case₁ : Eq (α := (z : ℝ) → ℝ) (fun (z : ℝ) ↦ z ^ (p - 1) / 1) fun (z : ℝ) ↦ z ^ (p - 1)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2) fun (z : ℝ) ↦
    p * 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 _ _

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Real.log, Filter.atTop, HPow.hPow, Asymptotics.isTheta_refl, OfNat.ofNat, Asymptotics.IsTheta.const_mul_right
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
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)

Tactic:
IsEquivalent.add_isLittleO ?one ?two

Premises used: Asymptotics.IsEquivalent.add_isLittleO
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
refine : IsEquivalent (E' := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1) * (1 + ε z)) fun (z : ℝ) ↦ p * z ^ (p - 1)
refine₁ :
  IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ -(z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2)) 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)

Tactic:
refine IsEquivalent.add_isLittleO ?one ?two

Premises used: Asymptotics.IsEquivalent.add_isLittleO
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsEquivalent (E' := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1) * (1 + ε z)) fun (z : ℝ) ↦ p * z ^ (p - 1) * 1

Tactic:
IsEquivalent.mul IsEquivalent.refl isEquivalent_one_add_smoothingFn_one

Premises used: Asymptotics.IsEquivalent.mul, Asymptotics.IsEquivalent.refl, AkraBazziRecurrence.isEquivalent_one_add_smoothingFn_one
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
z : Eq (α := (z : ℝ) → ℝ) (fun (z : ℝ) ↦ p * z ^ (p - 1) * 1) fun (z : ℝ) ↦ p * z ^ (p - 1)
⊢ IsEquivalent (E' := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1) * (1 + ε z)) 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

Premises used: HMul.hMul, Asymptotics.IsEquivalent.mul, HSub.hSub, Filter.atTop, AkraBazziRecurrence.smoothingFn, HPow.hPow, HAdd.hAdd, AkraBazziRecurrence.isEquivalent_one_add_smoothingFn_one, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsEquivalent (E' := ℝ) atTop (fun (z : ℝ) ↦ p * z ^ (p - 1) * (1 + ε z)) fun (z : ℝ) ↦ p * z ^ (p - 1)

Tactic:
case one => 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

Premises used: HMul.hMul, Asymptotics.IsEquivalent.mul, HSub.hSub, Filter.atTop, AkraBazziRecurrence.smoothingFn, HPow.hPow, HAdd.hAdd, AkraBazziRecurrence.isEquivalent_one_add_smoothingFn_one, OfNat.ofNat
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
simp_rw :
  IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x ^ (p - 1) * (HPow.hPow (β := ℕ) (log x) 2)⁻¹) fun (z : ℝ) ↦
    z ^ (p - 1) * 1⁻¹
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ -(z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2)) fun (z : ℝ) ↦
    z ^ (p - 1) / 1

Tactic:
simp_rw [isLittleO_neg_left, div_eq_mul_inv]

Premises used: div_eq_mul_inv, Asymptotics.isLittleO_neg_left
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ 1) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x ^ (p - 1) * (HPow.hPow (β := ℕ) (log x) 2)⁻¹) fun (z : ℝ) ↦
    z ^ (p - 1) * 1⁻¹

Tactic:
refine IsBigO.mul_isLittleO (isBigO_refl _ _)
              (IsLittleO.inv_rev ?_ (by simp))

Premises used: Asymptotics.IsBigO.mul_isLittleO
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
rw :
  Eq (α := ℝ) 1 0 ∨
    Tendsto (α := ℝ) (Function.comp (β := ℝ) Norm.norm fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2) atTop atTop
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ 1) fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2

Tactic:
rw [isLittleO_const_left]

Premises used: Asymptotics.isLittleO_const_left
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
⊢ Eq (α := ℝ) 1 0 ∨
    Tendsto (α := ℝ) (Function.comp (β := ℝ) Norm.norm fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2) atTop atTop

Tactic:
Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_

Premises used: tendsto_norm_atTop_atTop, Filter.Tendsto.comp, Or.inr
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2) atTop atTop
⊢ Eq (α := ℝ) 1 0 ∨
    Tendsto (α := ℝ) (Function.comp (β := ℝ) Norm.norm fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2) atTop atTop

Tactic:
refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_

Premises used: tendsto_norm_atTop_atTop, Filter.Tendsto.comp, Or.inr
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ HPow.hPow (β := ℕ) (log x) 2) atTop atTop

Tactic:
exact Tendsto.comp (g := fun z => z ^ 2)
              (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop

Premises used: Real.tendsto_log_atTop, Filter.Tendsto.comp, Filter.tendsto_pow_atTop
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
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
z₁ : Eq (α := (z : ℝ) → ℝ) (fun (z : ℝ) ↦ z ^ (p - 1) / 1) fun (z : ℝ) ↦ z ^ (p - 1)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ -(z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2)) fun (z : ℝ) ↦
    p * 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 _ _

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Real.log, Filter.atTop, HPow.hPow, Asymptotics.isTheta_refl, OfNat.ofNat, Neg.neg, Asymptotics.IsTheta.const_mul_right
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
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
case₁ : Eq (α := (z : ℝ) → ℝ) (fun (z : ℝ) ↦ z ^ (p - 1) / 1) fun (z : ℝ) ↦ z ^ (p - 1)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (z : ℝ) ↦ -(z ^ (p - 1) / HPow.hPow (β := ℕ) (log z) 2)) fun (z : ℝ) ↦
    p * 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 _ _

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, Real.log, Filter.atTop, HPow.hPow, Asymptotics.isTheta_refl, OfNat.ofNat, Neg.neg, Asymptotics.IsTheta.const_mul_right
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
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)

Tactic:
IsTheta.norm_left ?_

Premises used: Asymptotics.IsTheta.norm_left
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
refine : IsTheta (E := ℝ) (F := ℝ) atTop (deriv fun (z : ℝ) ↦ z ^ p * (1 - ε z)) fun (z : ℝ) ↦ z ^ (p - 1)
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ Norm.norm (E := ℝ) (deriv (fun (z : ℝ) ↦ z ^ p * (1 - ε z)) x))
    fun (z : ℝ) ↦ z ^ (p - 1)

Tactic:
refine IsTheta.norm_left ?_

Premises used: Asymptotics.IsTheta.norm_left
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
hp : p ≠ 0
⊢ IsTheta (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ deriv (fun (z : ℝ) ↦ z ^ p * (1 - ε z)) x) fun (z : ℝ) ↦
    p * z ^ (p - 1)

Tactic:
(isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn hp).isTheta

Premises used: Asymptotics.IsEquivalent.isTheta, AkraBazziRecurrence.isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn