awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
j : ι
hij : j ≠ i
⊢ HasFDerivAt.{u_1, u_3, u_3} (𝕜 := 𝕜) (F := E j) (fun (x_1 : E i) ↦ Function.update (β := E) x i x_1 j)
    (Pi.single (M := fun (i_1 : ι) ↦ E i →L[𝕜] E i_1) i (ContinuousLinearMap.id 𝕜 (E i) : E i →L[𝕜] E i) j) y

Tactic:
simpa [hij] using hasFDerivAt_const _ _

Premises used: hasFDerivAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
i : ι
y : E i
⊢ HasFDerivAt (𝕜 := 𝕜) (Pi.single (M := E) i)
    (ContinuousLinearMap.pi (φ := E)
      (Pi.single (M := fun (i_1 : ι) ↦ E i →L[𝕜] E i_1) i (ContinuousLinearMap.id 𝕜 (E i))))
    y

Tactic:
hasFDerivAt_update 0 y

Premises used: Pi.single, hasFDerivAt_update, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
x : (i : ι) → E i
i : ι
y : E i
⊢ Eq (α := E i →L[𝕜] (a : ι) → E a) (fderiv 𝕜 (Function.update (β := E) x i) y : E i →L[𝕜] (a : ι) → E a)
    (ContinuousLinearMap.pi (φ := E)
        (Pi.single (M := fun (i_1 : ι) ↦ E i →L[𝕜] E i_1) i (ContinuousLinearMap.id 𝕜 (E i))) :
      E i →L[𝕜] (i : ι) → E i)

Tactic:
(hasFDerivAt_update x y).fderiv

Premises used: hasFDerivAt_update, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
E : ι → Type u_3
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (E i)
i : ι
y : E i
⊢ Eq (α := E i →L[𝕜] (j : ι) → E j) (fderiv 𝕜 (Pi.single (M := E) i) y : E i →L[𝕜] (j : ι) → E j)
    (ContinuousLinearMap.pi (φ := E)
        (Pi.single (M := fun (i_1 : ι) ↦ E i →L[𝕜] E i_1) i (ContinuousLinearMap.id 𝕜 (E i))) :
      E i →L[𝕜] (i : ι) → E i)

Tactic:
fderiv_update 0 y

