awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
inl : ∀ (hx : 0 < x), HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) x
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) x
have inr : ∀ (hx : x < 0), HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) x
Tactic: rcases lt_or_gt_of_ne hx.symm with (hx | hx)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) x
have inl : HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) (↑x : ℂ)
Tactic: apply HasDerivAt.comp_ofReal (e := fun y => (y : ℂ) ^ (r + 1) / (r + 1))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) (↑x : ℂ)
have h : (↑x : ℂ) ^ r = (↑x : ℂ) ^ r * (r + 1) / (r + 1)
Tactic: convert! HasDerivAt.div_const (𝕜 := ℂ) ?_ (r + 1) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
h : (↑x : ℂ) ^ r = (↑x : ℂ) ^ r * (r + 1) / (r + 1)
inl : ℂ
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) (↑x : ℂ)
have inl₁ : HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1)) ((↑x : ℂ) ^ r * (r + 1)) (↑x : ℂ)
Tactic: convert! HasDerivAt.div_const (𝕜 := ℂ) ?_ (r + 1) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1)) ((↑x : ℂ) ^ r * (r + 1)) (↑x : ℂ)
have h : (↑x : ℂ) ^ r * (r + 1) = (r + 1) * (↑x : ℂ) ^ (r + 1 - 1) * 1
Tactic: convert! HasDerivAt.cpow_const ?_ ?_ using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
h : (↑x : ℂ) ^ r * (r + 1) = (r + 1) * (↑x : ℂ) ^ (r + 1 - 1) * 1
inl : ℂ
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1)) ((↑x : ℂ) ^ r * (r + 1)) (↑x : ℂ)
have inl₁ : HasDerivAt (F := ℂ) (fun (y : ℂ) ↦ y) 1 (↑x : ℂ)
Tactic: convert! HasDerivAt.cpow_const ?_ ?_ using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
h : (↑x : ℂ) ^ r * (r + 1) = (r + 1) * (↑x : ℂ) ^ (r + 1 - 1) * 1
inl : ℂ
inl₁ : HasDerivAt (F := ℂ) (fun (y : ℂ) ↦ y) 1 (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1)) ((↑x : ℂ) ^ r * (r + 1)) (↑x : ℂ)
have inl₂ : (↑x : ℂ) ∈ slitPlane
Tactic: convert! HasDerivAt.cpow_const ?_ ?_ using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ (↑x : ℂ) ^ r * (r + 1) = (r + 1) * (↑x : ℂ) ^ (r + 1 - 1) * 1
have h : (r + 1) * (↑x : ℂ) ^ r = (r + 1) * (↑x : ℂ) ^ r * 1
Tactic: rw [add_sub_cancel_right, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
⊢ ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
have refine : ∀ (y : ℝ) (hy : Membership.mem (γ := Set ℝ) (Set.Iio 0) y),
  (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
Tactic: refine Filter.eventually_of_mem (Iio_mem_nhds hx) fun y hy => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Iio 0) y
⊢ (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
have rw : (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1) =
  (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
Tactic: rw [ofReal_cpow_of_nonpos (le_of_lt hy)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (hypothesis)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) x
have this : ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
Tactic: have : ∀ᶠ y : ℝ in 𝓝 x,
        (y : ℂ) ^ (r + 1) / (r + 1) = (-y : ℂ) ^ (r + 1) * exp (π * I * (r + 1)) / (r + 1) := by
      refine Filter.eventually_of_mem (Iio_mem_nhds hx) fun y hy => ?_
      rw [ofReal_cpow_of_nonpos (le_of_lt hy)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) x
have inr : HasDerivAt (fun (x : ℝ) ↦ (-(↑x : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)) ((↑x : ℂ) ^ r) x
Tactic: refine HasDerivAt.congr_of_eventuallyEq ?_ this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun (x : ℝ) ↦ (-(↑x : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)) ((↑x : ℂ) ^ r) x
have inr : HasDerivAt (fun (x : ℝ) ↦ (-(↑x : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1))
  ((-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r)) x
Tactic: rw [ofReal_cpow_of_nonpos (le_of_lt hx)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this_1 :
  ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
this :
  HasDerivAt (fun (y : ℝ) ↦ (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)))
    ((r + 1) * (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r)) x
⊢ HasDerivAt (fun (x : ℝ) ↦ (-(↑x : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1))
    ((-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r)) x
have h : (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r) = (r + 1) * (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r) / (r + 1)
Tactic: convert! this.div_const (r + 1) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this_1 :
  ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
this :
  HasDerivAt (fun (y : ℝ) ↦ (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)))
    ((r + 1) * (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r)) x
| (r + 1) * (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r) / (r + 1)
have rw : (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r)
Tactic: rw [mul_assoc, mul_comm, mul_div_cancel_right₀ _ hr]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this_1 :
  ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
this :
  HasDerivAt (fun (y : ℝ) ↦ (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)))
    ((r + 1) * (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r)) x
⊢ (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r) = (r + 1) * (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r) / (r + 1)
have conv_rhs : (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r) = (r + 1) * (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r) / (r + 1)
Tactic: conv_rhs => rw [mul_assoc, mul_comm, mul_div_cancel_right₀ _ hr]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this_1 :
  ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
this :
  HasDerivAt (fun (y : ℝ) ↦ (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)))
    ((r + 1) * (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r)) x
conv_rhs : (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r) = (r + 1) * (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r) / (r + 1)
⊢ (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r) = (r + 1) * (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r) / (r + 1)
have h : (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r) = (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r)
Tactic: conv_rhs => rw [mul_assoc, mul_comm, mul_div_cancel_right₀ _ hr]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun (x : ℝ) ↦ (-(↑x : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1))
    ((-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r)) x
have inr : HasDerivAt (fun (y : ℝ) ↦ (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)))
  ((r + 1) * (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r)) x
Tactic: suffices HasDerivAt (fun y : ℝ => (-↑y) ^ (r + 1) * exp (↑π * I * (r + 1)))
        ((r + 1) * (-↑x) ^ r * exp (↑π * I * r)) x by
      convert! this.div_const (r + 1) using 1
      conv_rhs => rw [mul_assoc, mul_comm, mul_div_cancel_right₀ _ hr]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun (y : ℝ) ↦ (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)))
    ((r + 1) * (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r)) x
