awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
c : ℂ
hc : c ≠ 0
x : ℝ
hx : x ≠ 0
rw rw₁ : c * (↑x : ℂ) ^ (c - 1) = c * (↑x : ℂ) ^ (c - 1)
⊢ deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ c) x = c * (↑x : ℂ) ^ (c - 1)

Tactic:
rw [deriv_ofReal_cpow_const hx hc]

Premises used: Complex.deriv_ofReal_cpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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
h₁ h₂ : ∀ (x : ℝ) (hx : x ≠ 0), deriv (fun (x : ℝ) ↦ (↑x : ℂ) ^ c) x = c * (↑x : ℂ) ^ (c - 1)
⊢ EventuallyEq (β := ℂ) atTop (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ c) fun (x : ℝ) ↦ c * (↑x : ℂ) ^ (c - 1)

Tactic:
filter_upwards [eventually_ne_atTop 0] with x hx using by rw [deriv_ofReal_cpow_const hx hc]

Premises used: Filter.eventually_ne_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
c : ℂ
hc : c ≠ 0
⊢ Asymptotics.IsTheta (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ c * (↑x : ℂ) ^ (c - 1)) fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (c - 1)‖

Tactic:
(Asymptotics.IsTheta.of_norm_eventuallyEq EventuallyEq.rfl).const_mul_left hc

Premises used: Asymptotics.IsTheta.const_mul_left, Asymptotics.IsTheta.of_norm_eventuallyEq, Filter.EventuallyEq.rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
c : ℂ
hc : c ≠ 0
h : ∀ (x : ℝ) (hx : 0 < x), ‖(↑x : ℂ) ^ (c - 1)‖ = x ^ (c.re - 1)
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (c - 1)‖) fun (x : ℝ) ↦ x ^ (c.re - 1)

Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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)
h₂ h₃ : x ^ (c.re - 1) = x ^ (c.re - 1)
⊢ ‖(↑x : ℂ) ^ (c - 1)‖ = x ^ (c.re - 1)

Tactic:
rw [norm_cpow_eq_rpow_re_of_pos hx, sub_re, one_re]

Premises used: Complex.sub_re, Complex.one_re, Complex.norm_cpow_eq_rpow_re_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
c : ℂ
hc : c ≠ 0
_ : EventuallyEq (β := ℂ) atTop (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ c) fun (x : ℝ) ↦ c * (↑x : ℂ) ^ (c - 1)
_₁ : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ (c - 1)‖) fun (x : ℝ) ↦ x ^ (c.re - 1)
⊢ Asymptotics.IsTheta (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ c) 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]

Premises used: Norm.norm, Asymptotics.IsTheta.const_mul_left, HMul.hMul, HSub.hSub, Asymptotics.IsTheta.of_norm_eventuallyEq, Complex.ofReal, Complex.re, Filter.atTop, HPow.hPow, Filter.EventuallyEq.rfl, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
c : ℂ
inl :
  Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ HPow.hPow (β := ℂ) (↑x : ℂ) 0) fun (x : ℝ) ↦
    x ^ (re 0 - 1)
inr :
  ∀ (hc : c ≠ 0),
    Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ c) fun (x : ℝ) ↦ x ^ (c.re - 1)
⊢ 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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
inl : Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ 1) fun (x : ℝ) ↦ x ^ (re 0 - 1)
inl₁ : Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (fun (x : ℝ) ↦ 0) fun (x : ℝ) ↦ x ^ (re 0 - 1)
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ HPow.hPow (β := ℂ) (↑x : ℂ) 0) fun (x : ℝ) ↦
    x ^ (re 0 - 1)

Tactic:
simp_rw [cpow_zero, deriv_const', Asymptotics.isBigO_zero]

Premises used: Asymptotics.isBigO_zero, deriv_const', Complex.cpow_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
c : ℂ
hc : c ≠ 0
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ c) fun (x : ℝ) ↦ x ^ (c.re - 1)

Tactic:
(isTheta_deriv_ofReal_cpow_const_atTop hc).1

