awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
p_1 : 𝕜[X]
x : 𝕜
p q : 𝕜[X]
hp : HasStrictDerivAt (fun (x : 𝕜) ↦ eval x p) (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)) x
hq : HasStrictDerivAt (fun (x : 𝕜) ↦ eval x q) (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) q)) x
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ eval x (p + q)) (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) (p + q))) x

Tactic:
simpa using hp.add hq

Premises used: HasStrictDerivAt.add
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
p : 𝕜[X]
x : 𝕜
n : ℕ
a : 𝕜
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ eval x ((monomial n : (a : 𝕜) → 𝕜[X]) a))
    (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) ((monomial n : (a : 𝕜) → 𝕜[X]) a))) x

Tactic:
simpa [mul_assoc, derivative_monomial]
                      using (hasStrictDerivAt_pow n x).const_mul a

Premises used: Polynomial.derivative_monomial, HasStrictDerivAt.const_mul, mul_assoc, hasStrictDerivAt_pow
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
p : 𝕜[X]
x : 𝕜
add :
  ∀ (p q : 𝕜[X]) (hp : HasStrictDerivAt (fun (x : 𝕜) ↦ eval x p) (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)) x)
    (hq : HasStrictDerivAt (fun (x : 𝕜) ↦ eval x q) (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) q)) x),
    HasStrictDerivAt (fun (x : 𝕜) ↦ eval x (p + q)) (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) (p + q))) x
monomial :
  ∀ (n : ℕ) (a : 𝕜),
    HasStrictDerivAt (fun (x : 𝕜) ↦ eval x ((Polynomial.monomial n : (a : 𝕜) → 𝕜[X]) a))
      (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) ((Polynomial.monomial n : (a : 𝕜) → 𝕜[X]) a))) x
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ eval x p) (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)) x

Tactic:
induction p using Polynomial.induction_on' with
  | add p q hp hq => simpa using hp.add hq
  | monomial n a => simpa [mul_assoc, derivative_monomial]
                      using (hasStrictDerivAt_pow n x).const_mul a

Premises used: Polynomial.derivative_monomial, mul_assoc, Polynomial.monomial
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R 𝕜
q : R[X]
x : 𝕜
⊢ HasStrictDerivAt (F := 𝕜) (fun (x : 𝕜) ↦ ((aeval x : (a : R[X]) → 𝕜) q : 𝕜))
    ((aeval x : (a : R[X]) → 𝕜) ((derivative : (a : R[X]) → R[X]) q : R[X]) : 𝕜) x

Tactic:
simpa only [aeval_def, eval₂_eq_eval_map, derivative_map] using
    (q.map (algebraMap R 𝕜)).hasStrictDerivAt x

Premises used: Algebra.algebraMap, Polynomial.aeval_def, Polynomial.hasStrictDerivAt, Polynomial.map, Polynomial.derivative_map, Polynomial.eval₂_eq_eval_map
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
p : 𝕜[X]
x : 𝕜
⊢ HasDerivAt (fun (x : 𝕜) ↦ eval x p) (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)) x

Tactic:
(p.hasStrictDerivAt x).hasDerivAt

Premises used: Polynomial.hasStrictDerivAt, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R 𝕜
q : R[X]
x : 𝕜
⊢ HasDerivAt (F := 𝕜) (fun (x : 𝕜) ↦ ((aeval x : (a : R[X]) → 𝕜) q : 𝕜))
    ((aeval x : (a : R[X]) → 𝕜) ((derivative : (a : R[X]) → R[X]) q : R[X]) : 𝕜) x

Tactic:
(q.hasStrictDerivAt_aeval x).hasDerivAt

Premises used: Polynomial.hasStrictDerivAt_aeval, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
p : 𝕜[X]
x : 𝕜
s : Set 𝕜
⊢ HasDerivWithinAt (fun (x : 𝕜) ↦ eval x p) (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)) s x

Tactic:
(p.hasDerivAt x).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, Polynomial.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R 𝕜
q : R[X]
x : 𝕜
s : Set 𝕜
⊢ HasDerivWithinAt (F := 𝕜) (fun (x : 𝕜) ↦ ((aeval x : (a : R[X]) → 𝕜) q : 𝕜))
    ((aeval x : (a : R[X]) → 𝕜) ((derivative : (a : R[X]) → R[X]) q : R[X]) : 𝕜) s x