Premises used: Pi.single, fderiv_update, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n : ℕ
rw :
  ∑ x_1 ∈ Finset.range (n + 1), f x •> (f x ^ ((n + 1).pred - x_1) •> f' <• f x ^ x_1) + f' <• f x ^ (n + 1) =
    ∑ x_1 ∈ Finset.range (n + 1), f x ^ ((n + 1 + 1).pred - x_1) •> f' <• f x ^ x_1 +
      f x ^ ((n + 1 + 1).pred - (n + 1)) •> f' <• f x ^ (n + 1)
⊢ f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• f x ^ (n + 1) =
    ∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i

Tactic:
rw [Finset.sum_range_succ _ (n + 1), Finset.smul_sum]

Premises used: HAdd.hAdd, Finset.smul_sum, OfNat.ofNat, Finset.sum_range_succ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n : ℕ
simp :
  ∑ x_1 ∈ Finset.range (n + 1), f x •> (f x ^ (n - x_1) •> f' <• f x ^ x_1) + f' <• f x ^ (n + 1) =
    ∑ x_1 ∈ Finset.range (n + 1), f x ^ (n + 1 - x_1) •> f' <• f x ^ x_1 + f' <• f x ^ (n + 1)
⊢ ∑ x_1 ∈ Finset.range (n + 1), f x •> (f x ^ ((n + 1).pred - x_1) •> f' <• f x ^ x_1) + f' <• f x ^ (n + 1) =
    ∑ x_1 ∈ Finset.range (n + 1), f x ^ ((n + 1 + 1).pred - x_1) •> f' <• f x ^ x_1 +
      f x ^ ((n + 1 + 1).pred - (n + 1)) •> f' <• f x ^ (n + 1)

Tactic:
simp only [Nat.pred_eq_sub_one, add_tsub_cancel_right, tsub_self, pow_zero, one_smul]

Premises used: tsub_self, pow_zero, one_smul, Nat.pred_eq_sub_one, add_tsub_cancel_right
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n : ℕ
simp_rw :
  ∑ x_1 ∈ Finset.range (n + 1), f x ^ (n - x_1 + 1) •> f' <• f x ^ x_1 + f' <• f x ^ (n + 1) =
    ∑ x_1 ∈ Finset.range (n + 1), f x ^ (n + 1 - x_1) •> f' <• f x ^ x_1 + f' <• f x ^ (n + 1)
⊢ ∑ x_1 ∈ Finset.range (n + 1), f x •> (f x ^ (n - x_1) •> f' <• f x ^ x_1) + f' <• f x ^ (n + 1) =
    ∑ x_1 ∈ Finset.range (n + 1), f x ^ (n + 1 - x_1) •> f' <• f x ^ x_1 + f' <• f x ^ (n + 1)

Tactic:
simp_rw [smul_comm (_ : 𝔸) (_ : 𝔸ᵐᵒᵖ), smul_smul, ← pow_succ']

Premises used: smul_smul, SMulCommClass.smul_comm, pow_succ'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
n : ℕ
h : ∀ (x : ℕ) (hx : x ∈ Finset.range (n + 1)), n - x + 1 = n + 1 - x
⊢ ∑ x_1 ∈ Finset.range (n + 1), f x ^ (n - x_1 + 1) •> f' <• f x ^ x_1 + f' <• f x ^ (n + 1) =
    ∑ x_1 ∈ Finset.range (n + 1), f x ^ (n + 1 - x_1) •> f' <• f x ^ x_1 + f' <• f x ^ (n + 1)

Tactic:
congr! 5 with x hx
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x_1 : E
n x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ x ≤ n

Tactic:
simp only [Finset.mem_range, Nat.lt_succ_iff] at hx

Premises used: Finset.mem_range, Nat.lt_succ_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x_1 : E
n x : ℕ
hx : x ≤ n
h h₁ : n + 1 - x = n + 1 - x
⊢ n - x + 1 = n + 1 - x

Tactic:
rw [tsub_add_eq_add_tsub hx]

Premises used: tsub_add_eq_add_tsub
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasStrictFDerivAt f f' x
n : ℕ
⊢ HasStrictFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (HPow.hPow (β := ℕ) f 0)
    (∑ i ∈ Finset.range 0, f x ^ (Nat.pred 0 - i) •> f' <• f x ^ i) x

Tactic:
simpa using hasStrictFDerivAt_const 1 x

Premises used: hasStrictFDerivAt_const, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasStrictFDerivAt f f' x
n : ℕ
⊢ HasStrictFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (HPow.hPow (β := ℕ) f 1)
    (∑ i ∈ Finset.range 1, f x ^ (Nat.pred 1 - i) •> f' <• f x ^ i) x

Tactic:
simpa using h
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasStrictFDerivAt f f' x
n_1 n : ℕ
⊢ HasStrictFDerivAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) x

Tactic:
have := h.mul' (h.pow' (n + 1))
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasStrictFDerivAt f f' x
n_1 n : ℕ
this :
  HasStrictFDerivAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) x
simp_rw :
  HasStrictFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f * f ^ (n + 1))
    (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x
⊢ HasStrictFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f ^ (n + 1 + 1))
    (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x

Tactic:
simp_rw [pow_succ' _ (n + 1)]

Premises used: HAdd.hAdd, OfNat.ofNat, pow_succ'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasStrictFDerivAt f f' x
n_1 n : ℕ
this :
  HasStrictFDerivAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) x
⊢ HasStrictFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f * f ^ (n + 1))
    (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x

Tactic:
this.congr_fderiv <| aux _ _ _ _

Premises used: _private.0.aux, HasStrictFDerivAt.congr_fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasStrictFDerivAt f f' x
n_1 n : ℕ
this :
  HasStrictFDerivAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) x
⊢ HasStrictFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f * f ^ (n + 1))
    (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x

Tactic:
refine this.congr_fderiv <| aux _ _ _ _

Premises used: _private.0.aux, HasStrictFDerivAt.congr_fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
n : ℕ
x : 𝔸
⊢ HasStrictFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕜) (F := 𝔸) (fun (x : 𝔸) ↦ x ^ n)
    (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i) x

Tactic:
hasStrictFDerivAt_id _ |>.pow' n

Premises used: HasStrictFDerivAt.pow'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
n : ℕ
⊢ HasFDerivWithinAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (HPow.hPow (β := ℕ) f 0)
    (∑ i ∈ Finset.range 0, f x ^ (Nat.pred 0 - i) •> f' <• f x ^ i) s x

Tactic:
simpa using hasFDerivWithinAt_const 1 x s

Premises used: hasFDerivWithinAt_const, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
n : ℕ
⊢ HasFDerivWithinAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (HPow.hPow (β := ℕ) f 1)
    (∑ i ∈ Finset.range 1, f x ^ (Nat.pred 1 - i) •> f' <• f x ^ i) s x

Tactic:
simpa using h
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
n_1 n : ℕ
⊢ HasFDerivWithinAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) s x

Tactic:
have := h.mul' (h.pow' (n + 1))
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
n_1 n : ℕ
this :
  HasFDerivWithinAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) s x
simp_rw :
  HasFDerivWithinAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f * f ^ (n + 1))
    (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) s x