Premises used: And.left, isTheta_deriv_ofReal_cpow_const_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
c : ℂ
hc : c ≠ 0
⊢ Asymptotics.IsBigO (E := ℂ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ (↑x : ℂ) ^ c) fun (x : ℝ) ↦ x ^ (c.re - 1)

Tactic:
exact (isTheta_deriv_ofReal_cpow_const_atTop hc).1

Premises used: And.left, isTheta_deriv_ofReal_cpow_const_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : 0 < p.1
⊢ (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)

Tactic:
have : (fun x : ℝ × ℝ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) :=
    (continuousAt_fst.eventually (lt_mem_nhds hp)).mono fun p hp => rpow_def_of_pos hp _
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : 0 < p.1
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)
⊢ HasStrictFDerivAt (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.congr_of_eventuallyEq ?_ this.symm

Premises used: HasStrictFDerivAt.congr_of_eventuallyEq, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : 0 < p.1
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)
refine :
  HasStrictFDerivAt (fun (x : ℝ × ℝ) ↦ rexp (log 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
⊢ HasStrictFDerivAt (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:
refine HasStrictFDerivAt.congr_of_eventuallyEq ?_ this.symm

Premises used: HasStrictFDerivAt.congr_of_eventuallyEq, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : 0 < p.1
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)
⊢ HasStrictFDerivAt (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2))
    (rexp (log p.1 * p.2) •
      (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
        p.2 • HSMul.hSMul (β := StrongDual ℝ (ℝ × ℝ)) p.1⁻¹ (ContinuousLinearMap.fst ℝ ℝ ℝ)))
    p

Tactic:
((hasStrictFDerivAt_fst.log hp.ne').fun_mul hasStrictFDerivAt_snd).exp

Premises used: HasStrictFDerivAt.log, hasStrictFDerivAt_snd, LT.lt.ne', HasStrictFDerivAt.fun_mul, HasStrictFDerivAt.exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : 0 < p.1
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2)
h :
  Eq (α := AddCommGroup (ℝ × ℝ)) Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule →
      Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace →
        HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
            HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) =
          rexp (log p.1 * p.2) •
            (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
              p.2 • HSMul.hSMul (β := StrongDual ℝ (ℝ × ℝ)) p.1⁻¹ (ContinuousLinearMap.fst ℝ ℝ ℝ))
⊢ HasStrictFDerivAt (fun (x : ℝ × ℝ) ↦ rexp (log 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:
convert! ((hasStrictFDerivAt_fst.log hp.ne').fun_mul hasStrictFDerivAt_snd).exp using 1

Premises used: HasStrictFDerivAt.log, hasStrictFDerivAt_snd, LT.lt.ne', HasStrictFDerivAt.fun_mul, HasStrictFDerivAt.exp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : p.1 < 0
⊢ (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)

Tactic:
have : (fun x : ℝ × ℝ => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => exp (log x.1 * x.2) * cos (x.2 * π) :=
    (continuousAt_fst.eventually (gt_mem_nhds hp)).mono fun p hp => rpow_def_of_neg hp _
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : p.1 < 0
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
⊢ HasStrictFDerivAt (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 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
        (ContinuousLinearMap.snd ℝ ℝ ℝ))
    p

Tactic:
HasStrictFDerivAt.congr_of_eventuallyEq ?_ this.symm

Premises used: HasStrictFDerivAt.congr_of_eventuallyEq, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : p.1 < 0
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
refine :
  HasStrictFDerivAt (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π))
    (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
        (ContinuousLinearMap.snd ℝ ℝ ℝ))
    p
⊢ HasStrictFDerivAt (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 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
        (ContinuousLinearMap.snd ℝ ℝ ℝ))
    p

Tactic:
refine HasStrictFDerivAt.congr_of_eventuallyEq ?_ this.symm

Premises used: HasStrictFDerivAt.congr_of_eventuallyEq, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : p.1 < 0
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
⊢ HasStrictFDerivAt (fun (i : ℝ × ℝ) ↦ rexp (log i.1 * i.2) * cos (i.2 * π))
    (rexp (log p.1 * p.2) • -sin (p.2 * π) • HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) π (ContinuousLinearMap.snd ℝ ℝ ℝ) +
      cos (p.2 * π) •
        rexp (log p.1 * p.2) •
          (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
            p.2 • HSMul.hSMul (β := StrongDual ℝ (ℝ × ℝ)) p.1⁻¹ (ContinuousLinearMap.fst ℝ ℝ ℝ)))
    p

Tactic:
((hasStrictFDerivAt_fst.log hp.ne).fun_mul hasStrictFDerivAt_snd).exp.fun_mul
      (hasStrictFDerivAt_snd.mul_const π).cos

Premises used: HasStrictFDerivAt.log, Real.pi, hasStrictFDerivAt_snd, HasStrictFDerivAt.cos, HasStrictFDerivAt.fun_mul, HasStrictFDerivAt.mul_const, HasStrictFDerivAt.exp, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : p.1 < 0
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
h :
  Eq (α := AddCommGroup (ℝ × ℝ)) Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule →
      Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace →
        instAddCommGroup = Ring.toAddCommGroup →
          HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
            HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
                HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
                  (ContinuousLinearMap.snd ℝ ℝ ℝ) =
              rexp (log p.1 * p.2) •
                  -sin (p.2 * π) • HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) π (ContinuousLinearMap.snd ℝ ℝ ℝ) +
                cos (p.2 * π) •
                  rexp (log p.1 * p.2) •
                    (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
                      p.2 • HSMul.hSMul (β := StrongDual ℝ (ℝ × ℝ)) p.1⁻¹ (ContinuousLinearMap.fst ℝ ℝ ℝ))
⊢ HasStrictFDerivAt (fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π))
    (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
        (ContinuousLinearMap.snd ℝ ℝ ℝ))
    p

Tactic:
convert!
    ((hasStrictFDerivAt_fst.log hp.ne).fun_mul hasStrictFDerivAt_snd).exp.fun_mul
      (hasStrictFDerivAt_snd.mul_const π).cos using 1

Premises used: HasStrictFDerivAt.log, Real.pi, hasStrictFDerivAt_snd, HasStrictFDerivAt.cos, HasStrictFDerivAt.fun_mul, HasStrictFDerivAt.mul_const, HasStrictFDerivAt.exp, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : p.1 < 0
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
e_4 : Eq (α := AddCommGroup (ℝ × ℝ)) Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule
e_6 : Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace
e_8 : instAddCommGroup = Ring.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
h :
  HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * (p.1 ^ p.2 / p.1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
        (ContinuousLinearMap.snd ℝ ℝ ℝ) =
    HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1)
        (ContinuousLinearMap.snd ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * p.2 * p.1⁻¹) (ContinuousLinearMap.fst ℝ ℝ ℝ)
⊢ HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * p.1 ^ (p.2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
        (ContinuousLinearMap.snd ℝ ℝ ℝ) =
    rexp (log p.1 * p.2) • -sin (p.2 * π) • HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) π (ContinuousLinearMap.snd ℝ ℝ ℝ) +
      cos (p.2 * π) •
        rexp (log p.1 * p.2) •
          (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (log p.1) (ContinuousLinearMap.snd ℝ ℝ ℝ) +
            p.2 • HSMul.hSMul (β := StrongDual ℝ (ℝ × ℝ)) p.1⁻¹ (ContinuousLinearMap.fst ℝ ℝ ℝ))

Tactic:
simp_rw [rpow_sub_one hp.ne, smul_add, ← add_assoc, smul_smul, ← add_smul, ← mul_assoc,
    mul_comm (cos _), ← rpow_def_of_neg hp]

Premises used: Real.cos, add_assoc, mul_assoc, smul_smul, Real.rpow_def_of_neg, Real.rpow_sub_one, add_smul, mul_comm, smul_add, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : p.1 < 0
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
e_4 : Eq (α := AddCommGroup (ℝ × ℝ)) Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule
e_6 : Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace
e_8 : instAddCommGroup = Ring.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
h :
  HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
        (ContinuousLinearMap.snd ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * (p.1 ^ p.2 * p.1⁻¹)) (ContinuousLinearMap.fst ℝ ℝ ℝ) =
    HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1)
        (ContinuousLinearMap.snd ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * p.2 * p.1⁻¹) (ContinuousLinearMap.fst ℝ ℝ ℝ)
⊢ HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * (p.1 ^ p.2 / p.1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
        (ContinuousLinearMap.snd ℝ ℝ ℝ) =
    HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1)
        (ContinuousLinearMap.snd ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * p.2 * p.1⁻¹) (ContinuousLinearMap.fst ℝ ℝ ℝ)

Tactic:
rw [div_eq_mul_inv, add_comm]

Premises used: div_eq_mul_inv, add_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : p.1 < 0
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
e_4 : Eq (α := AddCommGroup (ℝ × ℝ)) Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule
e_6 : Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace
e_8 : instAddCommGroup = Ring.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
h :
  p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π =
    rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1
h₁ : p.2 * (p.1 ^ p.2 * p.1⁻¹) = p.1 ^ p.2 * p.2 * p.1⁻¹
⊢ HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π)
        (ContinuousLinearMap.snd ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.2 * (p.1 ^ p.2 * p.1⁻¹)) (ContinuousLinearMap.fst ℝ ℝ ℝ) =
    HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1)
        (ContinuousLinearMap.snd ℝ ℝ ℝ) +
      HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) (p.1 ^ p.2 * p.2 * p.1⁻¹) (ContinuousLinearMap.fst ℝ ℝ ℝ)

