awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
y : ℂ
h : y ≠ 0
⊢ (𝓝 y).EventuallyEq (β := ℂ) (fun (x : ℂ) ↦ 0) fun (y : ℂ) ↦ HPow.hPow (α := ℂ) 0 y

Tactic:
(isOpen_ne.eventually_mem h).mono fun y hy => (zero_cpow hy).symm

Premises used: IsOpen.eventually_mem, Filter.EventuallyEq, Filter.Eventually.mono, Complex.zero_cpow, isOpen_ne, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
y : ℂ
h : y ≠ 0
⊢ (𝓝 y).EventuallyEq (β := ℂ) (fun (x : ℂ) ↦ 0) fun (y : ℂ) ↦ HPow.hPow (α := ℂ) 0 y

Tactic:
exact (isOpen_ne.eventually_mem h).mono fun y hy => (zero_cpow hy).symm

Premises used: IsOpen.eventually_mem, Filter.Eventually.mono, Complex.zero_cpow, isOpen_ne, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x y : ℂ
h : x ≠ 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ HasStrictDerivAt (fun (y : ℂ) ↦ x ^ y) (x ^ y * log x) y

Tactic:
simpa only [cpow_def_of_ne_zero hx, mul_one] using
      ((hasStrictDerivAt_id y).const_mul (log x)).cexp

Premises used: Complex.log, HasStrictDerivAt.const_mul, HasStrictDerivAt.cexp, mul_one, Complex.cpow_def_of_ne_zero, hasStrictDerivAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℂ × ℂ
hp : p.1 ∈ slitPlane
⊢ HasFDerivAt (fun (x : ℂ × ℂ) ↦ x.1 ^ x.2)
    (HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℂ ℂ ℂ) +
      HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℂ ℂ ℂ))
    p

Tactic:
(hasStrictFDerivAt_cpow hp).hasFDerivAt

Premises used: Complex.hasStrictFDerivAt_cpow, HasStrictFDerivAt.hasFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
f' g' : StrongDual ℂ E
x : E
hf : HasStrictFDerivAt f f' x
hg : HasStrictFDerivAt g g' x
h0 : f x ∈ slitPlane
⊢ HasStrictFDerivAt (fun (x : E) ↦ f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x

Tactic:
(hasStrictFDerivAt_cpow (p := (f x, g x)) h0).comp x (hf.prodMk hg)

Premises used: ContinuousLinearMap.comp, HasStrictFDerivAt.prodMk, HasStrictFDerivAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
f' : StrongDual ℂ E
x : E
c : ℂ
hf : HasStrictFDerivAt f f' x
h0 : c ≠ 0 ∨ f x ≠ 0
⊢ HasStrictFDerivAt (fun (x : E) ↦ c ^ f x) ((c ^ f x * Complex.log c) • f') x

Tactic:
(hasStrictDerivAt_const_cpow h0).comp_hasStrictFDerivAt x hf

Premises used: Complex.hasStrictDerivAt_const_cpow, HasStrictDerivAt.comp_hasStrictFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
f' g' : StrongDual ℂ E
x : E
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
h0 : f x ∈ slitPlane
⊢ HasFDerivAt ((fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) ∘ fun (x : E) ↦ (f x, g x))
    ((HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ)
          (((fun (x : E) ↦ (f x, g x)) x).2 *
            HPow.hPow (α := ℂ) ((fun (x : E) ↦ (f x, g x)) x).1 (HSub.hSub (α := ℂ) ((fun (x : E) ↦ (f x, g x)) x).2 1))
          (ContinuousLinearMap.fst ℂ ℂ ℂ) +
        HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ)
          (HPow.hPow (α := ℂ) (β := ℂ) ((fun (x : E) ↦ (f x, g x)) x).1 ((fun (x : E) ↦ (f x, g x)) x).2 *
            Complex.log ((fun (x : E) ↦ (f x, g x)) x).1)
          (ContinuousLinearMap.snd ℂ ℂ ℂ)) ∘SL
      ContinuousLinearMap.prod f' g')
    x