⊢ HasFDerivWithinAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f ^ (n + 1 + 1))
    (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) s x

Tactic:
simp_rw [pow_succ' _ (n + 1)]

Premises used: HAdd.hAdd, OfNat.ofNat, pow_succ'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
n_1 n : ℕ
this :
  HasFDerivWithinAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) s x
⊢ HasFDerivWithinAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f * f ^ (n + 1))
    (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) s x

Tactic:
this.congr_fderiv <| aux _ _ _ _

Premises used: HasFDerivWithinAt.congr_fderiv, _private.0.aux
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
n_1 n : ℕ
this :
  HasFDerivWithinAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) s x
⊢ HasFDerivWithinAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f * f ^ (n + 1))
    (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) s x

Tactic:
exact this.congr_fderiv <| aux _ _ _ _

Premises used: HasFDerivWithinAt.congr_fderiv, _private.0.aux
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
n : ℕ
x : 𝔸
s : Set 𝔸
⊢ HasFDerivWithinAt.{u_1, u_2, u_2} (𝕜 := 𝕜) (F := 𝔸) (fun (x : 𝔸) ↦ x ^ n)
    (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i) s x

Tactic:
hasFDerivWithinAt_id _ _ |>.pow' n

Premises used: HasFDerivWithinAt.pow'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasFDerivAt f f' x
n : ℕ
⊢ HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (HPow.hPow (β := ℕ) f 0)
    (∑ i ∈ Finset.range 0, f x ^ (Nat.pred 0 - i) •> f' <• f x ^ i) x

Tactic:
simpa using hasFDerivAt_const 1 x

Premises used: hasFDerivAt_const, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasFDerivAt f f' x
n : ℕ
⊢ HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (HPow.hPow (β := ℕ) f 1)
    (∑ i ∈ Finset.range 1, f x ^ (Nat.pred 1 - i) •> f' <• f x ^ i) x

Tactic:
simpa using h
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasFDerivAt f f' x
n_1 n : ℕ
⊢ HasFDerivAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) x

Tactic:
have := h.mul' (h.pow' (n + 1))
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasFDerivAt f f' x
n_1 n : ℕ
this :
  HasFDerivAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) x