Tactic:
(q.hasDerivAt_aeval x).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, Polynomial.hasDerivAt_aeval
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
p : 𝕜[X]
⊢ DifferentiableAt 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ eval x p) x

Tactic:
(p.hasDerivAt x).differentiableAt

Premises used: HasDerivAt.differentiableAt, Polynomial.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R 𝕜
q : R[X]
⊢ DifferentiableAt 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) q) x

Tactic:
(q.hasDerivAt_aeval x).differentiableAt

Premises used: HasDerivAt.differentiableAt, Polynomial.hasDerivAt_aeval
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
p : 𝕜[X]
⊢ DifferentiableWithinAt 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ eval x p) s x

Tactic:
p.differentiableAt.differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, Polynomial.differentiableAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R 𝕜
q : R[X]
⊢ DifferentiableWithinAt 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) q) s x

Tactic:
q.differentiableAt_aeval.differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, Polynomial.differentiableAt_aeval
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
p : 𝕜[X]
⊢ Differentiable 𝕜 (F := 𝕜) fun (x : 𝕜) ↦ eval x p

Tactic:
fun _ => p.differentiableAt

Premises used: Differentiable, Polynomial.differentiableAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R 𝕜
q : R[X]
⊢ Differentiable 𝕜 (F := 𝕜) fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) q

Tactic:
fun _ =>
  q.differentiableAt_aeval

Premises used: Differentiable, Polynomial.differentiableAt_aeval
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
p : 𝕜[X]
⊢ DifferentiableOn 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ eval x p) s

Tactic:
p.differentiable.differentiableOn

Premises used: Differentiable.differentiableOn, Polynomial.differentiable
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R 𝕜
q : R[X]
⊢ DifferentiableOn 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) q) s

Tactic:
q.differentiable_aeval.differentiableOn

Premises used: Polynomial.differentiable_aeval, Differentiable.differentiableOn
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
p : 𝕜[X]
⊢ deriv (fun (x : 𝕜) ↦ eval x p) x = eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)

Tactic:
(p.hasDerivAt x).deriv

Premises used: HasDerivAt.deriv, Polynomial.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R 𝕜
q : R[X]
⊢ Eq (α := 𝕜) (deriv (fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) q) x : 𝕜)
    ((aeval x : (a : R[X]) → 𝕜) ((derivative : (a : R[X]) → R[X]) q : R[X]) : 𝕜)

Tactic:
(q.hasDerivAt_aeval x).deriv

Premises used: HasDerivAt.deriv, Polynomial.hasDerivAt_aeval
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
p : 𝕜[X]
hxs : UniqueDiffWithinAt 𝕜 s x
rw : deriv (fun (x : 𝕜) ↦ eval x p) x = eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)
⊢ derivWithin (fun (x : 𝕜) ↦ eval x p) s x = eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)

Tactic:
rw [DifferentiableAt.derivWithin p.differentiableAt hxs]

Premises used: DifferentiableAt.derivWithin, Polynomial.differentiableAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
p : 𝕜[X]
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ deriv (fun (x : 𝕜) ↦ eval x p) x = eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)

Tactic:
p.deriv

Premises used: Polynomial.deriv
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
p : 𝕜[X]
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ deriv (fun (x : 𝕜) ↦ eval x p) x = eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)

Tactic:
exact p.deriv

Premises used: Polynomial.deriv
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R 𝕜
q : R[X]
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := 𝕜) (derivWithin (fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) q) s x : 𝕜)
    ((aeval x : (a : R[X]) → 𝕜) ((derivative : (a : R[X]) → R[X]) q : R[X]) : 𝕜)

Tactic:
simpa only [aeval_def, eval₂_eq_eval_map, derivative_map] using
    (q.map (algebraMap R 𝕜)).derivWithin hxs

