awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  ∀ (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)
⊢ 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:
ext y
-- 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 : ℝ))
y : ℝ
a :
  y ^ (r - (↑k : ℝ) - 1) = y ^ (r - HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) ∨
    Polynomial.eval r (descPochhammer ℝ k) = 0 ∨ r - (↑k : ℝ) = 0
⊢ 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:
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]

Premises used: Polynomial.eval_X, Real.deriv_rpow_const, mul_assoc, mul_eq_mul_left_iff, Polynomial.eval_natCast, descPochhammer_succ_right, deriv_const_mul_field, Polynomial.eval_mul, mul_eq_zero, Polynomial.eval_sub
-- 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 : ℝ))
y : ℝ
⊢ y ^ (r - (↑k : ℝ) - 1) = y ^ (r - HAdd.hAdd (α := ℝ) (↑k : ℝ) 1) ∨
    Polynomial.eval r (descPochhammer ℝ k) = 0 ∨ r - (↑k : ℝ) = 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
r x : ℝ
k : ℕ
a :
  Eq (α := (x : ℝ) → ℝ) (deriv^[0] fun (x : ℝ) ↦ x ^ r) fun (x : ℝ) ↦
    Polynomial.eval r (descPochhammer ℝ 0) * x ^ (r - (↑0 : ℝ))
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) : ℝ))
⊢ Eq (α := (x : ℝ) → ℝ) (deriv^[k] fun (x : ℝ) ↦ x ^ r) fun (x : ℝ) ↦
    Polynomial.eval r (descPochhammer ℝ k) * x ^ (r - (↑k : ℝ))

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

Premises used: Polynomial.eval_X, Real.deriv_rpow_const, Function.iterate_succ', mul_assoc, mul_eq_mul_left_iff, Polynomial.eval_natCast, descPochhammer_succ_right, deriv_const_mul_field, Polynomial.eval_mul, mul_eq_zero, Nat.cast_add, Function.comp_apply, Polynomial.eval_sub, Nat.cast_one
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
x p : ℝ
hx : x ≠ 0 ∨ 1 ≤ p
rwa rwa₁ rwa₂ rwa₃ : ∀ (hx : x ≠ 0 ∨ (↑1 : ℝ) ≤ p), x ≠ 0 ∨ (↑1 : ℝ) ≤ p
⊢ x ≠ 0 ∨ (↑1 : ℝ) ≤ p

Tactic:
rwa [← Nat.cast_one] at hx

