awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ (↑x : ℂ) ^ r = (↑x : ℂ) ^ r * (r + 1) / (r + 1)

Tactic:
(mul_div_cancel_right₀ _ hr).symm

Premises used: mul_div_cancel_right₀, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ (↑x : ℂ) ^ r = (↑x : ℂ) ^ r * (r + 1) / (r + 1)

Tactic:
exact (mul_div_cancel_right₀ _ hr).symm

Premises used: mul_div_cancel_right₀, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (fun (x : ℂ) ↦ x ^ (r + 1)) ((r + 1) * (↑x : ℂ) ^ (r + 1 - 1) * 1) (↑x : ℂ)

Tactic:
HasDerivAt.cpow_const ?_ ?_

Premises used: HasDerivAt.cpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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 : ℂ)
inl₂ : (↑x : ℂ) ∈ slitPlane
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1)) ((↑x : ℂ) ^ r * (r + 1)) (↑x : ℂ)

Tactic:
convert! HasDerivAt.cpow_const ?_ ?_ using 1

Premises used: HasDerivAt.cpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
h : (r + 1) * (↑x : ℂ) ^ r = (r + 1) * (↑x : ℂ) ^ r * 1
⊢ (↑x : ℂ) ^ r * (r + 1) = (r + 1) * (↑x : ℂ) ^ (r + 1 - 1) * 1

Tactic:
rw [add_sub_cancel_right, mul_comm]

Premises used: mul_comm, add_sub_cancel_right
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ (r + 1) * (↑x : ℂ) ^ r = (r + 1) * (↑x : ℂ) ^ r * 1

Tactic:
(mul_one _).symm

Premises used: mul_one, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ (r + 1) * (↑x : ℂ) ^ r = (r + 1) * (↑x : ℂ) ^ r * 1

Tactic:
exact (mul_one _).symm

Premises used: mul_one, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (F := ℂ) (fun (y : ℂ) ↦ y) 1 (↑x : ℂ)

Tactic:
hasDerivAt_id (x : ℂ)

Premises used: Complex.ofReal, hasDerivAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ HasDerivAt (F := ℂ) (fun (y : ℂ) ↦ y) 1 (↑x : ℂ)

Tactic:
exact hasDerivAt_id (x : ℂ)

Premises used: Complex.ofReal, hasDerivAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
⊢ (↑x : ℂ) ∈ slitPlane

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)

Tactic:
Filter.eventually_of_mem (Iio_mem_nhds hx) fun y hy => ?_

Premises used: Iio_mem_nhds, Filter.eventually_of_mem
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
refine :
  ∀ (y : ℝ) (hy : Membership.mem (γ := Set ℝ) (Set.Iio 0) y),
    (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
⊢ ∀ᶠ (y : ℝ) in 𝓝 x, (↑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 => ?_

Premises used: Iio_mem_nhds, Filter.eventually_of_mem
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : x < 0
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Iio 0) y
rw rw₁ :
  (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1) =
    (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)
⊢ (↑y : ℂ) ^ (r + 1) / (r + 1) = (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)

Tactic:
rw [ofReal_cpow_of_nonpos (le_of_lt hy)]

Premises used: Complex.ofReal_cpow_of_nonpos, le_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)

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)]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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

Tactic:
HasDerivAt.congr_of_eventuallyEq ?_ this

Premises used: HasDerivAt.congr_of_eventuallyEq
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)
inr : HasDerivAt (fun (x : ℝ) ↦ (-(↑x : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1)) ((↑x : ℂ) ^ r) x
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) x

Tactic:
refine HasDerivAt.congr_of_eventuallyEq ?_ this

Premises used: HasDerivAt.congr_of_eventuallyEq
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)
inr :
  HasDerivAt (fun (x : ℝ) ↦ (-(↑x : ℂ)) ^ (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) x

Tactic:
rw [ofReal_cpow_of_nonpos (le_of_lt hx)]

Premises used: Complex.ofReal_cpow_of_nonpos, le_of_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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))
    ((r + 1) * (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r) / (r + 1)) x

Tactic:
this.div_const (r + 1)

Premises used: HAdd.hAdd, HasDerivAt.div_const, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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
h : (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r) = (r + 1) * (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r) / (r + 1)
⊢ HasDerivAt (fun (x : ℝ) ↦ (-(↑x : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)) / (r + 1))
    ((-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r)) x

Tactic:
convert! this.div_const (r + 1) using 1

Premises used: HAdd.hAdd, HasDerivAt.div_const, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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
rw : (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r)
| (r + 1) * (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r) / (r + 1)

Tactic:
rw [mul_assoc, mul_comm, mul_div_cancel_right₀ _ hr]