Premises used: Algebra.algebraMap, Polynomial.derivWithin, Polynomial.aeval_def, Polynomial.map, Polynomial.derivative_map, Polynomial.eval₂_eq_eval_map
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
p : 𝕜[X]
x : 𝕜
⊢ HasFDerivAt (𝕜 := 𝕜) (fun (x : 𝕜) ↦ eval x p) (smulRight (S := 𝕜) 1 (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p))) x

Tactic:
p.hasDerivAt x

Premises used: HasFDerivAt, ContinuousLinearMap.smulRight, HasDerivAtFilter, ContinuousLinearMap.toSpanSingleton, Polynomial.hasDerivAt, LinearMap.toSpanSingleton
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R 𝕜
q : R[X]
x : 𝕜
⊢ HasFDerivAt (𝕜 := 𝕜) (F := 𝕜) (fun (x : 𝕜) ↦ ((aeval x : (a : R[X]) → 𝕜) q : 𝕜))
    (smulRight (S := 𝕜) 1 ((aeval x : (a : R[X]) → 𝕜) ((derivative : (a : R[X]) → R[X]) q : R[X])) : 𝕜 →L[𝕜] 𝕜) x

Tactic:
q.hasDerivAt_aeval x

Premises used: HasFDerivAt, ContinuousLinearMap.smulRight, HasDerivAtFilter, ContinuousLinearMap.toSpanSingleton, Polynomial.hasDerivAt_aeval, LinearMap.toSpanSingleton
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
p : 𝕜[X]
x : 𝕜
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (fun (x : 𝕜) ↦ eval x p)
    (smulRight (S := 𝕜) 1 (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p))) s x

Tactic:
(p.hasFDerivAt x).hasFDerivWithinAt

Premises used: HasFDerivAt.hasFDerivWithinAt, Polynomial.hasFDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R 𝕜
q : R[X]
x : 𝕜
⊢ HasFDerivWithinAt (𝕜 := 𝕜) (F := 𝕜) (fun (x : 𝕜) ↦ ((aeval x : (a : R[X]) → 𝕜) q : 𝕜))
    (smulRight (S := 𝕜) 1 ((aeval x : (a : R[X]) → 𝕜) ((derivative : (a : R[X]) → R[X]) q : R[X])) : 𝕜 →L[𝕜] 𝕜) s x

Tactic:
(q.hasFDerivAt_aeval x).hasFDerivWithinAt

Premises used: HasFDerivAt.hasFDerivWithinAt, Polynomial.hasFDerivAt_aeval
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
p : 𝕜[X]
⊢ Eq (α := 𝕜 →L[𝕜] 𝕜) (fderiv 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ eval x p) x : 𝕜 →L[𝕜] 𝕜)
    (smulRight (S := 𝕜) 1 (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)) : 𝕜 →L[𝕜] 𝕜)

Tactic:
(p.hasFDerivAt x).fderiv

Premises used: Polynomial.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R 𝕜
q : R[X]
⊢ Eq (α := 𝕜 →L[𝕜] 𝕜) (fderiv 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) q) x : 𝕜 →L[𝕜] 𝕜)
    (smulRight (S := 𝕜) 1 ((aeval x : (a : R[X]) → 𝕜) ((derivative : (a : R[X]) → R[X]) q : R[X])) : 𝕜 →L[𝕜] 𝕜)

Tactic:
(q.hasFDerivAt_aeval x).fderiv

Premises used: Polynomial.hasFDerivAt_aeval, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
p : 𝕜[X]
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := 𝕜 →L[𝕜] 𝕜) (fderivWithin 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ eval x p) s x : 𝕜 →L[𝕜] 𝕜)
    (smulRight (S := 𝕜) 1 (eval x ((derivative : (a : 𝕜[X]) → 𝕜[X]) p)) : 𝕜 →L[𝕜] 𝕜)

Tactic:
(p.hasFDerivWithinAt x).fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, Polynomial.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Polynomial
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R 𝕜
q : R[X]
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := 𝕜 →L[𝕜] 𝕜) (fderivWithin 𝕜 (F := 𝕜) (fun (x : 𝕜) ↦ (aeval x : (a : R[X]) → 𝕜) q) s x : 𝕜 →L[𝕜] 𝕜)
    (smulRight (S := 𝕜) 1 ((aeval x : (a : R[X]) → 𝕜) ((derivative : (a : R[X]) → R[X]) q : R[X])) : 𝕜 →L[𝕜] 𝕜)