Premises used: Nat.cast_one
-- 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
h : 0 < f x
⊢ HasFDerivWithinAt (fun (x : E) ↦ f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') s x

Tactic:
(hasStrictFDerivAt_rpow_of_pos (f x, g x) h).hasFDerivAt.comp_hasFDerivWithinAt x
    (hf.prodMk hg)

Premises used: ContinuousLinearMap.comp, 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
h : 0 < f x
⊢ HasFDerivWithinAt (fun (x : E) ↦ f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') s x

Tactic:
exact (hasStrictFDerivAt_rpow_of_pos (f x, g x) h).hasFDerivAt.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
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
h : 0 < f x
⊢ HasFDerivAt (fun (x : E) ↦ f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') x

Tactic:
(hasStrictFDerivAt_rpow_of_pos (f x, g x) h).hasFDerivAt.comp x (hf.prodMk hg)

Premises used: ContinuousLinearMap.comp, 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
h : 0 < f x
⊢ HasFDerivAt (fun (x : E) ↦ f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') x

Tactic:
exact (hasStrictFDerivAt_rpow_of_pos (f x, g x) h).hasFDerivAt.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 : HasStrictFDerivAt f f' x
hg : HasStrictFDerivAt g g' x
h : 0 < f x
⊢ HasStrictFDerivAt (fun (x : E) ↦ f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') x

Tactic:
(hasStrictFDerivAt_rpow_of_pos (f x, g x) h).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 g : E → ℝ
x : E
s : Set E
hf : DifferentiableWithinAt ℝ f s x
hg : DifferentiableWithinAt ℝ g s x
h : f x ≠ 0
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ f x ^ g x) s x

Tactic:
(differentiableAt_rpow_of_ne (f x, g x) h).comp_differentiableWithinAt x (hf.prodMk hg)

Premises used: DifferentiableWithinAt.prodMk, DifferentiableAt.comp_differentiableWithinAt
-- 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
h : f x ≠ 0
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ f x ^ g x) s x

Tactic:
exact (differentiableAt_rpow_of_ne (f x, g x) h).comp_differentiableWithinAt x (hf.prodMk hg)

Premises used: DifferentiableWithinAt.prodMk, DifferentiableAt.comp_differentiableWithinAt
-- 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
h : f x ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ f x ^ g x) x

Tactic:
(differentiableAt_rpow_of_ne (f x, g x) h).comp x (hf.prodMk hg)

Premises used: DifferentiableAt.prodMk, DifferentiableAt.comp
-- 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
h : f x ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ f x ^ g x) x

Tactic:
exact (differentiableAt_rpow_of_ne (f x, g x) h).comp x (hf.prodMk hg)

Premises used: DifferentiableAt.prodMk, DifferentiableAt.comp
-- 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
h : ∀ x ∈ s, f x ≠ 0
⊢ DifferentiableOn ℝ (F := ℝ) (fun (x : E) ↦ f x ^ g x) s

Tactic:
fun x hx =>
  (hf x hx).rpow (hg x hx) (h x hx)

Premises used: DifferentiableOn, DifferentiableWithinAt.rpow
-- 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
h : ∀ (x : E), f x ≠ 0
⊢ Differentiable ℝ (F := ℝ) fun (x : E) ↦ f x ^ g x

Tactic:
fun x => (hf x).rpow (hg x) (h x)

Premises used: Differentiable, DifferentiableAt.rpow
-- 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
p : ℝ
hf : HasFDerivWithinAt f f' s x
h : f x ≠ 0 ∨ 1 ≤ p
⊢ HasFDerivWithinAt (fun (x : E) ↦ f x ^ p) ((p * f x ^ (p - 1)) • f') s x

Tactic:
(hasDerivAt_rpow_const h).comp_hasFDerivWithinAt x hf

Premises used: HasDerivAt.comp_hasFDerivWithinAt, Real.hasDerivAt_rpow_const
-- 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
p : ℝ
hf : HasFDerivAt f f' x
h : f x ≠ 0 ∨ 1 ≤ p
⊢ HasFDerivAt (fun (x : E) ↦ f x ^ p) ((p * f x ^ (p - 1)) • f') x

Tactic:
(hasDerivAt_rpow_const h).comp_hasFDerivAt x hf

Premises used: Real.hasDerivAt_rpow_const, HasDerivAt.comp_hasFDerivAt
-- 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
p : ℝ
hf : HasStrictFDerivAt f f' x
h : f x ≠ 0 ∨ 1 ≤ p
⊢ HasStrictFDerivAt (fun (x : E) ↦ f x ^ p) ((p * f x ^ (p - 1)) • f') x

Tactic:
(hasStrictDerivAt_rpow_const h).comp_hasStrictFDerivAt x hf

Premises used: HasStrictDerivAt.comp_hasStrictFDerivAt, Real.hasStrictDerivAt_rpow_const
-- 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
p : ℝ
hf : DifferentiableWithinAt ℝ f s x
h : f x ≠ 0 ∨ 1 ≤ p
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ f x ^ p) s x

Tactic:
(hf.hasFDerivWithinAt.rpow_const h).differentiableWithinAt

Premises used: HasFDerivWithinAt.rpow_const, 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
p : ℝ
hf : DifferentiableAt ℝ f x
h : f x ≠ 0 ∨ 1 ≤ p
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ f x ^ p) x

Tactic:
(hf.hasFDerivAt.rpow_const h).differentiableAt

Premises used: HasFDerivAt.rpow_const, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
p : ℝ
hf : DifferentiableOn ℝ f s
h : ∀ x ∈ s, f x ≠ 0 ∨ 1 ≤ p
⊢ DifferentiableOn ℝ (F := ℝ) (fun (x : E) ↦ f x ^ p) s

Tactic:
fun x hx => (hf x hx).rpow_const (h x hx)

Premises used: DifferentiableWithinAt.rpow_const, DifferentiableOn
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
p : ℝ
hf : Differentiable ℝ f
h : ∀ (x : E), f x ≠ 0 ∨ 1 ≤ p
⊢ Differentiable ℝ (F := ℝ) fun (x : E) ↦ f x ^ p

Tactic:
fun x => (hf x).rpow_const (h x)

Premises used: Differentiable, DifferentiableAt.rpow_const
-- 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
hc : 0 < c
⊢ HasFDerivWithinAt (fun (x : E) ↦ c ^ f x) ((c ^ f x * Real.log c) • f') s x

Tactic:
(hasStrictDerivAt_const_rpow hc (f x)).hasDerivAt.comp_hasFDerivWithinAt x hf

Premises used: HasDerivAt.comp_hasFDerivWithinAt, HasStrictDerivAt.hasDerivAt, Real.hasStrictDerivAt_const_rpow
-- 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
hc : 0 < c
⊢ HasFDerivAt (fun (x : E) ↦ c ^ f x) ((c ^ f x * Real.log c) • f') x

Tactic:
(hasStrictDerivAt_const_rpow hc (f x)).hasDerivAt.comp_hasFDerivAt x hf

Premises used: HasStrictDerivAt.hasDerivAt, HasDerivAt.comp_hasFDerivAt, Real.hasStrictDerivAt_const_rpow
-- 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
hc : 0 < c
⊢ HasStrictFDerivAt (fun (x : E) ↦ c ^ f x) ((c ^ f x * Real.log c) • f') x

Tactic:
(hasStrictDerivAt_const_rpow hc (f x)).comp_hasStrictFDerivAt x hf

Premises used: HasStrictDerivAt.comp_hasStrictFDerivAt, Real.hasStrictDerivAt_const_rpow
-- 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
n : WithTop ℕ∞
hf : ContDiffWithinAt ℝ n f s x
hg : ContDiffWithinAt ℝ n g s x
h : f x ≠ 0
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (x : E) ↦ f x ^ g x) s x

Tactic:
(contDiffAt_rpow_of_ne (f x, g x) h).comp_contDiffWithinAt x (hf.prodMk hg)

Premises used: ContDiffAt.comp_contDiffWithinAt, ContDiffWithinAt.prodMk
-- 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
n : WithTop ℕ∞
hf : ContDiffWithinAt ℝ n f s x
hg : ContDiffWithinAt ℝ n g s x
h : f x ≠ 0
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (x : E) ↦ f x ^ g x) s x

Tactic:
exact (contDiffAt_rpow_of_ne (f x, g x) h).comp_contDiffWithinAt x (hf.prodMk hg)

Premises used: ContDiffAt.comp_contDiffWithinAt, ContDiffWithinAt.prodMk
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : E → ℝ
x : E
n : WithTop ℕ∞
hf : ContDiffAt ℝ n f x
hg : ContDiffAt ℝ n g x
h : f x ≠ 0
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ f x ^ g x) x

Tactic:
(contDiffAt_rpow_of_ne (f x, g x) h).comp x (hf.prodMk hg)

Premises used: ContDiffAt.comp, ContDiffAt.prodMk
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : E → ℝ
x : E
n : WithTop ℕ∞
hf : ContDiffAt ℝ n f x
hg : ContDiffAt ℝ n g x
h : f x ≠ 0
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ f x ^ g x) x

Tactic:
exact (contDiffAt_rpow_of_ne (f x, g x) h).comp x (hf.prodMk hg)

Premises used: ContDiffAt.comp, ContDiffAt.prodMk
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : E → ℝ
s : Set E
n : WithTop ℕ∞
hf : ContDiffOn ℝ n f s
hg : ContDiffOn ℝ n g s
h : ∀ x ∈ s, f x ≠ 0
⊢ ContDiffOn ℝ (F := ℝ) n (fun (x : E) ↦ f x ^ g x) s

Tactic:
fun x hx => (hf x hx).rpow (hg x hx) (h x hx)

Premises used: ContDiffOn, ContDiffWithinAt.rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : E → ℝ
n : ℕ∞ω
hf : ContDiff ℝ n f
hg : ContDiff ℝ n g
h : ∀ (x : E), f x ≠ 0
⊢ ContDiff ℝ (F := ℝ) n fun (x : E) ↦ f x ^ g x

Tactic:
contDiff_iff_contDiffAt.mpr fun x => hf.contDiffAt.rpow hg.contDiffAt (h x)

Premises used: Iff.mpr, ContDiffAt.rpow, contDiff_iff_contDiffAt, ContDiff.contDiffAt
-- 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
p : ℝ
n : WithTop ℕ∞
hf : ContDiffWithinAt ℝ n f s x
h : f x ≠ 0
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (x : E) ↦ f x ^ p) s x

