awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
f g : ℝ → ℝ
f' g' : ℝ
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
h : 0 < f x
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * log (f x)) x
have 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')
Tactic: convert!
    (hasStrictFDerivAt_rpow_of_pos ((fun x => (f x, g x)) x) h).comp_hasStrictDerivAt x
      (hf.prodMk hg) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx : x ≠ 0
p : ℝ
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x
have inl : ∀ (hx : x < 0), HasStrictDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x
Tactic: rcases hx.lt_or_gt with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x : ℝ
hx : x ≠ 0
p : ℝ
inl : ∀ (hx : x < 0), HasStrictDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x
have inr : ∀ (hx : 0 < x), HasStrictDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x
Tactic: rcases hx.lt_or_gt with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (hypothesis)
Goal:
x : ℝ
hx_1 : x ≠ 0
p : ℝ
hx : x < 0
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x
have 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
Tactic: have := (hasStrictFDerivAt_rpow_of_neg (x, p) hx).comp_hasStrictDerivAt x
      ((hasStrictDerivAt_id x).prodMk (hasStrictDerivAt_const x p))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
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 (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x
have 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)
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
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)
have apply : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioi 0) x → x⁻¹ • ((0 + x) ^ r - HPow.hPow (α := ℝ) 0 r) = x ^ (r - 1)
Tactic: apply tendsto_nhdsWithin_congr _ h.hasDerivAt.tendsto_slope_zero_right
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
r : ℝ
hr : r < 1
hr' : r ≠ 0
h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ r) 0
y : ℝ := deriv (fun (x : ℝ) ↦ x ^ r) 0
x : ℝ
⊢ Membership.mem (γ := Set ℝ) (Set.Ioi 0) x → x⁻¹ • ((0 + x) ^ r - HPow.hPow (α := ℝ) 0 r) = x ^ (r - 1)
have this : ∀ (hx : 0 < x), x⁻¹ • ((0 + x) ^ r - HPow.hPow (α := ℝ) 0 r) = x ^ (r - 1)
Tactic: (hx : 0 < x)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
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
⊢ x⁻¹ • ((0 + x) ^ r - HPow.hPow (α := ℝ) 0 r) = x ^ (r - 1)
have simp : x⁻¹ * x ^ r = x ^ (r - 1)
Tactic: simp only [zero_add, ne_eq, hr', not_false_eq_true, Real.zero_rpow, sub_zero, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
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
⊢ x⁻¹ * x ^ r = x ^ (r - 1)
have field_simp : x ^ r = x * x ^ (r - 1)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
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
⊢ x ^ r = x * x ^ (r - 1)
have nth_rw : HPow.hPow (β := ℝ) x 1 * x ^ (r - 1) = x * x ^ (r - 1)
Tactic: nth_rw 1 [← add_sub_cancel 1 r, Real.rpow_add hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (hypothesis)
Goal:
r : ℝ
hr : r < 1
hr' : r ≠ 0
h : DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ r) 0
y : ℝ := deriv (fun (x : ℝ) ↦ x ^ r) 0
⊢ False
have h₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x p : ℝ
h : x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x
have inl : ∀ (hx : x ≠ 0), HasDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x
Tactic: rcases ne_or_eq x 0 with (hx | rfl)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x p : ℝ
h : x ≠ 0 ∨ 1 ≤ p
inl : ∀ (hx : x ≠ 0), HasDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x
⊢ HasDerivAt (fun (x : ℝ) ↦ x ^ p) (p * x ^ (p - 1)) x
have inr : ∀ (h : Ne (α := ℝ) 0 0 ∨ 1 ≤ p), HasDerivAt (fun (x : ℝ) ↦ x ^ p) (p * HPow.hPow (α := ℝ) 0 (p - 1)) 0
Tactic: rcases ne_or_eq x 0 with (hx | rfl)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (hypothesis)
Goal:
p : ℝ
h : Ne (α := ℝ) 0 0 ∨ 1 ≤ p
⊢ HasDerivAt (fun (x : ℝ) ↦ x ^ p) (p * HPow.hPow (α := ℝ) 0 (p - 1)) 0
have h₁ : 1 ≤ p
Tactic: replace h : 1 ≤ p := h.neg_resolve_left rfl
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
p : ℝ
h : 1 ≤ p
⊢ HasDerivAt (fun (x : ℝ) ↦ x ^ p) (p * HPow.hPow (α := ℝ) 0 (p - 1)) 0
have inr : ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ p) 0
Tactic: apply hasDerivAt_of_hasDerivAt_of_ne fun x hx =>
    (hasStrictDerivAt_rpow_const_of_ne hx p).hasDerivAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