Premises used: mul_assoc, mul_div_cancel_right₀, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)
h : (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r) = (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r)
⊢ (-(↑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]

Premises used: mul_assoc, mul_div_cancel_right₀, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)
inr :
  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

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]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)
inr :
  HasDerivAt (fun (y : ℝ) ↦ (-(↑y : ℂ)) ^ (r + 1) * -cexp ((↑π : ℂ) * I * r))
    ((r + 1) * (-(↑x : ℂ)) ^ r * cexp ((↑π : ℂ) * I * r)) x
⊢ HasDerivAt (fun (y : ℝ) ↦ (-(↑y : ℂ)) ^ (r + 1) * cexp ((↑π : ℂ) * I * (r + 1)))
    ((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]

Premises used: Real.pi, HMul.hMul, Complex.exp_add, neg_one_mul, Complex.ofReal, Complex.exp_pi_mul_I, mul_comm, mul_add, mul_one, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)
inr :
  HasDerivAt (fun (y : ℝ) ↦ -(↑(-y) : ℂ) ^ (r + 1) * cexp ((↑π : ℂ) * I * r))
    ((r + 1) * (↑(-x) : ℂ) ^ r * cexp ((↑π : ℂ) * I * r)) x
⊢ 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]

Premises used: Complex.ofReal_neg, neg_mul, mul_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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 : ℝ) ↦ (-fun (y : ℝ) ↦ (↑(-y) : ℂ) ^ (r + 1)) y * cexp ((↑π : ℂ) * I * r))
    (-(-(r + 1) * (↑(-x) : ℂ) ^ r) * cexp ((↑π : ℂ) * I * r)) x

Tactic:
this.neg.mul_const _

Premises used: HasDerivAt.neg, HasDerivAt.mul_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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
h : (r + 1) * (↑(-x) : ℂ) ^ r * cexp ((↑π : ℂ) * I * r) = -(-(r + 1) * (↑(-x) : ℂ) ^ r) * cexp ((↑π : ℂ) * I * r)
⊢ HasDerivAt (fun (y : ℝ) ↦ -(↑(-y) : ℂ) ^ (r + 1) * cexp ((↑π : ℂ) * I * r))
    ((r + 1) * (↑(-x) : ℂ) ^ r * cexp ((↑π : ℂ) * I * r)) x

Tactic:
convert! this.neg.mul_const _ using 1

Premises used: HasDerivAt.neg, HasDerivAt.mul_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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 * cexp ((↑π : ℂ) * I * r) = -(-(r + 1) * (↑(-x) : ℂ) ^ r) * cexp ((↑π : ℂ) * I * r)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)
inr : 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

Tactic:
suffices HasDerivAt (fun y : ℝ => (↑(-y) : ℂ) ^ (r + 1)) (-(r + 1) * ↑(-x) ^ r) x by
      convert! this.neg.mul_const _ using 1; ring
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)) ∘ Neg.neg) (HSMul.hSMul (α := ℝ) (-1) ((r + 1) * (↑(-x) : ℂ) ^ r)) x

Tactic:
@HasDerivAt.scomp ℝ _ ℂ _ _ x ℝ _ _ _ _ _ _ _ _ this (hasDerivAt_neg x)

Premises used: HasDerivAt.scomp, hasDerivAt_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)
h : -(r + 1) * (↑(-x) : ℂ) ^ r = HSMul.hSMul (α := ℝ) (-1) ((r + 1) * (↑(-x) : ℂ) ^ r)
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑(-y) : ℂ) ^ (r + 1)) (-(r + 1) * (↑(-x) : ℂ) ^ r) x

Tactic:
convert! @HasDerivAt.scomp ℝ _ ℂ _ _ x ℝ _ _ _ _ _ _ _ _ this (hasDerivAt_neg x) using 1

Premises used: HasDerivAt.scomp, hasDerivAt_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)
h : -(r + 1) * (↑(-x) : ℂ) ^ r = -1 * ((r + 1) * (↑(-x) : ℂ) ^ r)
⊢ -(r + 1) * (↑(-x) : ℂ) ^ r = HSMul.hSMul (α := ℝ) (-1) ((r + 1) * (↑(-x) : ℂ) ^ r)

Tactic:
rw [real_smul, ofReal_neg 1, ofReal_one]

Premises used: Complex.real_smul, Complex.ofReal_neg, Complex.ofReal_one, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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 = -1 * ((r + 1) * (↑(-x) : ℂ) ^ r)

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)
inr : HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ (r + 1)) ((r + 1) * (↑(-x) : ℂ) ^ r) (-x)
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)

Tactic:
this.comp_ofReal

Premises used: HasDerivAt.comp_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)

Tactic:
exact this.comp_ofReal

Premises used: HasDerivAt.comp_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)
inr : HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1)) ((r + 1) * (↑(-x) : ℂ) ^ r) (↑(-x) : ℂ)
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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 : ℂ
⊢ r = r + 1 - 1

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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 : ℂ
rw : y ^ (r + 1 - 1 + 1)
| y ^ (r + 1)