Tactic:
hf.rpow contDiffWithinAt_const h

Premises used: contDiffWithinAt_const, ContDiffWithinAt.rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
p : ℝ
n : WithTop ℕ∞
hf : ContDiffAt ℝ n f x
h : f x ≠ 0
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : E) ↦ f x ^ p) x

Tactic:
hf.rpow contDiffAt_const h

Premises used: ContDiffAt.rpow, contDiffAt_const
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
p : ℝ
n : WithTop ℕ∞
hf : ContDiffOn ℝ n f s
h : ∀ x ∈ s, f x ≠ 0
⊢ ContDiffOn ℝ (F := ℝ) n (fun (x : E) ↦ f x ^ p) s

Tactic:
fun x hx => (hf x hx).rpow_const_of_ne (h x hx)

Premises used: ContDiffOn, ContDiffWithinAt.rpow_const_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
p : ℝ
n : ℕ∞ω
hf : ContDiff ℝ n f
h : ∀ (x : E), f x ≠ 0
⊢ ContDiff ℝ (F := ℝ) n fun (x : E) ↦ f x ^ p

Tactic:
hf.rpow contDiff_const h

Premises used: contDiff_const, ContDiff.rpow
-- 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
p : ℝ
m : ℕ
hf : ContDiffWithinAt ℝ (↑m : WithTop ℕ∞) f s x
h : (↑m : ℝ) ≤ p
⊢ ContDiffWithinAt ℝ (F := ℝ) (↑m : WithTop ℕ∞) (fun (x : E) ↦ f x ^ p) s x