have inr : HasDerivAt (fun (y : ℝ) ↦ (-(↑y : ℂ)) ^ (r + 1) * -cexp ((↑π : ℂ) * I * r))
  ((r + 1) * (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r)) x
Tactic: rw [mul_add ((π : ℂ) * _), mul_one, exp_add, exp_pi_mul_I, mul_comm (_ : ℂ) (-1 : ℂ),
      neg_one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun (y : ℝ) ↦ (-(↑y : ℂ)) ^ (r + 1) * -cexp ((↑π : ℂ) * I * r))
    ((r + 1) * (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r)) x
have inr : HasDerivAt (fun (y : ℝ) ↦ -(↑(-y) : ℂ) ^ (r + 1) * cexp ((↑π : ℂ) * I * r))
  ((r + 1) * (↑(-x) : ℂ) ^ r * cexp ((↑π : ℂ) * I * r)) x
Tactic: simp_rw [mul_neg, ← neg_mul, ← ofReal_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this_1 :
  ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun (y : ℝ) ↦ (↑(-y) : ℂ) ^ (r + 1)) (-(r + 1) * (↑(-x) : ℂ) ^ r) x
⊢ HasDerivAt (fun (y : ℝ) ↦ -(↑(-y) : ℂ) ^ (r + 1) * cexp ((↑π : ℂ) * I * r))
    ((r + 1) * (↑(-x) : ℂ) ^ r * cexp ((↑π : ℂ) * I * r)) x
have h : (r + 1) * (↑(-x) : ℂ) ^ r * cexp ((↑π : ℂ) * I * r) = -(-(r + 1) * (↑(-x) : ℂ) ^ r) * cexp ((↑π : ℂ) * I * r)
Tactic: convert! this.neg.mul_const _ using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun (y : ℝ) ↦ -(↑(-y) : ℂ) ^ (r + 1) * cexp ((↑π : ℂ) * I * r))
    ((r + 1) * (↑(-x) : ℂ) ^ r * cexp ((↑π : ℂ) * I * r)) x