Tactic:
rw [(by ring : r = r + 1 - 1)]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)
inr : HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1 - 1 + 1)) ((r + 1) * (↑(-x) : ℂ) ^ r) (↑(-x) : ℂ)
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1)) ((r + 1) * (↑(-x) : ℂ) ^ r) (↑(-x) : ℂ)

Tactic:
conv in ↑_ ^ _ => rw [(by ring : r = r + 1 - 1)]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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 - 1 + 1)) ((r + 1 - 1 + 1) * (↑(-x) : ℂ) ^ (r + 1 - 1 + 1 - 1) * 1) (↑(-x) : ℂ)

Tactic:
HasDerivAt.cpow_const ?_ ?_

Premises used: HasDerivAt.cpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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) : ℂ)
inr₂ : (↑(-x) : ℂ) ∈ slitPlane
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1 - 1 + 1)) ((r + 1) * (↑(-x) : ℂ) ^ r) (↑(-x) : ℂ)

Tactic:
convert! HasDerivAt.cpow_const ?_ ?_ using 1

Premises used: HasDerivAt.cpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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) * (↑(-x) : ℂ) ^ r * 1
⊢ (r + 1) * (↑(-x) : ℂ) ^ r = (r + 1 - 1 + 1) * (↑(-x) : ℂ) ^ (r + 1 - 1 + 1 - 1) * 1

Tactic:
rw [add_sub_cancel_right, add_sub_cancel_right]

Premises used: add_sub_cancel_right
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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) * (↑(-x) : ℂ) ^ r * 1

Tactic:
(mul_one _).symm

Premises used: mul_one, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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) * (↑(-x) : ℂ) ^ r * 1

Tactic:
exact (mul_one _).symm

Premises used: mul_one, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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 (F := ℂ) (fun (y : ℂ) ↦ y) 1 (↑(-x) : ℂ)

Tactic:
hasDerivAt_id ((-x : ℝ) : ℂ)

Premises used: Complex.ofReal, hasDerivAt_id, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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 (F := ℂ) (fun (y : ℂ) ↦ y) 1 (↑(-x) : ℂ)

Tactic:
exact hasDerivAt_id ((-x : ℝ) : ℂ)

Premises used: Complex.ofReal, hasDerivAt_id, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)
⊢ (↑(-x) : ℂ) ∈ slitPlane

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ 0
rwa : ¬r - 1 = -1
a : ℂ
rwa₁ : ¬r = 0
rwa₂ : ℂ
rwa₃ : ¬r = 0
rwa₄ : ℂ
rwa₅ : ¬r = 0
rwa₆ : ℂ
rwa₇ : ¬r = 0
rwa₈ : ℂ
⊢ r - 1 ≠ -1

Tactic:
rwa [ne_eq, sub_eq_neg_self]

Premises used: ne_eq, sub_eq_neg_self
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ 0
⊢ 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])
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ 0
this : HasDerivAt (fun (y : ℝ) ↦ r * ((↑y : ℂ) ^ (r - 1 + 1) / (r - 1 + 1))) (r * (↑x : ℂ) ^ (r - 1)) x
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ r) (r * (↑x : ℂ) ^ (r - 1)) x

Tactic:
simpa [sub_add_cancel, mul_div_cancel₀ _ hr] using this

Premises used: mul_div_cancel₀, sub_add_cancel
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
c : ℂ
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
h0 : f x ≠ 0
h1 : c ≠ 0
⊢ DifferentiableAt ℝ (F := ℂ) (fun (y : ℝ) ↦ (↑(f y) : ℂ) ^ c) x

Tactic:
(hasDerivAt_ofReal_cpow_const h0 h1).differentiableAt.comp x hf

Premises used: HasDerivAt.differentiableAt, hasDerivAt_ofReal_cpow_const, DifferentiableAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x c : ℂ
hx : x ∈ slitPlane
⊢ deriv (fun (x : ℂ) ↦ x ^ c) x = c * x ^ (c - 1)

Tactic:
(hasStrictDerivAt_cpow_const hx).hasDerivAt.deriv

Premises used: HasDerivAt.deriv, Complex.hasStrictDerivAt_cpow_const, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
c : ℂ
x : ℝ
hx : x ≠ 0
hc : c ≠ 0
⊢ deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ c) x = c * (↑x : ℂ) ^ (c - 1)

Tactic:
(hasDerivAt_ofReal_cpow_const hx hc).deriv

Premises used: HasDerivAt.deriv, hasDerivAt_ofReal_cpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
x c : ℂ
hf : DifferentiableAt ℂ f x
hx : f x ∈ slitPlane
⊢ deriv (fun (x : ℂ) ↦ f x ^ c) x = c * f x ^ (c - 1) * deriv f x

Tactic:
(hf.hasDerivAt.cpow_const hx).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.cpow_const