Tactic:
(q.hasFDerivWithinAt_aeval x).fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, Polynomial.hasFDerivWithinAt_aeval
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
f' : 𝔸
x : 𝕜
h : HasStrictDerivAt f f' x
n : ℕ
⊢ HasStrictDerivAt.{u_1, u_2} (F := 𝔸) (fun (x : 𝕜) ↦ f x ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i)
    x

Tactic:
simpa using h.hasStrictFDerivAt.pow' n |>.hasStrictDerivAt

Premises used: HasStrictDerivAt.hasStrictFDerivAt, HasStrictFDerivAt.hasStrictDerivAt, HasStrictFDerivAt.pow'
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
f' : 𝔸
x : 𝕜
h : HasStrictDerivAt f f' x
n : ℕ
⊢ HasStrictDerivAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) x

Tactic:
h.fun_pow' n

Premises used: HasStrictDerivAt.fun_pow'
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
f' : 𝔸
x : 𝕜
s : Set 𝕜
h : HasDerivWithinAt f f' s x
n : ℕ
⊢ HasDerivWithinAt.{u_1, u_2} (F := 𝔸) (fun (x : 𝕜) ↦ f x ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i)
    s x

Tactic:
simpa using h.hasFDerivWithinAt.pow' n |>.hasDerivWithinAt

Premises used: HasDerivWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.hasDerivWithinAt, HasFDerivWithinAt.pow'
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
f' : 𝔸
x : 𝕜
s : Set 𝕜
h : HasDerivWithinAt f f' s x
n : ℕ
⊢ HasDerivWithinAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) s x

Tactic:
h.fun_pow' n

Premises used: HasDerivWithinAt.fun_pow'
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
f' : 𝔸
x : 𝕜
h : HasDerivAt f f' x
n : ℕ
⊢ HasDerivAt.{u_1, u_2} (F := 𝔸) (fun (x : 𝕜) ↦ f x ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) x

Tactic:
simpa using h.hasFDerivAt.pow' n |>.hasDerivAt

Premises used: HasDerivAt.hasFDerivAt, HasFDerivAt.hasDerivAt, HasFDerivAt.pow'
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
f' : 𝔸
x : 𝕜
h : HasDerivAt f f' x
n : ℕ
⊢ HasDerivAt (f ^ n) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * f' * f x ^ i) x

Tactic:
h.fun_pow' n

Premises used: HasDerivAt.fun_pow'
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    Eq.{u_2 + 1} (α := 𝔸) (derivWithin (fun (x : 𝕜) ↦ f x ^ n) s x)
      (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i)
neg :
  ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
    Eq.{u_2 + 1} (α := 𝔸) (derivWithin (fun (x : 𝕜) ↦ f x ^ n) s x)
      (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i)
⊢ Eq.{u_2 + 1} (α := 𝔸) (derivWithin (fun (x : 𝕜) ↦ f x ^ n) s x)
    (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i)

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ Eq.{u_2 + 1} (α := 𝔸) (derivWithin (fun (x : 𝕜) ↦ f x ^ n) s x)
    (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i)

