awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h₁ :
  f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * log (f 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')
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * log (f x)) x

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

Premises used: HasStrictFDerivAt.comp_hasStrictDerivAt, HasStrictDerivAt.prodMk
-- 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
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * log (f 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')

Tactic:
simp [mul_assoc, mul_comm]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx : x ≠ 0
p : ℝ
inl : ∀ (hx : x < 0), HasStrictDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x
inr : ∀ (hx : 0 < x), HasStrictDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x

Tactic:
rcases hx.lt_or_gt with hx | hx

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
p : ℝ
hx : x < 0
⊢ HasStrictDerivAt (F := ℝ) ((fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) ∘ fun (x : ℝ) ↦ (id x, p) : ℝ → ℝ)
    ((HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) ((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
            HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ)
              ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π)
              (ContinuousLinearMap.snd ℝ ℝ ℝ) :
          (a : ℝ × ℝ) → ℝ)
        (1, 0) :
      ℝ)
    x

Tactic:
have := (hasStrictFDerivAt_rpow_of_neg (x, p) hx).comp_hasStrictDerivAt x
      ((hasStrictDerivAt_id x).prodMk (hasStrictDerivAt_const x p))
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
p : ℝ
hx : x < 0
this :
  HasStrictDerivAt (F := ℝ) ((fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) ∘ fun (x : ℝ) ↦ (id x, p) : ℝ → ℝ)
    ((HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) ((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
            HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ)
              ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π)
              (ContinuousLinearMap.snd ℝ ℝ ℝ) :
          (a : ℝ × ℝ) → ℝ)
        (1, 0) :
      ℝ)
    x
⊢ HasStrictDerivAt (F := ℝ) ((fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) ∘ fun (x : ℝ) ↦ (id x, p) : ℝ → ℝ)
    ((HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) ((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
            HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ)
              ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π)
              (ContinuousLinearMap.snd ℝ ℝ ℝ) :
          (a : ℝ × ℝ) → ℝ)
        (1, 0) :
      ℝ)
    x

Tactic:
this
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
p : ℝ
hx : x < 0
this :
  HasStrictDerivAt (F := ℝ) ((fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) ∘ fun (x : ℝ) ↦ (id x, p) : ℝ → ℝ)
    ((HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) ((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
            HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ)
              ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π)
              (ContinuousLinearMap.snd ℝ ℝ ℝ) :
          (a : ℝ × ℝ) → ℝ)
        (1, 0) :
      ℝ)
    x
h :
  p * x ^ (p - 1) =
    (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) ((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
          HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ)
            ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π)
            (ContinuousLinearMap.snd ℝ ℝ ℝ) :
        (a : ℝ × ℝ) → ℝ)
      (1, 0)
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x

Tactic:
convert! this using 1
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
p : ℝ
hx : x < 0
this :
  HasStrictDerivAt (F := ℝ) ((fun (x : ℝ × ℝ) ↦ x.1 ^ x.2) ∘ fun (x : ℝ) ↦ (id x, p) : ℝ → ℝ)
    ((HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) ((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
            HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ)
              ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π)
              (ContinuousLinearMap.snd ℝ ℝ ℝ) :
          (a : ℝ × ℝ) → ℝ)
        (1, 0) :
      ℝ)
    x
⊢ p * x ^ (p - 1) =
    (HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ) ((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) (ContinuousLinearMap.fst ℝ ℝ ℝ) +
          HSMul.hSMul (β := ℝ × ℝ →L[ℝ] ℝ)
            ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π)
            (ContinuousLinearMap.snd ℝ ℝ ℝ) :
        (a : ℝ × ℝ) → ℝ)
      (1, 0)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x : ℝ
hx_1 : x ≠ 0
p : ℝ
hx : 0 < x
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x

Tactic:
simpa using (hasStrictDerivAt_id x).rpow (hasStrictDerivAt_const x p) hx

Premises used: HasStrictDerivAt.rpow, hasStrictDerivAt_const, hasStrictDerivAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
a : ℝ
ha : 0 < a
x : ℝ
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ a ^ x) (a ^ x * log a) x

Tactic:
simpa using (hasStrictDerivAt_const _ _).rpow (hasStrictDerivAt_id x) ha

Premises used: HasStrictDerivAt.rpow, hasStrictDerivAt_const, hasStrictDerivAt_id
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ p) x