Tactic:
(@Complex.hasFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp x (hf.prodMk hg)

Premises used: HasFDerivAt.prodMk, HasFDerivAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
f' g' : StrongDual ℂ E
x : E
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
h0 : f x ∈ slitPlane
⊢ HasFDerivAt (fun (x : E) ↦ f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x

Tactic:
convert! (@Complex.hasFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp x (hf.prodMk hg)

Premises used: HasFDerivAt.prodMk, HasFDerivAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
f' : StrongDual ℂ E
x : E
c : ℂ
hf : HasFDerivAt f f' x
h0 : c ≠ 0 ∨ f x ≠ 0
⊢ HasFDerivAt (fun (x : E) ↦ c ^ f x) ((c ^ f x * Complex.log c) • f') x

Tactic:
(hasStrictDerivAt_const_cpow h0).hasDerivAt.comp_hasFDerivAt x hf

Premises used: Complex.hasStrictDerivAt_const_cpow, HasStrictDerivAt.hasDerivAt, HasDerivAt.comp_hasFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
f' g' : StrongDual ℂ E
x : E
s : Set E
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt g g' s x
h0 : f x ∈ slitPlane
⊢ HasFDerivWithinAt ((fun (x : ℂ × ℂ) ↦ x.1 ^ x.2) ∘ fun (x : E) ↦ (f x, g x))
    ((HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ)
          (((fun (x : E) ↦ (f x, g x)) x).2 *
            HPow.hPow (α := ℂ) ((fun (x : E) ↦ (f x, g x)) x).1 (HSub.hSub (α := ℂ) ((fun (x : E) ↦ (f x, g x)) x).2 1))
          (ContinuousLinearMap.fst ℂ ℂ ℂ) +
        HSMul.hSMul (β := ℂ × ℂ →L[ℂ] ℂ)
          (HPow.hPow (α := ℂ) (β := ℂ) ((fun (x : E) ↦ (f x, g x)) x).1 ((fun (x : E) ↦ (f x, g x)) x).2 *
            Complex.log ((fun (x : E) ↦ (f x, g x)) x).1)
          (ContinuousLinearMap.snd ℂ ℂ ℂ)) ∘SL
      ContinuousLinearMap.prod f' g')
    s x

Tactic:
(@Complex.hasFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp_hasFDerivWithinAt x (hf.prodMk hg)

Premises used: HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
f' g' : StrongDual ℂ E
x : E
s : Set E
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt g g' s x
h0 : f x ∈ slitPlane
⊢ HasFDerivWithinAt (fun (x : E) ↦ f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') s x

Tactic:
convert!
    (@Complex.hasFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp_hasFDerivWithinAt x (hf.prodMk hg)

Premises used: HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
f' : StrongDual ℂ E
x : E
s : Set E
c : ℂ
hf : HasFDerivWithinAt f f' s x
h0 : c ≠ 0 ∨ f x ≠ 0
⊢ HasFDerivWithinAt (fun (x : E) ↦ c ^ f x) ((c ^ f x * Complex.log c) • f') s x

Tactic:
(hasStrictDerivAt_const_cpow h0).hasDerivAt.comp_hasFDerivWithinAt x hf

Premises used: HasDerivAt.comp_hasFDerivWithinAt, Complex.hasStrictDerivAt_const_cpow, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
x : E
hf : DifferentiableAt ℂ f x
hg : DifferentiableAt ℂ g x
h0 : f x ∈ slitPlane
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x : E) ↦ f x ^ g x) x

Tactic:
(hf.hasFDerivAt.cpow hg.hasFDerivAt h0).differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
x : E
c : ℂ
hf : DifferentiableAt ℂ f x
h0 : c ≠ 0 ∨ f x ≠ 0
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x : E) ↦ c ^ f x) x

Tactic:
(hf.hasFDerivAt.const_cpow h0).differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.const_cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
x : E
c : ℂ
hf : DifferentiableAt ℂ f x
h0 : f x ∈ slitPlane
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x : E) ↦ f x ^ c) x

Tactic:
hf.cpow (differentiableAt_const c) h0

Premises used: differentiableAt_const, DifferentiableAt.cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
x : E
s : Set E
hf : DifferentiableWithinAt ℂ f s x
hg : DifferentiableWithinAt ℂ g s x
h0 : f x ∈ slitPlane
⊢ DifferentiableWithinAt ℂ (F := ℂ) (fun (x : E) ↦ f x ^ g x) s x

Tactic:
(hf.hasFDerivWithinAt.cpow hg.hasFDerivWithinAt h0).differentiableWithinAt

Premises used: HasFDerivWithinAt.cpow, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
x : E
s : Set E
c : ℂ
hf : DifferentiableWithinAt ℂ f s x
h0 : c ≠ 0 ∨ f x ≠ 0
⊢ DifferentiableWithinAt ℂ (F := ℂ) (fun (x : E) ↦ c ^ f x) s x

Tactic:
(hf.hasFDerivWithinAt.const_cpow h0).differentiableWithinAt

Premises used: HasFDerivWithinAt.differentiableWithinAt, HasFDerivWithinAt.const_cpow, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
x : E
s : Set E
c : ℂ
hf : DifferentiableWithinAt ℂ f s x
h0 : f x ∈ slitPlane
⊢ DifferentiableWithinAt ℂ (F := ℂ) (fun (x : E) ↦ f x ^ c) s x

Tactic:
hf.cpow (differentiableWithinAt_const c) h0

Premises used: differentiableWithinAt_const, DifferentiableWithinAt.cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
s : Set E
hf : DifferentiableOn ℂ f s
hg : DifferentiableOn ℂ g s
h0 : Set.MapsTo f s slitPlane
⊢ DifferentiableOn ℂ (F := ℂ) (fun (x : E) ↦ f x ^ g x) s

Tactic:
fun x hx ↦ (hf x hx).cpow (hg x hx) (h0 hx)

Premises used: DifferentiableWithinAt.cpow, DifferentiableOn
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
s : Set E
c : ℂ
hf : DifferentiableOn ℂ f s
h0 : c ≠ 0 ∨ ∀ x ∈ s, f x ≠ 0
⊢ DifferentiableOn ℂ (F := ℂ) (fun (x : E) ↦ c ^ f x) s

Tactic:
fun x hx ↦ (hf x hx).const_cpow (h0.imp_right fun h ↦ h x hx)

Premises used: DifferentiableWithinAt.const_cpow, DifferentiableOn, Or.imp_right
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
s : Set E
c : ℂ
hf : DifferentiableOn ℂ f s
h0 : ∀ x ∈ s, f x ∈ slitPlane
⊢ DifferentiableOn ℂ (F := ℂ) (fun (x : E) ↦ f x ^ c) s

Tactic:
hf.cpow (differentiableOn_const c) h0

Premises used: DifferentiableOn.cpow, differentiableOn_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : E → ℂ
hf : Differentiable ℂ f
hg : Differentiable ℂ g
h0 : ∀ (x : E), f x ∈ slitPlane
⊢ Differentiable ℂ (F := ℂ) fun (x : E) ↦ f x ^ g x

Tactic:
fun x ↦ (hf x).cpow (hg x) (h0 x)

Premises used: Differentiable, DifferentiableAt.cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : E → ℂ
c : ℂ
hf : Differentiable ℂ f
h0 : c ≠ 0 ∨ ∀ (x : E), f x ≠ 0
⊢ Differentiable ℂ (F := ℂ) fun (x : E) ↦ c ^ f x

Tactic:
fun x ↦ (hf x).const_cpow (h0.imp_right fun h ↦ h x)

Premises used: Differentiable, DifferentiableAt.const_cpow, Or.imp_right
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
z : ℂ
inst : NeZero z
⊢ Differentiable ℂ (F := ℂ) fun (s : ℂ) ↦ z ^ s

Tactic:
differentiable_id.const_cpow (.inl <| NeZero.ne z)

Premises used: Or.inl, differentiable_id, Differentiable.const_cpow, NeZero.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
z : ℂ
inst : NeZero z
t : ℂ
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ z ^ s) t