Tactic:
(h.hasDerivWithinAt.pow' n).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.pow'
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ Eq.{u_2 + 1} (α := 𝔸) (derivWithin (fun (x : 𝕜) ↦ f x ^ n) s x)
    (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i)

Tactic:
exact (h.hasDerivWithinAt.pow' n).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.pow'
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ Eq.{u_2 + 1} (α := 𝔸) (derivWithin (fun (x : 𝕜) ↦ f x ^ n) s x)
    (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i)

Tactic:
simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Premises used: derivWithin_zero_of_not_uniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
⊢ derivWithin (f ^ n) s x = ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i

Tactic:
derivWithin_fun_pow' h n

Premises used: derivWithin_fun_pow'
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
h : DifferentiableAt 𝕜 f x
n : ℕ
⊢ Eq.{u_2 + 1} (α := 𝔸) (deriv (fun (x : 𝕜) ↦ f x ^ n) x)
    (∑ i ∈ Finset.range n, f x ^ (n.pred - i) * deriv f x * f x ^ i)

Tactic:
(h.hasDerivAt.pow' n).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.pow'
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
h : DifferentiableAt 𝕜 f x
n : ℕ
⊢ deriv (f ^ n) x = ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * deriv f x * f x ^ i

Tactic:
deriv_fun_pow' h n

Premises used: deriv_fun_pow'
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
f' : 𝔸
x : 𝕜
h : HasStrictDerivAt f f' x
n : ℕ
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ f x ^ n) ((↑n : 𝔸) * f x ^ (n - 1) * f') x

Tactic:
simpa using h.hasStrictFDerivAt.pow n |>.hasStrictDerivAt

Premises used: HasStrictFDerivAt.pow, HasStrictDerivAt.hasStrictFDerivAt, HasStrictFDerivAt.hasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
f' : 𝔸
x : 𝕜
h : HasStrictDerivAt f f' x
n : ℕ
⊢ HasStrictDerivAt (f ^ n) ((↑n : 𝔸) * f x ^ (n - 1) * f') x

Tactic:
h.fun_pow n

Premises used: HasStrictDerivAt.fun_pow
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
f' : 𝔸
x : 𝕜
s : Set 𝕜
h : HasDerivWithinAt f f' s x
n : ℕ
⊢ HasDerivWithinAt (fun (x : 𝕜) ↦ f x ^ n) ((↑n : 𝔸) * f x ^ (n - 1) * f') s x

Tactic:
simpa using h.hasFDerivWithinAt.pow n |>.hasDerivWithinAt

Premises used: HasFDerivWithinAt.pow, HasDerivWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
f' : 𝔸
x : 𝕜
s : Set 𝕜
h : HasDerivWithinAt f f' s x
n : ℕ
⊢ HasDerivWithinAt (f ^ n) ((↑n : 𝔸) * f x ^ (n - 1) * f') s x

Tactic:
h.fun_pow n

Premises used: HasDerivWithinAt.fun_pow
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
f' : 𝔸
x : 𝕜
h : HasDerivAt f f' x
n : ℕ
⊢ HasDerivAt (f ^ n) ((↑n : 𝔸) * f x ^ (n - 1) * f') x

Tactic:
simpa using h.hasFDerivAt.pow n |>.hasDerivAt

Premises used: HasDerivAt.hasFDerivAt, HasFDerivAt.pow, HasFDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (f ^ n) s x = (↑n : 𝔸) * f x ^ (n - 1) * derivWithin f s x
neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (f ^ n) s x = (↑n : 𝔸) * f x ^ (n - 1) * derivWithin f s x
⊢ derivWithin (f ^ n) s x = (↑n : 𝔸) * f x ^ (n - 1) * derivWithin f s x

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (f ^ n) s x = (↑n : 𝔸) * f x ^ (n - 1) * derivWithin f s x

Tactic:
(h.hasDerivWithinAt.pow n).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.pow
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (f ^ n) s x = (↑n : 𝔸) * f x ^ (n - 1) * derivWithin f s x

Tactic:
exact (h.hasDerivWithinAt.pow n).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.pow
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 f s x
n : ℕ
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (f ^ n) s x = (↑n : 𝔸) * f x ^ (n - 1) * derivWithin f s x

Tactic:
simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Premises used: derivWithin_zero_of_not_uniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedCommRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
f : 𝕜 → 𝔸
x : 𝕜
h : DifferentiableAt 𝕜 f x
n : ℕ
⊢ deriv (f ^ n) x = (↑n : 𝔸) * f x ^ (n - 1) * deriv f x

Tactic:
(h.hasDerivAt.pow n).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.pow, HasDerivAt.deriv
-- Module: Mathlib.Analysis.Calculus.Deriv.Pow
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ
x : 𝕜
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ x ^ n) ((↑n : 𝕜) * x ^ (n - 1)) x

Tactic:
simpa using (hasStrictDerivAt_id x).pow n

Premises used: HasStrictDerivAt.pow, hasStrictDerivAt_id