Tactic:
(hasStrictDerivAt_rpow_const_of_ne hx p).hasStrictFDerivAt.differentiableAt

Premises used: Real.hasStrictDerivAt_rpow_const_of_ne, HasStrictFDerivAt.differentiableAt, HasStrictDerivAt.hasStrictFDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
r : ℝ
hr : r < 1
hr' : r ≠ 0
by_contra : ∀ (h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ r) 0), False
⊢ ¬DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ r) 0

Tactic:
by_contra h
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
r : ℝ
hr : r < 1
hr' : r ≠ 0
h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ r) 0
y : ℝ := deriv (fun (x : ℝ) ↦ x ^ r) 0
apply :
  ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioi 0) x → x⁻¹ • ((0 + x) ^ r - HPow.hPow (α := ℝ) 0 r) = x ^ (r - 1)
⊢ Tendsto (fun (t : ℝ) ↦ t ^ (r - 1)) (𝓝[>] 0) (𝓝 y)

Tactic:
apply tendsto_nhdsWithin_congr _ h.hasDerivAt.tendsto_slope_zero_right

Premises used: DifferentiableAt.hasDerivAt, tendsto_nhdsWithin_congr, HasDerivAt.tendsto_slope_zero_right
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
r : ℝ
hr : r < 1
hr' : r ≠ 0
h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ r) 0
y : ℝ := deriv (fun (x : ℝ) ↦ x ^ r) 0
x : ℝ
this : ∀ (hx : 0 < x), x⁻¹ • ((0 + x) ^ r - HPow.hPow (α := ℝ) 0 r) = x ^ (r - 1)
⊢ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x → x⁻¹ • ((0 + x) ^ r - HPow.hPow (α := ℝ) 0 r) = x ^ (r - 1)

Tactic:
(hx : 0 < x)
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
r : ℝ
hr : r < 1
hr' : r ≠ 0
h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ r) 0
y : ℝ := deriv (fun (x : ℝ) ↦ x ^ r) 0
x : ℝ
hx : 0 < x
simp : x⁻¹ * x ^ r = x ^ (r - 1)
⊢ x⁻¹ • ((0 + x) ^ r - HPow.hPow (α := ℝ) 0 r) = x ^ (r - 1)

Tactic:
simp only [zero_add, ne_eq, hr', not_false_eq_true, Real.zero_rpow, sub_zero, smul_eq_mul]

Premises used: sub_zero, zero_add, ne_eq, Real.zero_rpow, smul_eq_mul, not_false_eq_true
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
r : ℝ
hr : r < 1
hr' : r ≠ 0
h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ r) 0
y : ℝ := deriv (fun (x : ℝ) ↦ x ^ r) 0
x : ℝ
hx : 0 < x
field_simp : x ^ r = x * x ^ (r - 1)
⊢ x⁻¹ * x ^ r = x ^ (r - 1)

Tactic:
field_simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
r : ℝ
hr : r < 1
hr' : r ≠ 0
h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ r) 0
y : ℝ := deriv (fun (x : ℝ) ↦ x ^ r) 0
x : ℝ
hx : 0 < x
nth_rw : HPow.hPow (β := ℝ) x 1 * x ^ (r - 1) = x * x ^ (r - 1)
⊢ x ^ r = x * x ^ (r - 1)

Tactic:
nth_rw 1 [← add_sub_cancel 1 r, Real.rpow_add hx]

Premises used: add_sub_cancel, Real.rpow_add, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
r : ℝ
hr : r < 1
hr' : r ≠ 0
h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ r) 0
y : ℝ := deriv (fun (x : ℝ) ↦ x ^ r) 0
x : ℝ
hx : 0 < x
⊢ HPow.hPow (β := ℝ) x 1 * x ^ (r - 1) = x * x ^ (r - 1)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
r : ℝ
hr : r < 1
hr' : r ≠ 0
h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ r) 0
y : ℝ := deriv (fun (x : ℝ) ↦ x ^ r) 0
⊢ Tendsto (fun (t : ℝ) ↦ t ^ (r - 1)) (𝓝[>] 0) (𝓝 y)