p : ℝ
h : 1 ≤ p
inr : ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ p) 0
⊢ HasDerivAt (fun (x : ℝ) ↦ x ^ p) (p * HPow.hPow (α := ℝ) 0 (p - 1)) 0
have inr₁ : ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ p * x ^ (p - 1)) 0
Tactic: apply hasDerivAt_of_hasDerivAt_of_ne fun x hx =>
    (hasStrictDerivAt_rpow_const_of_ne hx p).hasDerivAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x p : ℝ
⊢ deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)
have pos : ∀ (h : p = 0), deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)
Tactic: by_cases! h : p = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x p : ℝ
pos : ∀ (h : p = 0), deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)
⊢ deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)
have neg : ∀ (h : p ≠ 0), deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)
Tactic: by_cases! h : p = 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x p : ℝ
h : p ≠ 0
⊢ deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)
have pos : ∀ (h' : x ≠ 0 ∨ 1 ≤ p), deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)
Tactic: by_cases! h' : x ≠ 0 ∨ 1 ≤ p
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x p : ℝ
h : p ≠ 0
pos : ∀ (h' : x ≠ 0 ∨ 1 ≤ p), deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)
⊢ deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)
have neg : ∀ (h' : x = 0 ∧ p < 1), deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)
Tactic: by_cases! h' : x ≠ 0 ∨ 1 ≤ p
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (hypothesis)
Goal:
x p : ℝ
h : p ≠ 0
h' : x = 0 ∧ p < 1
⊢ deriv (fun (x : ℝ) ↦ x ^ p) x = p * x ^ (p - 1)
have h'' : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ x ^ p) 0) 0
Tactic: have h'' := deriv_zero_of_not_differentiableAt (not_differentiableAt_rpow_const_zero h'.2 h ·)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (hypothesis)
Goal:
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
have h1 : 1 ≤ p
Tactic: have h1 : 1 ≤ p := le_trans (by simp) h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (hypothesis)
Goal:
n : ℕ
ihn : ∀ {p : ℝ} (h : (↑n : ℝ) ≤ p), ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p
p : ℝ
h : (↑(n + 1) : ℝ) ≤ p
h1 : 1 ≤ p
⊢ ContDiff ℝ (F := ℝ) (↑(n + 1) : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p
have h₁ : (↑n : ℝ) ≤ p - 1
Tactic: rw [Nat.cast_add_one, ← le_sub_iff_add_le] at h
Cleared hypotheses: h, h1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
n : ℕ
ihn : ∀ {p : ℝ} (h : (↑n : ℝ) ≤ p), ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p
p : ℝ
h : (↑n : ℝ) ≤ p - 1
h1 : 1 ≤ p
⊢ ContDiff ℝ (F := ℝ) (↑(n + 1) : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p
have 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)
Tactic: rw [Nat.cast_add_one, contDiff_succ_iff_deriv, deriv_rpow_const' p]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
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) ∧
    (Eq (α := WithTop ℕ∞) (↑n : WithTop ℕ∞) ⊤ → AnalyticOn ℝ (F := ℝ) (fun (x : ℝ) ↦ x ^ p) Set.univ) ∧
      ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ p * x ^ (p - 1)
have succ : (Differentiable ℝ (F := ℝ) fun (x : ℝ) ↦ x ^ p) ∧ ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ p * x ^ (p - 1)
Tactic: simp only [WithTop.natCast_ne_top, analyticOn_univ, IsEmpty.forall_iff, true_and]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
p : ℝ
n : ℕ
h : (↑n : ℝ) ≤ p
⊢ ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p
have zero : ∀ {p : ℝ} (h : (↑0 : ℝ) ≤ p), ContDiff ℝ (F := ℝ) (↑0 : 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)⟩
Cleared hypotheses: p, n, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
p : ℝ
n : ℕ
h : (↑n : ℝ) ≤ p
zero : ∀ {p : ℝ} (h : (↑0 : ℝ) ≤ p), ContDiff ℝ (F := ℝ) (↑0 : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p
⊢ ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ x ^ p
have 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
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)⟩
Cleared hypotheses: p, n, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
r x : ℝ
k : ℕ
⊢ deriv^[k] (fun (x : ℝ) ↦ x ^ r) x = Polynomial.eval r (descPochhammer ℝ k) * x ^ (r - (↑k : ℝ))
have a : Eq (α := (x : ℝ) → ℝ) (deriv^[k] fun (x : ℝ) ↦ x ^ r) fun (x : ℝ) ↦
  Polynomial.eval r (descPochhammer ℝ k) * x ^ (r - (↑k : ℝ))
Tactic: apply funext_iff.mp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
r x : ℝ
k : ℕ
IH :
  Eq (α := (x : ℝ) → ℝ) (deriv^[k] fun (x : ℝ) ↦ x ^ r) fun (x : ℝ) ↦
    Polynomial.eval r (descPochhammer ℝ k) * x ^ (r - (↑k : ℝ))
⊢ Eq (α := (x : ℝ) → ℝ) (deriv^[k + 1] fun (x : ℝ) ↦ x ^ r) fun (x : ℝ) ↦
    Polynomial.eval r (descPochhammer ℝ (k + 1)) * x ^ (r - (↑(k + 1) : ℝ))
have 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)
Tactic: simp only [Function.iterate_succ', Function.comp_apply, Nat.cast_add, Nat.cast_one, IH]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
r x : ℝ
k : ℕ
IH :
  Eq (α := (x : ℝ) → ℝ) (deriv^[k] fun (x : ℝ) ↦ x ^ r) fun (x : ℝ) ↦
    Polynomial.eval r (descPochhammer ℝ k) * x ^ (r - (↑k : ℝ))
⊢ 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)
have a : ∀ (y : ℝ),
  deriv (fun (x : ℝ) ↦ Polynomial.eval r (descPochhammer ℝ k) * x ^ (r - (↑k : ℝ))) y =
    Polynomial.eval r (descPochhammer ℝ (k + 1)) * y ^ (r - HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
r x : ℝ
k : ℕ
IH :
  Eq (α := (x : ℝ) → ℝ) (deriv^[k] fun (x : ℝ) ↦ x ^ r) fun (x : ℝ) ↦
    Polynomial.eval r (descPochhammer ℝ k) * x ^ (r - (↑k : ℝ))
y : ℝ
⊢ deriv (fun (x : ℝ) ↦ Polynomial.eval r (descPochhammer ℝ k) * x ^ (r - (↑k : ℝ))) y =
    Polynomial.eval r (descPochhammer ℝ (k + 1)) * y ^ (r - HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
have a : y ^ (r - (↑k : ℝ) - 1) = y ^ (r - HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) ∨
  Polynomial.eval r (descPochhammer ℝ k) = 0 ∨ r - (↑k : ℝ) = 0
Tactic: simp only [deriv_const_mul_field, deriv_rpow_const, ← mul_assoc, descPochhammer_succ_right,
      Polynomial.eval_mul, Polynomial.eval_sub, Polynomial.eval_X, Polynomial.eval_natCast,
      mul_eq_mul_left_iff, mul_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
r x : ℝ
k : ℕ
⊢ Eq (α := (x : ℝ) → ℝ) (deriv^[k] fun (x : ℝ) ↦ x ^ r) fun (x : ℝ) ↦
    Polynomial.eval r (descPochhammer ℝ k) * x ^ (r - (↑k : ℝ))
have a : Eq (α := (x : ℝ) → ℝ) (deriv^[0] fun (x : ℝ) ↦ x ^ r) fun (x : ℝ) ↦
  Polynomial.eval r (descPochhammer ℝ 0) * x ^ (r - (↑0 : ℝ))
Tactic: induction k with
  | zero => simp
  | succ k IH =>
    simp only [Function.iterate_succ', Function.comp_apply, Nat.cast_add, Nat.cast_one, IH]
    ext y
    simp only [deriv_const_mul_field, deriv_rpow_const, ← mul_assoc, descPochhammer_succ_right,
      Polynomial.eval_mul, Polynomial.eval_sub, Polynomial.eval_X, Polynomial.eval_natCast,
      mul_eq_mul_left_iff, mul_eq_zero]
    grind
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
r x : ℝ
k : ℕ
a :
  Eq (α := (x : ℝ) → ℝ) (deriv^[0] fun (x : ℝ) ↦ x ^ r) fun (x : ℝ) ↦
    Polynomial.eval r (descPochhammer ℝ 0) * x ^ (r - (↑0 : ℝ))
⊢ Eq (α := (x : ℝ) → ℝ) (deriv^[k] fun (x : ℝ) ↦ x ^ r) fun (x : ℝ) ↦
    Polynomial.eval r (descPochhammer ℝ k) * x ^ (r - (↑k : ℝ))
have a₁ : ∀ (k : ℕ)
  (IH :
    Eq (α := (x : ℝ) → ℝ) (deriv^[k] fun (x : ℝ) ↦ x ^ r) fun (x : ℝ) ↦
      Polynomial.eval r (descPochhammer ℝ k) * x ^ (r - (↑k : ℝ))),
  Eq (α := (x : ℝ) → ℝ) (deriv^[k + 1] fun (x : ℝ) ↦ x ^ r) fun (x : ℝ) ↦
    Polynomial.eval r (descPochhammer ℝ (k + 1)) * x ^ (r - (↑(k + 1) : ℝ))
Tactic: induction k with
  | zero => simp
  | succ k IH =>
    simp only [Function.iterate_succ', Function.comp_apply, Nat.cast_add, Nat.cast_one, IH]
    ext y
    simp only [deriv_const_mul_field, deriv_rpow_const, ← mul_assoc, descPochhammer_succ_right,
      Polynomial.eval_mul, Polynomial.eval_sub, Polynomial.eval_X, Polynomial.eval_natCast,
      mul_eq_mul_left_iff, mul_eq_zero]
    grind
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
x p : ℝ
hx : x ≠ 0 ∨ 1 ≤ p
⊢ x ≠ 0 ∨ (↑1 : ℝ) ≤ p
have rwa : ∀ (hx : x ≠ 0 ∨ (↑1 : ℝ) ≤ p), x ≠ 0 ∨ (↑1 : ℝ) ≤ p
Tactic: rwa [← Nat.cast_one] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
p : ℝ
m : ℕ
hf : ContDiffAt ℝ (↑m : WithTop ℕ∞) f x
h : (↑m : ℝ) ≤ p
⊢ ContDiffAt ℝ (F := ℝ) (↑m : WithTop ℕ∞) (fun (x : E) ↦ f x ^ p) x
have hf₁ : ContDiffWithinAt ℝ (↑m : WithTop ℕ∞) f Set.univ x
Tactic: rw [← contDiffWithinAt_univ] at *
Cleared hypotheses: hf, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f g : ℝ → ℝ
f' g' x : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) s x
have h₁ : f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x) =
  (HSMul.hSMul (β := StrongDual ℝ ℝ) (g x * f x ^ (g x - 1)) (ContinuousLinearMap.toSpanSingleton ℝ f') +
        HSMul.hSMul (β := StrongDual ℝ ℝ) (f x ^ g x * Real.log (f x)) (ContinuousLinearMap.toSpanSingleton ℝ g') :
      (a : ℝ) → ℝ)
    1
Tactic: convert! (hf.hasFDerivWithinAt.rpow hg.hasFDerivWithinAt h).hasDerivWithinAt using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f g : ℝ → ℝ
f' g' x : ℝ
hf : HasDerivAt f f' x
hg : HasDerivAt g g' x
h : 0 < f x
⊢ HasDerivAt (fun (x : ℝ) ↦ f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x
have rw : ∀ (hf : HasDerivWithinAt f f' Set.univ x) (hg : HasDerivWithinAt g g' Set.univ x) (h : 0 < f x),
  HasDerivWithinAt (fun (x : ℝ) ↦ f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) Set.univ x
Tactic: rw [← hasDerivWithinAt_univ] at *
Cleared hypotheses: hf, hg, h
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℝ → ℝ
f' x p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivWithinAt (fun (y : ℝ) ↦ f y ^ p) (f' * p * f x ^ (p - 1)) s x
have h : f' * p * f x ^ (p - 1) = p * f x ^ (p - 1) * f'
Tactic: convert! (hasDerivAt_rpow_const hx).comp_hasDerivWithinAt x hf using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℝ → ℝ
f' x p : ℝ
hf : HasDerivAt f f' x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivAt (fun (y : ℝ) ↦ f y ^ p) (f' * p * f x ^ (p - 1)) x
have rw : ∀ (hf : HasDerivWithinAt f f' Set.univ x) (hx : f x ≠ 0 ∨ 1 ≤ p),
  HasDerivWithinAt (fun (y : ℝ) ↦ f y ^ p) (f' * p * f x ^ (p - 1)) Set.univ x
Tactic: rw [← hasDerivWithinAt_univ] at *
Cleared hypotheses: hf, hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
c : ℂ
t : ℝ
ht : 0 < t
⊢ deriv (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ c‖) t = c.re * t ^ (c.re - 1)
have rw : deriv (fun (x : ℝ) ↦ x ^ c.re) t = c.re * t ^ (c.re - 1)
Tactic: rw [EventuallyEq.deriv_eq (f := fun x ↦ x ^ c.re)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
c : ℂ
t : ℝ
ht : 0 < t
rw : deriv (fun (x : ℝ) ↦ x ^ c.re) t = c.re * t ^ (c.re - 1)
⊢ deriv (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ c‖) t = c.re * t ^ (c.re - 1)
have rw₁ : (𝓝 t).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ c‖) fun (x : ℝ) ↦ x ^ c.re
Tactic: rw [EventuallyEq.deriv_eq (f := fun x ↦ x ^ c.re)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
c : ℂ
t : ℝ
ht : 0 < t
⊢ deriv (fun (x : ℝ) ↦ x ^ c.re) t = c.re * t ^ (c.re - 1)
have rw : c.re * t ^ (c.re - 1) = c.re * t ^ (c.re - 1)
Tactic: rw [Real.deriv_rpow_const t]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
c : ℂ
t : ℝ
ht : 0 < t
⊢ (𝓝 t).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ ‖(↑x : ℂ) ^ c‖) fun (x : ℝ) ↦ x ^ c.re
have h : ∀ (x : ℝ) (hx : 0 < x), ‖(↑x : ℂ) ^ c‖ = x ^ c.re
Tactic: filter_upwards [eventually_gt_nhds ht] with x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
c : ℂ
t : ℝ
ht : 0 < t
x : ℝ
hx : 0 < x
⊢ ‖(↑x : ℂ) ^ c‖ = x ^ c.re
have h : x ^ c.re = x ^ c.re
Tactic: rw [Complex.norm_cpow_eq_rpow_re_of_pos hx]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
p : ℝ
⊢ Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ x ^ p) fun (x : ℝ) ↦ x ^ (p - 1)
have rcases : Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 0) fun (x : ℝ) ↦
  x ^ HSub.hSub (α := ℝ) 0 1
Tactic: rcases eq_or_ne p 0 with rfl | hp
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
p : ℝ
rcases :
  Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ HPow.hPow (β := ℝ) x 0) fun (x : ℝ) ↦
    x ^ HSub.hSub (α := ℝ) 0 1
⊢ Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ x ^ p) fun (x : ℝ) ↦ x ^ (p - 1)
have rcases₁ : ∀ (hp : p ≠ 0), Asymptotics.IsBigO (E := ℝ) (F := ℝ) atTop (deriv fun (x : ℝ) ↦ x ^ p) fun (x : ℝ) ↦ x ^ (p - 1)
Tactic: rcases eq_or_ne p 0 with rfl | hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℝ → ℝ
f' x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (fun (x : ℝ) ↦ a ^ f x) (Real.log a * f' * a ^ f x) s x
have h : Real.log a * f' * a ^ f x = 0 * f x * a ^ (f x - 1) + f' * a ^ f x * Real.log a
Tactic: convert! (hasDerivWithinAt_const x s a).rpow hf ha using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℝ → ℝ
f' x a : ℝ
ha : 0 < a
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun (x : ℝ) ↦ a ^ f x) (Real.log a * f' * a ^ f x) x
have rw : ∀ (hf : HasDerivWithinAt f f' Set.univ x),
  HasDerivWithinAt (fun (x : ℝ) ↦ a ^ f x) (Real.log a * f' * a ^ f x) Set.univ x
Tactic: rw [← hasDerivWithinAt_univ] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Deriv (goal)
Goal:
f : ℝ → ℝ
x : ℝ
s : Set ℝ
a : ℝ
ha : 0 < a
hf : DifferentiableWithinAt ℝ f s x
⊢ derivWithin (fun (x : ℝ) ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x
have pos : ∀ (hxs : UniqueDiffWithinAt ℝ s x), derivWithin (fun (x : ℝ) ↦ a ^ f x) s x = log a * derivWithin f s x * a ^ f x
Tactic: by_cases hxs : UniqueDiffWithinAt ℝ s x