have inr : HasDerivAt (fun (y : ℝ) ↦ (↑(-y) : ℂ) ^ (r + 1)) (-(r + 1) * (↑(-x) : ℂ) ^ r) x
Tactic: suffices HasDerivAt (fun y : ℝ => (↑(-y) : ℂ) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x by
      convert! this.neg.mul_const _ using 1; ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this_1 :
  ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ (r + 1)) ((r + 1) * (↑(-x) : ℂ) ^ r) (-x)
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑(-y) : ℂ) ^ (r + 1)) (-(r + 1) * (↑(-x) : ℂ) ^ r) x
have h : -(r + 1) * (↑(-x) : ℂ) ^ r = HSMul.hSMul (α := ℝ) (-1) ((r + 1) * (↑(-x) : ℂ) ^ r)
Tactic: convert! @HasDerivAt.scomp ℝ _ ℂ _ _ x ℝ _ _ _ _ _ _ _ _ this (hasDerivAt_neg x) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this_1 :
  ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
this : HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ (r + 1)) ((r + 1) * (↑(-x) : ℂ) ^ r) (-x)
⊢ -(r + 1) * (↑(-x) : ℂ) ^ r = HSMul.hSMul (α := ℝ) (-1) ((r + 1) * (↑(-x) : ℂ) ^ r)
have h : -(r + 1) * (↑(-x) : ℂ) ^ r = -1 * ((r + 1) * (↑(-x) : ℂ) ^ r)
Tactic: rw [real_smul, ofReal_neg 1, ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑(-y) : ℂ) ^ (r + 1)) (-(r + 1) * (↑(-x) : ℂ) ^ r) x
have inr : HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ (r + 1)) ((r + 1) * (↑(-x) : ℂ) ^ r) (-x)
Tactic: suffices HasDerivAt (fun y : ℝ => (y : ℂ) ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) (-x) by
      convert! @HasDerivAt.scomp ℝ _ ℂ _ _ x ℝ _ _ _ _ _ _ _ _ this (hasDerivAt_neg x) using 1
      rw [real_smul, ofReal_neg 1, ofReal_one]; ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ (r + 1)) ((r + 1) * (↑(-x) : ℂ) ^ r) (-x)
have inr : HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1)) ((r + 1) * (↑(-x) : ℂ) ^ r) (↑(-x) : ℂ)
Tactic: suffices HasDerivAt (fun y : ℂ => y ^ (r + 1)) ((r + 1) * ↑(-x) ^ r) ↑(-x) by
      exact this.comp_ofReal
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
y : ℂ
| y ^ (r + 1)
have rw : y ^ (r + 1 - 1 + 1)
Tactic: rw [(by ring : r = r + 1 - 1)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1)) ((r + 1) * (↑(-x) : ℂ) ^ r) (↑(-x) : ℂ)
have inr : HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1 - 1 + 1)) ((r + 1) * (↑(-x) : ℂ) ^ r) (↑(-x) : ℂ)
Tactic: conv in ↑_ ^ _ => rw [(by ring : r = r + 1 - 1)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1 - 1 + 1)) ((r + 1) * (↑(-x) : ℂ) ^ r) (↑(-x) : ℂ)
have h : (r + 1) * (↑(-x) : ℂ) ^ r = (r + 1 - 1 + 1) * (↑(-x) : ℂ) ^ (r + 1 - 1 + 1 - 1) * 1
Tactic: convert! HasDerivAt.cpow_const ?_ ?_ using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
h : (r + 1) * (↑(-x) : ℂ) ^ r = (r + 1 - 1 + 1) * (↑(-x) : ℂ) ^ (r + 1 - 1 + 1 - 1) * 1
inr : ℂ
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1 - 1 + 1)) ((r + 1) * (↑(-x) : ℂ) ^ r) (↑(-x) : ℂ)
have inr₁ : HasDerivAt (F := ℂ) (fun (y : ℂ) ↦ y) 1 (↑(-x) : ℂ)
Tactic: convert! HasDerivAt.cpow_const ?_ ?_ using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
h : (r + 1) * (↑(-x) : ℂ) ^ r = (r + 1 - 1 + 1) * (↑(-x) : ℂ) ^ (r + 1 - 1 + 1 - 1) * 1
inr : ℂ
inr₁ : HasDerivAt (F := ℂ) (fun (y : ℂ) ↦ y) 1 (↑(-x) : ℂ)
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1 - 1 + 1)) ((r + 1) * (↑(-x) : ℂ) ^ r) (↑(-x) : ℂ)
have inr₂ : (↑(-x) : ℂ) ∈ slitPlane
Tactic: convert! HasDerivAt.cpow_const ?_ ?_ using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
this : ∀ᶠ (y : ℝ) in 𝓝 x, (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
⊢ (r + 1) * (↑(-x) : ℂ) ^ r = (r + 1 - 1 + 1) * (↑(-x) : ℂ) ^ (r + 1 - 1 + 1 - 1) * 1
have h : (r + 1) * (↑(-x) : ℂ) ^ r = (r + 1) * (↑(-x) : ℂ) ^ r * 1
Tactic: rw [add_sub_cancel_right, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ 0
⊢ r - 1 ≠ -1
have rwa : ¬r - 1 = -1
Tactic: rwa [ne_eq, sub_eq_neg_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ 0
rwa : ¬r - 1 = -1
a : ℂ
⊢ r - 1 ≠ -1
have rwa₁ : ¬r = 0
Tactic: rwa [ne_eq, sub_eq_neg_self]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (hypothesis)
Goal:
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ 0
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ r) (r * (↑x : ℂ) ^ (r - 1)) x
have this : HasDerivAt (fun (y : ℝ) ↦ r * ((↑y : ℂ) ^ (r - 1 + 1) / (r - 1 + 1))) (r * (↑x : ℂ) ^ (r - 1)) x
Tactic: have := HasDerivAt.const_mul r <| hasDerivAt_ofReal_cpow_const' hx
    (by rwa [ne_eq, sub_eq_neg_self])
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
c : ℂ
hc : c ≠ 0
x : ℝ
hx : x ≠ 0
⊢ deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ c) x = c * (↑x : ℂ) ^ (c - 1)
have rw : c * (↑x : ℂ) ^ (c - 1) = c * (↑x : ℂ) ^ (c - 1)
Tactic: rw [deriv_ofReal_cpow_const hx hc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
c : ℂ
hc : c ≠ 0
⊢ EventuallyEq (β := ℂ) atTop (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ c) fun (x : ℝ) ↦ c * (↑x : ℂ) ^ (c - 1)
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ≠ 0) x} x →
        Membership.mem (γ := Set ℝ)
          {x : ℝ |
            (fun (x : ℝ) ↦
                Eq (α := ℂ) (deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ c) x) ((fun (x : ℝ) ↦ c * (↑x : ℂ) ^ (c - 1)) x))
              x}
          x}
    a