Tactic:
(contDiffAt_rpow_const_of_le h).comp_contDiffWithinAt x hf

Premises used: Real.contDiffAt_rpow_const_of_le, ContDiffAt.comp_contDiffWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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
⊢ ContDiffWithinAt ℝ (↑m : WithTop ℕ∞) f Set.univ x

Tactic:
rw [← contDiffWithinAt_univ] at *

Premises used: contDiffWithinAt_univ
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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
hf₁ : ContDiffWithinAt ℝ (↑m : WithTop ℕ∞) f Set.univ x
⊢ (↑m : ℝ) ≤ p

Tactic:
rw [← contDiffWithinAt_univ] at *

Premises used: contDiffWithinAt_univ
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
p : ℝ
m : ℕ
hf : ContDiffWithinAt ℝ (↑m : WithTop ℕ∞) f Set.univ x
h : (↑m : ℝ) ≤ p
⊢ ContDiffWithinAt ℝ (F := ℝ) (↑m : WithTop ℕ∞) (fun (x : E) ↦ f x ^ p) Set.univ x

Tactic:
hf.rpow_const_of_le h

Premises used: ContDiffWithinAt.rpow_const_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
p : ℝ
m : ℕ
hf : ContDiffWithinAt ℝ (↑m : WithTop ℕ∞) f Set.univ x
h : (↑m : ℝ) ≤ p
⊢ ContDiffWithinAt ℝ (F := ℝ) (↑m : WithTop ℕ∞) (fun (x : E) ↦ f x ^ p) Set.univ x