simp_rw :
  HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f * f ^ (n + 1))
    (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x
⊢ HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f ^ (n + 1 + 1))
    (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x

Tactic:
simp_rw [pow_succ' _ (n + 1)]

Premises used: HAdd.hAdd, OfNat.ofNat, pow_succ'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasFDerivAt f f' x
n_1 n : ℕ
this :
  HasFDerivAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) x
⊢ HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f * f ^ (n + 1))
    (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x

Tactic:
this.congr_fderiv <| aux _ _ _ _

Premises used: HasFDerivAt.congr_fderiv, _private.0.aux
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
f' : E →L[𝕜] 𝔸
x : E
h : HasFDerivAt f f' x
n_1 n : ℕ
this :
  HasFDerivAt (f * f ^ (n + 1))
    (f x •> ∑ i ∈ Finset.range (n + 1), f x ^ ((n + 1).pred - i) •> f' <• f x ^ i + f' <• (f ^ (n + 1)) x) x
⊢ HasFDerivAt.{u_1, u_3, u_2} (𝕜 := 𝕜) (f * f ^ (n + 1))
    (∑ i ∈ Finset.range (n + 1 + 1), f x ^ ((n + 1 + 1).pred - i) •> f' <• f x ^ i) x

Tactic:
exact this.congr_fderiv <| aux _ _ _ _

Premises used: HasFDerivAt.congr_fderiv, _private.0.aux
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
n : ℕ
x : 𝔸
⊢ HasFDerivAt.{u_1, u_2, u_2} (𝕜 := 𝕜) (F := 𝔸) (fun (x : 𝔸) ↦ x ^ n)
    (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i) x

Tactic:
hasFDerivAt_id _ |>.pow' n

Premises used: HasFDerivAt.pow'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
x : E
s : Set E
hf : DifferentiableWithinAt 𝕜 f s x
n : ℕ
⊢ DifferentiableWithinAt.{u_1, u_3, u_2} 𝕜 (F := 𝔸) (fun (x : E) ↦ f x ^ n) s x

Tactic:
let ⟨_, hf'⟩ := hf; ⟨_, hf'.pow' n⟩

Premises used: _private.0.DifferentiableWithinAt.fun_pow.match_1, HSub.hSub, Finset.range, HPow.hPow, HasFDerivWithinAt.pow', Exists.intro, DifferentiableWithinAt, HSMul.hSMul, Nat.pred, Finset.sum, MulOpposite.op
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
x : E
s : Set E
hf : DifferentiableWithinAt 𝕜 f s x
⊢ ∀ (n : ℕ), DifferentiableWithinAt 𝕜 (f ^ n) s x

Tactic:
hf.fun_pow

Premises used: DifferentiableWithinAt.fun_pow
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
n : ℕ
x : 𝔸
s : Set 𝔸
⊢ DifferentiableWithinAt 𝕜 (F := 𝔸) (fun (x : 𝔸) ↦ x ^ n) s x

Tactic:
differentiableWithinAt_id.pow _

Premises used: DifferentiableWithinAt.pow
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
x : E
hf : DifferentiableAt 𝕜 f x
n : ℕ
⊢ DifferentiableAt 𝕜 (f ^ n) x

Tactic:
differentiableWithinAt_univ.mp <| hf.differentiableWithinAt.pow n

Premises used: DifferentiableAt.differentiableWithinAt, DifferentiableWithinAt.pow, Iff.mp, differentiableWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
n : ℕ
x : 𝔸
⊢ DifferentiableAt 𝕜 (F := 𝔸) (fun (x : 𝔸) ↦ x ^ n) x

Tactic:
differentiableAt_id.pow _

Premises used: DifferentiableAt.pow
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
s : Set E
hf : DifferentiableOn 𝕜 f s
n : ℕ
⊢ DifferentiableOn 𝕜 (f ^ n) s

Tactic:
fun x h => (hf x h).pow n

Premises used: DifferentiableWithinAt.pow, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
n : ℕ
s : Set 𝔸
⊢ DifferentiableOn 𝕜 (F := 𝔸) (fun (x : 𝔸) ↦ x ^ n) s

Tactic:
differentiableOn_id.pow n

Premises used: DifferentiableOn.pow
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
hf : Differentiable 𝕜 f
n : ℕ
⊢ Differentiable 𝕜 (f ^ n)

Tactic:
fun x => (hf x).pow n

Premises used: Differentiable, DifferentiableAt.pow
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
n : ℕ
⊢ Differentiable 𝕜 (F := 𝔸) fun (x : 𝔸) ↦ x ^ n

Tactic:
differentiable_id.pow _

Premises used: Differentiable.pow
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
x : E
n : ℕ
hf : DifferentiableAt 𝕜 f x
⊢ Eq (α := E →L[𝕜] 𝔸) (fderiv 𝕜 (f ^ n) x) (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> fderiv 𝕜 f x <• f x ^ i)

Tactic:
hf.hasFDerivAt.pow' n |>.fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, HasFDerivAt.pow'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
x : 𝔸
n : ℕ
rw :
  Eq.{u_2 + 1} (α := 𝔸 →L[𝕜] 𝔸) (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> fderiv 𝕜 (fun (x : 𝔸) ↦ x) x <• x ^ i)
    (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := 𝔸 →L[𝕜] 𝔸) (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i)
    (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i)
⊢ Eq (α := 𝔸 →L[𝕜] 𝔸) (fderiv 𝕜 (fun (x : 𝔸) ↦ x ^ n) x)
    (∑ i ∈ Finset.range n, x ^ (n.pred - i) •> ContinuousLinearMap.id 𝕜 𝔸 <• x ^ i)

Tactic:
rw [fderiv_fun_pow' n differentiableAt_fun_id, fderiv_fun_id]

Premises used: fderiv_fun_id, fderiv_fun_pow'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Pow
Goal:
𝕜 : Type u_1
𝔸 : Type u_2
E : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedRing 𝔸
inst_2 : NormedAddCommGroup E
inst_3 : NormedAlgebra 𝕜 𝔸
inst_4 : NormedSpace 𝕜 E
f : E → 𝔸
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
n : ℕ
hf : DifferentiableWithinAt 𝕜 f s x
⊢ Eq (α := E →L[𝕜] 𝔸) (fderivWithin 𝕜 (f ^ n) s x)
    (∑ i ∈ Finset.range n, f x ^ (n.pred - i) •> fderivWithin 𝕜 f s x <• f x ^ i)

Tactic:
hf.hasFDerivWithinAt.pow' n |>.fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, HasFDerivWithinAt.pow', DifferentiableWithinAt.hasFDerivWithinAt