Tactic: filter_upwards [eventually_ne_atTop 0] with x hx using by rw [deriv_ofReal_cpow_const hx hc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
c : ℂ
hc : c ≠ 0
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ≠ 0) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  Eq (α := ℂ) (deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ c) x) ((fun (x : ℝ) ↦ c * (↑x : ℂ) ^ (c - 1)) x))
                x}
            x}
      a
⊢ EventuallyEq (β := ℂ) atTop (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ c) fun (x : ℝ) ↦ c * (↑x : ℂ) ^ (c - 1)
have h₁ : ∀ (a : ℝ), a ≠ 0 → deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ c) a = c * (↑a : ℂ) ^ (c - 1)
Tactic: filter_upwards [eventually_ne_atTop 0] with x hx using by rw [deriv_ofReal_cpow_const hx hc]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
c : ℂ
hc : c ≠ 0
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (c - 1)‖) fun (x : ℝ) ↦ x ^ (c.re - 1)
have h : ∀ (x : ℝ) (hx : 0 < x), ‖(↑x : ℂ) ^ (c - 1)‖ = x ^ (c.re - 1)
Tactic: filter_upwards [eventually_gt_atTop 0] with x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
c : ℂ
hc : c ≠ 0
x : ℝ
hx : 0 < x
⊢ ‖(↑x : ℂ) ^ (c - 1)‖ = x ^ (c.re - 1)
have h : x ^ (c - 1).re = x ^ (c.re - 1)
Tactic: rw [norm_cpow_eq_rpow_re_of_pos hx, sub_re, one_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
c : ℂ
hc : c ≠ 0
x : ℝ
hx : 0 < x
h : x ^ (c - 1).re = x ^ (c.re - 1)
⊢ ‖(↑x : ℂ) ^ (c - 1)‖ = x ^ (c.re - 1)
have h₁ : x ^ (c.re - re 1) = x ^ (c.re - 1)
Tactic: rw [norm_cpow_eq_rpow_re_of_pos hx, sub_re, one_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
c : ℂ
hc : c ≠ 0
x : ℝ
hx : 0 < x
h : x ^ (c - 1).re = x ^ (c.re - 1)
h₁ : x ^ (c.re - re 1) = x ^ (c.re - 1)
⊢ ‖(↑x : ℂ) ^ (c - 1)‖ = x ^ (c.re - 1)
have h₂ : x ^ (c.re - 1) = x ^ (c.re - 1)
Tactic: rw [norm_cpow_eq_rpow_re_of_pos hx, sub_re, one_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
c : ℂ
hc : c ≠ 0
⊢ Asymptotics.IsTheta (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ c) fun (x : ℝ) ↦ x ^ (c.re - 1)
have _ : EventuallyEq (β := ℂ) atTop (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ c) fun (x : ℝ) ↦ c * (↑x : ℂ) ^ (c - 1)
Tactic: calc
    _ =ᶠ[atTop] fun x : ℝ ↦ c * x ^ (c - 1) := by
      filter_upwards [eventually_ne_atTop 0] with x hx using by rw [deriv_ofReal_cpow_const hx hc]
    _ =Θ[atTop] fun x : ℝ ↦ ‖(x : ℂ) ^ (c - 1)‖ :=
      (Asymptotics.IsTheta.of_norm_eventuallyEq EventuallyEq.rfl).const_mul_left hc
    _ =ᶠ[atTop] fun x ↦ x ^ (c.re - 1) := by
      filter_upwards [eventually_gt_atTop 0] with x hx
      rw [norm_cpow_eq_rpow_re_of_pos hx, sub_re, one_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
c : ℂ
hc : c ≠ 0
_ : EventuallyEq (β := ℂ) atTop (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ c) fun (x : ℝ) ↦ c * (↑x : ℂ) ^ (c - 1)
⊢ Asymptotics.IsTheta (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ c) fun (x : ℝ) ↦ x ^ (c.re - 1)
have _₁ : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (c - 1)‖) fun (x : ℝ) ↦ x ^ (c.re - 1)
Tactic: calc
    _ =ᶠ[atTop] fun x : ℝ ↦ c * x ^ (c - 1) := by
      filter_upwards [eventually_ne_atTop 0] with x hx using by rw [deriv_ofReal_cpow_const hx hc]
    _ =Θ[atTop] fun x : ℝ ↦ ‖(x : ℂ) ^ (c - 1)‖ :=
      (Asymptotics.IsTheta.of_norm_eventuallyEq EventuallyEq.rfl).const_mul_left hc
    _ =ᶠ[atTop] fun x ↦ x ^ (c.re - 1) := by
      filter_upwards [eventually_gt_atTop 0] with x hx
      rw [norm_cpow_eq_rpow_re_of_pos hx, sub_re, one_re]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
c : ℂ
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ c) fun (x : ℝ) ↦ x ^ (c.re - 1)
have inl : Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ HPow.hPow (β := ℂ) (↑x : ℂ) 0) fun (x : ℝ) ↦
  x ^ (re 0 - 1)
Tactic: obtain rfl | hc := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
c : ℂ
inl :
  Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ HPow.hPow (β := ℂ) (↑x : ℂ) 0) fun (x : ℝ) ↦
    x ^ (re 0 - 1)
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ c) fun (x : ℝ) ↦ x ^ (c.re - 1)
have inr : ∀ (hc : c ≠ 0),
  Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ c) fun (x : ℝ) ↦ x ^ (c.re - 1)
Tactic: obtain rfl | hc := eq_or_ne c 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ HPow.hPow (β := ℂ) (↑x : ℂ) 0) fun (x : ℝ) ↦
    x ^ (re 0 - 1)
have inl : Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ 1) fun (x : ℝ) ↦ x ^ (re 0 - 1)
Tactic: simp_rw [cpow_zero, deriv_const', Asymptotics.isBigO_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
inl : Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ 1) fun (x : ℝ) ↦ x ^ (re 0 - 1)
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ HPow.hPow (β := ℂ) (↑x : ℂ) 0) fun (x : ℝ) ↦
    x ^ (re 0 - 1)
have inl₁ : Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ 0) fun (x : ℝ) ↦ x ^ (re 0 - 1)
Tactic: simp_rw [cpow_zero, deriv_const', Asymptotics.isBigO_zero]