Tactic:
differentiableAt_id.const_cpow (.inl <| NeZero.ne z)

Premises used: DifferentiableAt.const_cpow, Or.inl, differentiableAt_id, NeZero.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f g : ℂ → ℂ
f' g' x : ℂ
⊢ (HSMul.hSMul (β := ℂ →L[ℂ] ℂ) (g x * f x ^ (g x - 1)) (ContinuousLinearMap.smulRight (S := ℂ) 1 f') +
          HSMul.hSMul (β := ℂ →L[ℂ] ℂ) (f x ^ g x * log (f x)) (ContinuousLinearMap.smulRight (S := ℂ) 1 g') :
        (a : ℂ) → ℂ)
      1 =
    g x * f x ^ (g x - 1) * f' + f x ^ g x * log (f x) * g'

Tactic:
simp only [smul_eq_mul, one_mul, ContinuousLinearMap.one_apply,
    ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.add_apply, Pi.smul_apply,
    ContinuousLinearMap.coe_smul']

Premises used: ContinuousLinearMap.coe_smul', ContinuousLinearMap.add_apply, ContinuousLinearMap.one_apply, smul_eq_mul, ContinuousLinearMap.smulRight_apply, one_mul, Pi.smul_apply
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f g : ℂ → ℂ
f' g' x : ℂ
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
h0 : f x ∈ slitPlane
⊢ HasStrictDerivAt (fun (x : ℂ) ↦ f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x

Tactic:
simpa using (hf.hasStrictFDerivAt.cpow hg h0).hasStrictDerivAt

Premises used: HasStrictDerivAt.hasStrictFDerivAt, HasStrictFDerivAt.hasStrictDerivAt, HasStrictFDerivAt.cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
f' x c : ℂ
hf : HasStrictDerivAt f f' x
h : c ≠ 0 ∨ f x ≠ 0
⊢ HasStrictDerivAt (fun (x : ℂ) ↦ c ^ f x) (c ^ f x * Complex.log c * f') x

Tactic:
(hasStrictDerivAt_const_cpow h).comp x hf

Premises used: Complex.hasStrictDerivAt_const_cpow, HasStrictDerivAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x c : ℂ
h : x ∈ slitPlane
⊢ HasStrictDerivAt (fun (z : ℂ) ↦ z ^ c) (c * x ^ (c - 1)) x

Tactic:
simpa only [mul_zero, add_zero, mul_one] using
    (hasStrictDerivAt_id x).cpow (hasStrictDerivAt_const x c) h

Premises used: HasStrictDerivAt.cpow, MulZeroClass.mul_zero, hasStrictDerivAt_const, mul_one, add_zero, hasStrictDerivAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
f' x c : ℂ
hf : HasStrictDerivAt f f' x
h0 : f x ∈ slitPlane
⊢ HasStrictDerivAt (fun (x : ℂ) ↦ f x ^ c) (c * f x ^ (c - 1) * f') x

Tactic:
(Complex.hasStrictDerivAt_cpow_const h0).comp x hf

Premises used: HasStrictDerivAt.comp, Complex.hasStrictDerivAt_cpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f g : ℂ → ℂ
f' g' x : ℂ
hf : HasDerivAt f f' x
hg : HasDerivAt g g' x
h0 : f x ∈ slitPlane
⊢ HasDerivAt (fun (x : ℂ) ↦ f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x

Tactic:
simpa [aux] using (hf.hasFDerivAt.cpow hg h0).hasDerivAt

Premises used: HasDerivAt.hasFDerivAt, HasFDerivAt.hasDerivAt, _private.0.aux, HasFDerivAt.cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
f' x c : ℂ
hf : HasDerivAt f f' x
h0 : c ≠ 0 ∨ f x ≠ 0
⊢ HasDerivAt (fun (x : ℂ) ↦ c ^ f x) (c ^ f x * Complex.log c * f') x

Tactic:
(hasStrictDerivAt_const_cpow h0).hasDerivAt.comp x hf

Premises used: HasDerivAt.comp, Complex.hasStrictDerivAt_const_cpow, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
f' x c : ℂ
hf : HasDerivAt f f' x
h0 : f x ∈ slitPlane
⊢ HasDerivAt (fun (x : ℂ) ↦ f x ^ c) (c * f x ^ (c - 1) * f') x

Tactic:
(Complex.hasStrictDerivAt_cpow_const h0).hasDerivAt.comp x hf

Premises used: HasDerivAt.comp, Complex.hasStrictDerivAt_cpow_const, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f g : ℂ → ℂ
s : Set ℂ
f' g' x : ℂ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h0 : f x ∈ slitPlane
⊢ HasDerivWithinAt (fun (x : ℂ) ↦ f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') s x

Tactic:
simpa [aux] using (hf.hasFDerivWithinAt.cpow hg h0).hasDerivWithinAt

Premises used: HasDerivWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.cpow, HasFDerivWithinAt.hasDerivWithinAt, _private.0.aux
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
s : Set ℂ
f' x c : ℂ
hf : HasDerivWithinAt f f' s x
h0 : c ≠ 0 ∨ f x ≠ 0
⊢ HasDerivWithinAt (fun (x : ℂ) ↦ c ^ f x) (c ^ f x * Complex.log c * f') s x

Tactic:
(hasStrictDerivAt_const_cpow h0).hasDerivAt.comp_hasDerivWithinAt x hf

Premises used: Complex.hasStrictDerivAt_const_cpow, HasDerivAt.comp_hasDerivWithinAt, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
s : Set ℂ
f' x c : ℂ
hf : HasDerivWithinAt f f' s x
h0 : f x ∈ slitPlane
⊢ HasDerivWithinAt (fun (x : ℂ) ↦ f x ^ c) (c * f x ^ (c - 1) * f') s x

Tactic:
(Complex.hasStrictDerivAt_cpow_const h0).hasDerivAt.comp_hasDerivWithinAt x hf

Premises used: HasDerivAt.comp_hasDerivWithinAt, Complex.hasStrictDerivAt_cpow_const, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
pos : ∀ (h : UniqueDiffWithinAt ℂ s x), derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
neg : ∀ (h : ¬UniqueDiffWithinAt ℂ s x), derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
⊢ derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x

Tactic:
by_cases h : UniqueDiffWithinAt ℂ s x

Premises used: UniqueDiffWithinAt, Complex
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : ¬UniqueDiffWithinAt ℂ s x
neg : 0 = log c * derivWithin f s x * c ^ f x
neg₁ : 0 = log c * 0 * c ^ f x
neg₂ : 0 = 0 * c ^ f x
neg₃ neg₄ : Eq (α := ℂ) 0 0
⊢ derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x

Tactic:
rw [derivWithin_zero_of_not_uniqueDiffWithinAt h,
      derivWithin_zero_of_not_uniqueDiffWithinAt h, mul_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, derivWithin_zero_of_not_uniqueDiffWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
pos : ∀ (hc : c = 0), derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
neg : ∀ (hc : ¬c = 0), derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x
⊢ derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
hc : ¬c = 0
neg : derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = c ^ f x * log c * derivWithin f s x
⊢ derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x

Tactic:
rw [mul_comm, ← mul_assoc]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
hc : ¬c = 0
⊢ derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = c ^ f x * log c * derivWithin f s x

Tactic:
(hf.hasDerivWithinAt.const_cpow (Or.inl hc)).derivWithin h

Premises used: HasDerivWithinAt.const_cpow, DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
hc : ¬c = 0
⊢ derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = c ^ f x * log c * derivWithin f s x

Tactic:
exact (hf.hasDerivWithinAt.const_cpow (Or.inl hc)).derivWithin h

Premises used: HasDerivWithinAt.const_cpow, DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, Or.inl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
hc : c = 0
⊢ (𝓝[s \ {x}] x).NeBot

Tactic:
rw [uniqueDiffWithinAt_iff_accPt, accPt_principal_iff_nhdsWithin] at h

Premises used: uniqueDiffWithinAt_iff_accPt, accPt_principal_iff_nhdsWithin
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : UniqueDiffWithinAt ℂ s x
hc : c = 0
h₁ : (𝓝[s \ {x}] x).NeBot
⊢ c = 0

Tactic:
rw [uniqueDiffWithinAt_iff_accPt, accPt_principal_iff_nhdsWithin] at h

Premises used: uniqueDiffWithinAt_iff_accPt, accPt_principal_iff_nhdsWithin
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : (𝓝[s \ {x}] x).NeBot
hc : c = 0
pos : Eq (α := ℂ) (derivWithin (fun (x : ℂ) ↦ HPow.hPow (α := ℂ) 0 (f x)) s x) 0
⊢ derivWithin (fun (x : ℂ) ↦ c ^ f x) s x = log c * derivWithin f s x * c ^ f x

Tactic:
simp only [hc, log_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, Complex.log_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : (𝓝[s \ {x}] x).NeBot
hc : c = 0
⊢ ¬Set.Infinite (α := ℂ) {0, 1}

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : (𝓝[s \ {x}] x).NeBot
hc : c = 0
pos : ∃ᶠ (y : ℂ) in 𝓝[s \ {x}] x, Membership.mem (γ := Set ℂ) {0, 1} (HPow.hPow (α := ℂ) 0 (f y))
⊢ Eq (α := ℂ) (derivWithin (fun (x : ℂ) ↦ HPow.hPow (α := ℂ) 0 (f x)) s x) 0

Tactic:
apply derivWithin_zero_of_frequently_mem {0, 1} (mt Set.Infinite.of_accPt (by simp))

Premises used: derivWithin_zero_of_frequently_mem, mt, Set.Infinite.of_accPt, Insert.insert, Singleton.singleton, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
s : Set ℂ
x : ℂ
hf : DifferentiableWithinAt ℂ f s x
c : ℂ
h : (𝓝[s \ {x}] x).NeBot
hc : c = 0
⊢ ∃ᶠ (y : ℂ) in 𝓝[s \ {x}] x, Membership.mem (γ := Set ℂ) {0, 1} (HPow.hPow (α := ℂ) 0 (f y))

Tactic:
simpa [zero_cpow_eq_iff, em']

Premises used: Complex.zero_cpow_eq_iff, em'
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
x : ℂ
hf : DifferentiableAt ℂ f x
c : ℂ
hf₁ : DifferentiableWithinAt ℂ f Set.univ x
⊢ deriv (fun (x : ℂ) ↦ c ^ f x) x = log c * deriv f x * c ^ f x

Tactic:
rw [← derivWithin_univ, derivWithin_const_cpow, derivWithin_univ]

Premises used: derivWithin_univ, Complex.derivWithin_const_cpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℂ → ℂ
x : ℂ
hf : DifferentiableAt ℂ f x
c : ℂ
hf₁ hf₂ hf₃ hf₄ : DifferentiableAt ℂ f x
⊢ DifferentiableWithinAt ℂ f Set.univ x

Tactic:
rwa [differentiableWithinAt_univ]

Premises used: differentiableWithinAt_univ
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx : x ≠ 0
r : ℂ
hr : r ≠ -1
⊢ r + 1 ≠ 0

Tactic:
rw [Ne, ← add_eq_zero_iff_eq_neg, ← Ne] at hr

Premises used: add_eq_zero_iff_eq_neg, Ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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
inr : ∀ (hx : x < 0), HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) x
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) x

Tactic:
rcases lt_or_gt_of_ne hx.symm with (hx | hx)

Premises used: lt_or_gt_of_ne, Ne.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
r : ℂ
hr : r + 1 ≠ 0
hx : 0 < x
inl : HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℝ) ↦ (↑y : ℂ) ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) x

Tactic:
apply HasDerivAt.comp_ofReal (e := fun y => (y : ℂ) ^ (r + 1) / (r + 1))

Premises used: HasDerivAt.comp_ofReal
-- 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 * (r + 1) / (r + 1)) (↑x : ℂ)

Tactic:
HasDerivAt.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 : 0 < x
h : (↑x : ℂ) ^ r = (↑x : ℂ) ^ r * (r + 1) / (r + 1)
inl : ℂ
inl₁ : HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1)) ((↑x : ℂ) ^ r * (r + 1)) (↑x : ℂ)
⊢ HasDerivAt (fun (y : ℂ) ↦ y ^ (r + 1) / (r + 1)) ((↑x : ℂ) ^ r) (↑x : ℂ)

Tactic:
convert! HasDerivAt.div_const (𝕜 := ℂ) ?_ (r + 1) using 1

Premises used: HAdd.hAdd, HasDerivAt.div_const, OfNat.ofNat