Tactic:
have h : Filter.Tendsto (fun t ↦ t ^ (r - 1)) (𝓝[>] 0) (𝓝 y) := by
    apply tendsto_nhdsWithin_congr _ h.hasDerivAt.tendsto_slope_zero_right
    intro x (hx : 0 < x)
    simp only [zero_add, ne_eq, hr', not_false_eq_true, Real.zero_rpow, sub_zero, smul_eq_mul]
    field_simp
    nth_rw 1 [← add_sub_cancel 1 r, Real.rpow_add hx]
    simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
r : ℝ
hr : r < 1
hr' : r ≠ 0
h_1 : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ r) 0
y : ℝ := deriv (fun (x : ℝ) ↦ x ^ r) 0
h : Tendsto (fun (t : ℝ) ↦ t ^ (r - 1)) (𝓝[>] 0) (𝓝 y)
⊢ r - 1 < 0

Tactic:
simp [hr]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
r : ℝ
hr : r < 1
hr' : r ≠ 0
h_1 : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ r) 0
y : ℝ := deriv (fun (x : ℝ) ↦ x ^ r) 0
h : Tendsto (fun (t : ℝ) ↦ t ^ (r - 1)) (𝓝[>] 0) (𝓝 y)
⊢ False

Tactic:
exact not_tendsto_nhds_of_tendsto_atTop (tendsto_rpow_neg_nhdsGT_zero (by simp [hr])) y h

Premises used: not_tendsto_nhds_of_tendsto_atTop, tendsto_rpow_neg_nhdsGT_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ
⊢ DifferentiableOn ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ p) {0}ᶜ

Tactic:
fun _ hx => (Real.differentiableAt_rpow_const_of_ne p hx).differentiableWithinAt

Premises used: Real.differentiableAt_rpow_const_of_ne, DifferentiableAt.differentiableWithinAt, DifferentiableOn
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
a x : ℝ
ha : a < 0
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ a ^ x) (a ^ x * log a - rexp (log a * x) * sin (x * π) * π) x

Tactic:
simpa using (hasStrictFDerivAt_rpow_of_neg (a, x) ha).comp_hasStrictDerivAt x
    ((hasStrictDerivAt_const _ _).prodMk (hasStrictDerivAt_id _))

Premises used: HasStrictFDerivAt.comp_hasStrictDerivAt, Prod.mk, hasStrictDerivAt_const, HasStrictDerivAt.prodMk, hasStrictDerivAt_id, Real.hasStrictFDerivAt_rpow_of_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x p : ℝ
h : x ≠ 0 ∨ 1 ≤ p
inl : ∀ (hx : x ≠ 0), HasDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x
inr : ∀ (h : Ne (α := ℝ) 0 0 ∨ 1 ≤ p), HasDerivAt (fun (x : ℝ) ↦ x ^ p) (p * HPow.hPow (α := ℝ) 0 (p - 1)) 0
⊢ HasDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x

Tactic:
rcases ne_or_eq x 0 with (hx | rfl)

Premises used: ne_or_eq, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x p : ℝ
h : x ≠ 0 ∨ 1 ≤ p
hx : x ≠ 0
⊢ HasDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x

Tactic:
(hasStrictDerivAt_rpow_const_of_ne hx _).hasDerivAt

Premises used: Real.hasStrictDerivAt_rpow_const_of_ne, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x p : ℝ
h : x ≠ 0 ∨ 1 ≤ p
hx : x ≠ 0
⊢ HasDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x

Tactic:
exact (hasStrictDerivAt_rpow_const_of_ne hx _).hasDerivAt

Premises used: Real.hasStrictDerivAt_rpow_const_of_ne, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ
h : Ne (α := ℝ) 0 0 ∨ 1 ≤ p
⊢ 1 ≤ p

Tactic:
replace h : 1 ≤ p := h.neg_resolve_left rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ
h : 1 ≤ p
inr : ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ p) 0
inr₁ : ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ p * x ^ (p - 1)) 0
⊢ HasDerivAt (fun (x : ℝ) ↦ x ^ p) (p * HPow.hPow (α := ℝ) 0 (p - 1)) 0

Tactic:
apply hasDerivAt_of_hasDerivAt_of_ne fun x hx =>
    (hasStrictDerivAt_rpow_const_of_ne hx p).hasDerivAt