Tactic:
exact hf.rpow_const_of_le h

Premises used: ContDiffWithinAt.rpow_const_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
p : ℝ
m : ℕ
hf : ContDiffOn ℝ (↑m : WithTop ℕ∞) f s
h : (↑m : ℝ) ≤ p
⊢ ContDiffOn ℝ (F := ℝ) (↑m : WithTop ℕ∞) (fun (x : E) ↦ f x ^ p) s

Tactic:
fun x hx => (hf x hx).rpow_const_of_le h

Premises used: ContDiffOn, ContDiffWithinAt.rpow_const_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
p : ℝ
m : ℕ
hf : ContDiff ℝ (↑m : ℕ∞ω) f
h : (↑m : ℝ) ≤ p
⊢ ContDiff ℝ (F := ℝ) (↑m : ℕ∞ω) fun (x : E) ↦ f x ^ p

Tactic:
contDiff_iff_contDiffAt.mpr fun _ => hf.contDiffAt.rpow_const_of_le h

Premises used: Iff.mpr, ContDiffAt.rpow_const_of_le, contDiff_iff_contDiffAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
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 (F := ℝ) (fun (x : ℝ) ↦ f x ^ g 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 :
      ℝ)
    s x

Tactic:
(hf.hasFDerivWithinAt.rpow hg.hasFDerivWithinAt h).hasDerivWithinAt

Premises used: HasDerivWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.hasDerivWithinAt, HasFDerivWithinAt.rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f g : ℝ → ℝ
f' g' x : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
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
⊢ 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

Tactic:
convert! (hf.hasFDerivWithinAt.rpow hg.hasFDerivWithinAt h).hasDerivWithinAt using 1

Premises used: HasDerivWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.hasDerivWithinAt, HasFDerivWithinAt.rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f g : ℝ → ℝ
f' g' x : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
h : 0 < f x
⊢ f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x) =
    g x * f x ^ (g x - 1) * (1 * f') + f x ^ g x * Real.log (f x) * (1 * g')

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f g : ℝ → ℝ
f' g' x : ℝ
hf : HasDerivAt f f' x
hg : HasDerivAt g g' x
h : 0 < f x
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
⊢ 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

Tactic:
rw [← hasDerivWithinAt_univ] at *

Premises used: hasDerivWithinAt_univ
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f g : ℝ → ℝ
f' g' x : ℝ
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:
hf.rpow hg h

Premises used: HasDerivWithinAt.rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f g : ℝ → ℝ
f' g' x : ℝ
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:
exact hf.rpow hg h

Premises used: HasDerivWithinAt.rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
f' x p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ HasDerivWithinAt ((fun (x : ℝ) ↦ x ^ p) ∘ f) (p * f x ^ (p - 1) * f') s x

Tactic:
(hasDerivAt_rpow_const hx).comp_hasDerivWithinAt x hf

Premises used: Real.hasDerivAt_rpow_const, HasDerivAt.comp_hasDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
f' x p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0 ∨ 1 ≤ p
h : f' * p * f x ^ (p - 1) = p * f x ^ (p - 1) * f'
⊢ HasDerivWithinAt (fun (y : ℝ) ↦ f y ^ p) (f' * p * f x ^ (p - 1)) s x

Tactic:
convert! (hasDerivAt_rpow_const hx).comp_hasDerivWithinAt x hf using 1

Premises used: Real.hasDerivAt_rpow_const, HasDerivAt.comp_hasDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
f' x p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0 ∨ 1 ≤ p
⊢ f' * p * f x ^ (p - 1) = p * f x ^ (p - 1) * f'

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Goal:
f : ℝ → ℝ
f' x p : ℝ
hf : HasDerivAt f f' x
hx : f x ≠ 0 ∨ 1 ≤ p
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
⊢ HasDerivAt (fun (y : ℝ) ↦ f y ^ p) (f' * p * f x ^ (p - 1)) x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Premises used: hasDerivWithinAt_univ