Tactic:
congr 2
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : p.1 < 0
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
e_4 : Eq (α := AddCommGroup (ℝ × ℝ)) Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule
e_6 : Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace
e_8 : instAddCommGroup = Ring.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
⊢ p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π =
    rexp (log p.1 * p.2) * -sin (p.2 * π) * π + p.1 ^ p.2 * log p.1

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : p.1 < 0
this : (𝓝 p).EventuallyEq (β := ℝ) (fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) fun (x : ℝ × ℝ) ↦ rexp (log x.1 * x.2) * cos (x.2 * π)
e_4 : Eq (α := AddCommGroup (ℝ × ℝ)) Prod.instAddCommGroup NormedAddCommGroup.toAddCommGroup
e_5 : HEq (α := Module ℝ (ℝ × ℝ)) Prod.instModule (β := Module ℝ (ℝ × ℝ)) NormedSpace.toModule
e_6 : Eq (α := TopologicalSpace (ℝ × ℝ)) instTopologicalSpaceProd UniformSpace.toTopologicalSpace
e_8 : instAddCommGroup = Ring.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
⊢ p.2 * (p.1 ^ p.2 * p.1⁻¹) = p.1 ^ p.2 * p.2 * p.1⁻¹

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : p.1 ≠ 0
n : WithTop ℕ∞
inl : ∀ (hneg : p.1 < 0), ContDiffAt ℝ (F := ℝ) n (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p
inr : ∀ (hpos : 0 < p.1), ContDiffAt ℝ (F := ℝ) n (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p
⊢ ContDiffAt ℝ (F := ℝ) n (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p

Tactic:
rcases hp.lt_or_gt with hneg | hpos

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : p.1 ≠ 0
n : WithTop ℕ∞
hneg : p.1 < 0
⊢ ContDiffAt ℝ (F := ℝ) n (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p

Tactic:
(((contDiffAt_fst.log hneg.ne).mul contDiffAt_snd).exp.mul
          (contDiffAt_snd.mul contDiffAt_const).cos).congr_of_eventuallyEq
      ((continuousAt_fst.eventually (gt_mem_nhds hneg)).mono fun p hp => rpow_def_of_neg hp _)

Premises used: contDiffAt_snd, gt_mem_nhds, Real.rpow_def_of_neg, ContDiffAt.log, Filter.Eventually.mono, Filter.Tendsto.eventually, contDiffAt_const, ContDiffAt.cos, Prod.snd, contDiffAt_fst, ContDiffAt.exp, continuousAt_fst, ContDiffAt.congr_of_eventuallyEq, LT.lt.ne, ContDiffAt.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : p.1 ≠ 0
n : WithTop ℕ∞
hpos : 0 < p.1
⊢ ContDiffAt ℝ (F := ℝ) n (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p

Tactic:
((contDiffAt_fst.log hpos.ne').mul contDiffAt_snd).exp.congr_of_eventuallyEq
      ((continuousAt_fst.eventually (lt_mem_nhds hpos)).mono fun p hp => rpow_def_of_pos hp _)

Premises used: contDiffAt_snd, Real.rpow_def_of_pos, ContDiffAt.log, Filter.Eventually.mono, LT.lt.ne', Filter.Tendsto.eventually, Prod.snd, contDiffAt_fst, ContDiffAt.exp, continuousAt_fst, ContDiffAt.congr_of_eventuallyEq, lt_mem_nhds, ContDiffAt.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : p.1 ≠ 0
n : WithTop ℕ∞
hneg : p.1 < 0
⊢ ContDiffAt ℝ (F := ℝ) n (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p

Tactic:
exacts
    [(((contDiffAt_fst.log hneg.ne).mul contDiffAt_snd).exp.mul
          (contDiffAt_snd.mul contDiffAt_const).cos).congr_of_eventuallyEq
      ((continuousAt_fst.eventually (gt_mem_nhds hneg)).mono fun p hp => rpow_def_of_neg hp _),
    ((contDiffAt_fst.log hpos.ne').mul contDiffAt_snd).exp.congr_of_eventuallyEq
      ((continuousAt_fst.eventually (lt_mem_nhds hpos)).mono fun p hp => rpow_def_of_pos hp _)]

Premises used: contDiffAt_snd, gt_mem_nhds, Real.rpow_def_of_neg, ContDiffAt.log, Filter.Eventually.mono, Filter.Tendsto.eventually, contDiffAt_const, ContDiffAt.cos, Prod.snd, contDiffAt_fst, ContDiffAt.exp, continuousAt_fst, ContDiffAt.congr_of_eventuallyEq, LT.lt.ne, ContDiffAt.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ × ℝ
hp : p.1 ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (p : ℝ × ℝ) ↦ p.1 ^ p.2) p

Tactic:
(contDiffAt_rpow_of_ne p hp).differentiableAt one_ne_zero

Premises used: ContDiffAt.differentiableAt, setOf, one_ne_zero, Real.contDiffAt_rpow_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
f g : ℝ → ℝ
f' g' : ℝ
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
h : 0 < f x
⊢ HasStrictDerivAt (F := ℝ) ((fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) ∘ fun (x : ℝ) ↦ (f x, g x) : ℝ → ℝ)
    ((HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ)
              (((fun (x : ℝ) ↦ (f x, g x)) x).2 *
                HPow.hPow (α := ℝ) ((fun (x : ℝ) ↦ (f x, g x)) x).1
                  (HSub.hSub (α := ℝ) ((fun (x : ℝ) ↦ (f x, g x)) x).2 1))
              (ContinuousLinearMap.fst ℝ ℝ ℝ) +
            HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ)
              (HPow.hPow (α := ℝ) (β := ℝ) ((fun (x : ℝ) ↦ (f x, g x)) x).1 ((fun (x : ℝ) ↦ (f x, g x)) x).2 *
                log ((fun (x : ℝ) ↦ (f x, g x)) x).1)
              (ContinuousLinearMap.snd ℝ ℝ ℝ) :
          (a : ℝ × ℝ) → ℝ)
        (f', g') :
      ℝ)
    x

Tactic:
(hasStrictFDerivAt_rpow_of_pos ((fun x => (f x, g x)) x) h).comp_hasStrictDerivAt x
      (hf.prodMk hg)

Premises used: HasStrictFDerivAt.comp_hasStrictDerivAt, HasStrictDerivAt.prodMk