Premises used: Real.hasStrictDerivAt_rpow_const_of_ne, hasDerivAt_of_hasDerivAt_of_ne, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ
h : 1 ≤ p
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ p) 0

Tactic:
continuousAt_id.rpow_const (Or.inr (zero_le_one.trans h))

Premises used: zero_le_one, ContinuousAt.rpow_const, LE.le.trans, continuousAt_id, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ
h : 1 ≤ p
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ p * x ^ (p - 1)) 0

Tactic:
continuousAt_const.mul (continuousAt_id.rpow_const (Or.inr (sub_nonneg.2 h)))

Premises used: Iff.mpr, continuousAt_const, ContinuousAt.rpow_const, ContinuousAt.mul, sub_nonneg, continuousAt_id, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ
h : 1 ≤ p
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ p) 0

Tactic:
exacts [continuousAt_id.rpow_const (Or.inr (zero_le_one.trans h)),
    continuousAt_const.mul (continuousAt_id.rpow_const (Or.inr (sub_nonneg.2 h)))]

Premises used: Iff.mpr, continuousAt_const, zero_le_one, ContinuousAt.rpow_const, ContinuousAt.mul, LE.le.trans, sub_nonneg, continuousAt_id, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ
hp : 1 ≤ p
⊢ Differentiable ℝ (F := ℝ) fun (x : ℝ) ↦ x ^ p

Tactic:
fun _ => (hasDerivAt_rpow_const (Or.inr hp)).differentiableAt

Premises used: Differentiable, HasDerivAt.differentiableAt, Real.hasDerivAt_rpow_const, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x p : ℝ
pos : ∀ (h : p = 0), deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)
neg : ∀ (h : p ≠ 0), deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)
⊢ deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)

Tactic:
by_cases! h : p = 0
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x p : ℝ
h : p = 0
⊢ deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x p : ℝ
h : p ≠ 0
pos : ∀ (h' : x ≠ 0 ∨ 1 ≤ p), deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)
neg : ∀ (h' : x = 0 ∧ p < 1), deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)
⊢ deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)

Tactic:
by_cases! h' : x ≠ 0 ∨ 1 ≤ p
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x p : ℝ
h : p ≠ 0
h' : x ≠ 0 ∨ 1 ≤ p
⊢ deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)

Tactic:
apply (Real.hasDerivAt_rpow_const h').deriv

Premises used: HasDerivAt.deriv, Real.hasDerivAt_rpow_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x p : ℝ
h : p ≠ 0
h' : x = 0 ∧ p < 1
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ x ^ p) 0) 0

Tactic:
have h'' := deriv_zero_of_not_differentiableAt (not_differentiableAt_rpow_const_zero h'.2 h ·)
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x p : ℝ
h : p ≠ 0
h' : x = 0 ∧ p < 1
h'' : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ x ^ p) 0) 0
⊢ deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)

Tactic:
grind [Real.zero_rpow]

Premises used: Real.zero_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ
⊢ Eq (α := (x : ℝ) → ℝ) (deriv fun (x : ℝ) ↦ x ^ p) fun (x : ℝ) ↦ p * x ^ (p - 1)

Tactic:
funext (deriv_rpow_const · p)

Premises used: Real.deriv_rpow_const, funext
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x p : ℝ
n : WithTop ℕ∞
h : x ≠ 0
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ x ^ p) x

Tactic:
(contDiffAt_rpow_of_ne (x, p) h).comp x (contDiffAt_id.prodMk contDiffAt_const)

Premises used: contDiffAt_id, ContDiffAt.comp, contDiffAt_const, ContDiffAt.prodMk
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ
h : (↑0 : ℝ) ≤ p
x : ℝ
⊢ 0 ≤ p

Tactic:
simpa using h
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ
h : (↑0 : ℝ) ≤ p
⊢ ContDiff ℝ (F := ℝ) (↑0 : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p

Tactic:
exact contDiff_zero.2 (continuous_id.rpow_const fun x => Or.inr <| by simpa using h)

Premises used: Iff.mpr, contDiff_zero, continuous_id, Continuous.rpow_const, Or.inr
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
n : ℕ
ihn : ∀ {p : ℝ} (h : (↑n : ℝ) ≤ p), ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p
p : ℝ
h : (↑(n + 1) : ℝ) ≤ p
⊢ LE.le (α := ℝ) 1 (↑(n + 1) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
n : ℕ
ihn : ∀ {p : ℝ} (h : (↑n : ℝ) ≤ p), ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p
p : ℝ
h : (↑(n + 1) : ℝ) ≤ p
⊢ 1 ≤ p

Tactic:
have h1 : 1 ≤ p := le_trans (by simp) h
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
n : ℕ
ihn : ∀ {p : ℝ} (h : (↑n : ℝ) ≤ p), ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p
p : ℝ
h : (↑(n + 1) : ℝ) ≤ p
h1 : 1 ≤ p
⊢ (↑n : ℝ) ≤ p - 1

Tactic:
rw [Nat.cast_add_one, ← le_sub_iff_add_le] at h

Premises used: le_sub_iff_add_le, Nat.cast_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
n : ℕ
ihn : ∀ {p : ℝ} (h : (↑n : ℝ) ≤ p), ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p
p : ℝ
h : (↑(n + 1) : ℝ) ≤ p
h1 : 1 ≤ p
h₁ : (↑n : ℝ) ≤ p - 1
⊢ 1 ≤ p

Tactic:
rw [Nat.cast_add_one, ← le_sub_iff_add_le] at h

Premises used: le_sub_iff_add_le, Nat.cast_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
n : ℕ
ihn : ∀ {p : ℝ} (h : (↑n : ℝ) ≤ p), ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p
p : ℝ
h : (↑n : ℝ) ≤ p - 1
h1 : 1 ≤ p
succ :
  (Differentiable ℝ (F := ℝ) fun (x : ℝ) ↦ x ^ p) ∧
    (Eq (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) ⊤ → AnalyticOn ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ p) Set.univ) ∧
      ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ p * x ^ (p - 1)
⊢ ContDiff ℝ (F := ℝ) (↑(n + 1) : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p

Tactic:
rw [Nat.cast_add_one, contDiff_succ_iff_deriv, deriv_rpow_const' p]

Premises used: contDiff_succ_iff_deriv, Real.deriv_rpow_const', Nat.cast_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
n : ℕ
ihn : ∀ {p : ℝ} (h : (↑n : ℝ) ≤ p), ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p
p : ℝ
h : (↑n : ℝ) ≤ p - 1
h1 : 1 ≤ p
succ :
  (Differentiable ℝ (F := ℝ) fun (x : ℝ) ↦ x ^ p) ∧ ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ p * x ^ (p - 1)
⊢ (Differentiable ℝ (F := ℝ) fun (x : ℝ) ↦ x ^ p) ∧
    (Eq (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) ⊤ → AnalyticOn ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ p) Set.univ) ∧
      ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ p * x ^ (p - 1)

Tactic:
simp only [WithTop.natCast_ne_top, analyticOn_univ, IsEmpty.forall_iff, true_and]

Premises used: WithTop.natCast_ne_top, analyticOn_univ, true_and, IsEmpty.forall_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
n : ℕ
ihn : ∀ {p : ℝ} (h : (↑n : ℝ) ≤ p), ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p
p : ℝ
h : (↑n : ℝ) ≤ p - 1
h1 : 1 ≤ p
⊢ (Differentiable ℝ (F := ℝ) fun (x : ℝ) ↦ x ^ p) ∧ ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ p * x ^ (p - 1)

Tactic:
⟨differentiable_rpow_const h1, contDiff_const.mul (ihn h)⟩

Premises used: contDiff_const, And.intro, Real.differentiable_rpow_const, ContDiff.mul
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
n : ℕ
ihn : ∀ {p : ℝ} (h : (↑n : ℝ) ≤ p), ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p
p : ℝ
h : (↑n : ℝ) ≤ p - 1
h1 : 1 ≤ p
⊢ (Differentiable ℝ (F := ℝ) fun (x : ℝ) ↦ x ^ p) ∧ ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ p * x ^ (p - 1)

Tactic:
exact ⟨differentiable_rpow_const h1, contDiff_const.mul (ihn h)⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
p : ℝ
n : ℕ
h : (↑n : ℝ) ≤ p
zero : ∀ {p : ℝ} (h : (↑0 : ℝ) ≤ p), ContDiff ℝ (F := ℝ) (↑0 : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p
succ :
  ∀ (n : ℕ) (ihn : ∀ {p : ℝ} (h : (↑n : ℝ) ≤ p), ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p) {p : ℝ}
    (h : (↑(n + 1) : ℝ) ≤ p), ContDiff ℝ (F := ℝ) (↑(n + 1) : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p
⊢ ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p

Tactic:
induction n generalizing p with
  | zero => exact contDiff_zero.2 (continuous_id.rpow_const fun x => Or.inr <| by simpa using h)
  | succ n ihn =>
    have h1 : 1 ≤ p := le_trans (by simp) h
    rw [Nat.cast_add_one, ← le_sub_iff_add_le] at h
    rw [Nat.cast_add_one, contDiff_succ_iff_deriv, deriv_rpow_const' p]
    simp only [WithTop.natCast_ne_top, analyticOn_univ, IsEmpty.forall_iff, true_and]
    exact ⟨differentiable_rpow_const h1, contDiff_const.mul (ihn h)⟩

Premises used: Iff.mpr, contDiff_zero, WithTop.natCast_ne_top, continuous_id, analyticOn_univ, contDiff_succ_iff_deriv, Real.deriv_rpow_const', le_sub_iff_add_le, Continuous.rpow_const, Nat.cast_add_one, Or.inr, true_and, IsEmpty.forall_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x p : ℝ
n : ℕ
h : (↑n : ℝ) ≤ p
⊢ ContDiffAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (x : ℝ) ↦ x ^ p) x

Tactic:
(contDiff_rpow_const_of_le h).contDiffAt

Premises used: Real.contDiff_rpow_const_of_le, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x p : ℝ
n : ℕ
h : x ≠ 0 ∨ (↑n : ℝ) ≤ p
⊢ ContDiffAt ℝ (F := ℝ) (↑n : WithTop ℕ∞) (fun (x : ℝ) ↦ x ^ p) x

Tactic:
h.elim contDiffAt_rpow_const_of_ne contDiffAt_rpow_const_of_le

Premises used: Real.contDiffAt_rpow_const_of_le, Real.contDiffAt_rpow_const_of_ne, Or.elim
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
r x : ℝ
k : ℕ
a :
  Eq (α := (x : ℝ) → ℝ) (deriv^[k] fun (x : ℝ) ↦ x ^ r) fun (x : ℝ) ↦
    Polynomial.eval r (descPochhammer ℝ k) * x ^ (r - (↑k : ℝ))
⊢ deriv^[k] (fun (x : ℝ) ↦ x ^ r) x = Polynomial.eval r (descPochhammer ℝ k) * x ^ (r - (↑k : ℝ))

Tactic:
apply funext_iff.mp

Premises used: funext_iff, Iff.mp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
r x : ℝ
⊢ Eq (α := (x : ℝ) → ℝ) (deriv^[0] fun (x : ℝ) ↦ x ^ r) fun (x : ℝ) ↦
    Polynomial.eval r (descPochhammer ℝ 0) * x ^ (r - (↑0 : ℝ))

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
r x : ℝ
k : ℕ
IH :
  Eq (α := (x : ℝ) → ℝ) (deriv^[k] fun (x : ℝ) ↦ x ^ r) fun (x : ℝ) ↦
    Polynomial.eval r (descPochhammer ℝ k) * x ^ (r - (↑k : ℝ))
a :
  Eq (α := (x : ℝ) → ℝ) (deriv fun (x : ℝ) ↦ Polynomial.eval r (descPochhammer ℝ k) * x ^ (r - (↑k : ℝ))) fun (x : ℝ) ↦
    Polynomial.eval r (descPochhammer ℝ (k + 1)) * x ^ (r - HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
⊢ Eq (α := (x : ℝ) → ℝ) (deriv^[k + 1] fun (x : ℝ) ↦ x ^ r) fun (x : ℝ) ↦
    Polynomial.eval r (descPochhammer ℝ (k + 1)) * x ^ (r - (↑(k + 1) : ℝ))

Tactic:
simp only [Function.iterate_succ', Function.comp_apply, Nat.cast_add, Nat.cast_one, IH]

Premises used: Function.iterate_succ', Nat.cast_add, Function.comp_apply, Nat.cast_one