Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul (ForML/SchwartzRealFourier.lean)

State before:
case zero
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
⊢ (iteratedDeriv Nat.zero fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ Nat.zero),
      Nat.choose Nat.zero i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (Nat.zero - i) (⇑f) x
Tactic:
simp
State after:
no goals

State before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
⊢ (iteratedDeriv (Nat.succ n) fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ (Nat.succ n)),
      Nat.choose (Nat.succ n) i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (Nat.succ n - i) (⇑f) x
Tactic:
rw [iteratedDeriv_succ, IH]
State after:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
⊢ (deriv fun x =>
      ∑ i in Finset.range (Nat.succ n),
        Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x) =
    fun x =>
    ∑ i in Finset.range (Nat.succ (Nat.succ n)),
      Nat.choose (Nat.succ n) i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (Nat.succ n - i) (⇑f) x

State before:
case succ
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
⊢ (deriv fun x =>
      ∑ i in Finset.range (Nat.succ n),
        Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x) =
    fun x =>
    ∑ i in Finset.range (Nat.succ (Nat.succ n)),
      Nat.choose (Nat.succ n) i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (Nat.succ n - i) (⇑f) x
Tactic:
funext x
State after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
⊢ deriv
      (fun x =>
        ∑ i in Finset.range (Nat.succ n),
          Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x)
      x =
    ∑ i in Finset.range (Nat.succ (Nat.succ n)),
      Nat.choose (Nat.succ n) i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (Nat.succ n - i) (⇑f) x

State before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
⊢ deriv
      (fun x =>
        ∑ i in Finset.range (Nat.succ n),
          Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x)
      x =
    ∑ i in Finset.range (Nat.succ (Nat.succ n)),
      Nat.choose (Nat.succ n) i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (Nat.succ n - i) (⇑f) x
Tactic:
simp only [smul_smul]
State after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
⊢ deriv
      (fun x =>
        ∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1) (⇑f) x)
      x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x

State before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
⊢ deriv
      (fun x =>
        ∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1) (⇑f) x)
      x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x
Tactic:
have hf (i) := (f.smooth ⊤).differentiable_iteratedDeriv i (WithTop.coe_lt_top _)
State after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ deriv
      (fun x =>
        ∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1) (⇑f) x)
      x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x

State before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ deriv
      (fun x =>
        ∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1) (⇑f) x)
      x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x
Tactic:
rw [deriv_sum fun i _ ↦ ((differentiable_pow _).smul (hf _)).const_smul _ _]
State after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ i in Finset.range (Nat.succ n),
      deriv (fun y => (Nat.choose n i * Nat.descFactorial k i) • y ^ (k - i) • iteratedDeriv (n - i) (⇑f) y) x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x

State before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ i in Finset.range (Nat.succ n),
      deriv (fun y => (Nat.choose n i * Nat.descFactorial k i) • y ^ (k - i) • iteratedDeriv (n - i) (⇑f) y) x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x
Tactic:
simp only [deriv_const_smul _ ((differentiable_pow _).smul (hf _) _)]
State after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
      (Nat.choose n x_1 * Nat.descFactorial k x_1) • deriv (fun y => y ^ (k - x_1) • iteratedDeriv (n - x_1) (⇑f) y) x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x

State before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
      (Nat.choose n x_1 * Nat.descFactorial k x_1) • deriv (fun y => y ^ (k - x_1) • iteratedDeriv (n - x_1) (⇑f) y) x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x
Tactic:
simp only [deriv_smul (differentiable_pow _ _) (hf _ _)]
State after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
      (Nat.choose n x_1 * Nat.descFactorial k x_1) •
        (x ^ (k - x_1) • deriv (iteratedDeriv (n - x_1) ⇑f) x +
          deriv (fun x => x ^ (k - x_1)) x • iteratedDeriv (n - x_1) (⇑f) x) =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x

State before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
      (Nat.choose n x_1 * Nat.descFactorial k x_1) •
        (x ^ (k - x_1) • deriv (iteratedDeriv (n - x_1) ⇑f) x +
          deriv (fun x => x ^ (k - x_1)) x • iteratedDeriv (n - x_1) (⇑f) x) =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x
Tactic:
simp only [smul_add, Finset.sum_add_distrib]
State after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • deriv (iteratedDeriv (n - x_1) ⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          deriv (fun x => x ^ (k - x_1)) x • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x

State before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • deriv (iteratedDeriv (n - x_1) ⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          deriv (fun x => x ^ (k - x_1)) x • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x
Tactic:
simp only [← iteratedDeriv_succ, deriv_pow]
State after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          (↑(k - x_1) * x ^ (k - x_1 - 1)) • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x

State before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          (↑(k - x_1) * x ^ (k - x_1 - 1)) • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x
Tactic:
simp only [← Nat.sub_succ']
State after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          (↑(k - x_1) * x ^ (k - Nat.succ x_1)) • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x

State before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          (↑(k - x_1) * x ^ (k - Nat.succ x_1)) • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ (Nat.succ n)),
      (Nat.choose (Nat.succ n) x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (Nat.succ n - x_1) (⇑f) x
Tactic:
rw [Finset.sum_range_succ' _ n.succ]
State after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          (↑(k - x_1) * x ^ (k - Nat.succ x_1)) • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ k_1 in Finset.range (Nat.succ n),
        (Nat.choose (Nat.succ n) (k_1 + 1) * Nat.descFactorial k (k_1 + 1)) •
          x ^ (k - (k_1 + 1)) • iteratedDeriv (Nat.succ n - (k_1 + 1)) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x

State before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          (↑(k - x_1) * x ^ (k - Nat.succ x_1)) • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ k_1 in Finset.range (Nat.succ n),
        (Nat.choose (Nat.succ n) (k_1 + 1) * Nat.descFactorial k (k_1 + 1)) •
          x ^ (k - (k_1 + 1)) • iteratedDeriv (Nat.succ n - (k_1 + 1)) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x
Tactic:
simp only [Nat.choose_succ_succ]
State after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          (↑(k - x_1) * x ^ (k - Nat.succ x_1)) • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ n),
        ((Nat.choose n x_1 + Nat.choose n (Nat.succ x_1)) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (Nat.succ n - (x_1 + 1)) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x

State before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          (↑(k - x_1) * x ^ (k - Nat.succ x_1)) • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ n),
        ((Nat.choose n x_1 + Nat.choose n (Nat.succ x_1)) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (Nat.succ n - (x_1 + 1)) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x
Tactic:
simp only [add_mul, add_smul, Finset.sum_add_distrib]
State after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          (↑(k - x_1) * x ^ (k - Nat.succ x_1)) • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n x_1 * Nat.descFactorial k (x_1 + 1)) •
            x ^ (k - (x_1 + 1)) • iteratedDeriv (Nat.succ n - (x_1 + 1)) (⇑f) x +
        ∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
            x ^ (k - (x_1 + 1)) • iteratedDeriv (Nat.succ n - (x_1 + 1)) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x

State before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          (↑(k - x_1) * x ^ (k - Nat.succ x_1)) • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n x_1 * Nat.descFactorial k (x_1 + 1)) •
            x ^ (k - (x_1 + 1)) • iteratedDeriv (Nat.succ n - (x_1 + 1)) (⇑f) x +
        ∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
            x ^ (k - (x_1 + 1)) • iteratedDeriv (Nat.succ n - (x_1 + 1)) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x
Tactic:
simp only [Nat.succ_sub_succ_eq_sub]
State after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          (↑(k - x_1) * x ^ (k - Nat.succ x_1)) • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n x_1 * Nat.descFactorial k (x_1 + 1)) • x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
        ∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
            x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x

State before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          (↑(k - x_1) * x ^ (k - Nat.succ x_1)) • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n x_1 * Nat.descFactorial k (x_1 + 1)) • x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
        ∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
            x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x
Tactic:
rw [add_comm, add_assoc]
State after:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          (↑(k - x_1) * x ^ (k - Nat.succ x_1)) • iteratedDeriv (n - x_1) (⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k (x_1 + 1)) • x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      (∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
            x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
        (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x)

State before:
case succ.h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) •
          (↑(k - x_1) * x ^ (k - Nat.succ x_1)) • iteratedDeriv (n - x_1) (⇑f) x +
      ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n x_1 * Nat.descFactorial k (x_1 + 1)) • x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      (∑ x_1 in Finset.range (Nat.succ n),
          (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
            x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
        (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x)
Tactic:
refine congrArg₂ _ ?_ ?_
State after:
case succ.h.refine_1
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
      (Nat.choose n x_1 * Nat.descFactorial k x_1) •
        (↑(k - x_1) * x ^ (k - Nat.succ x_1)) • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ n),
      (Nat.choose n x_1 * Nat.descFactorial k (x_1 + 1)) • x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x

case succ.h.refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
      (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x

State before:
case succ.h.refine_1
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
      (Nat.choose n x_1 * Nat.descFactorial k x_1) •
        (↑(k - x_1) * x ^ (k - Nat.succ x_1)) • iteratedDeriv (n - x_1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ n),
      (Nat.choose n x_1 * Nat.descFactorial k (x_1 + 1)) • x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x
Tactic:
refine Finset.sum_congr rfl ?_
State after:
case succ.h.refine_1
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∀ x_1 ∈ Finset.range (Nat.succ n),
    (Nat.choose n x_1 * Nat.descFactorial k x_1) •
        (↑(k - x_1) * x ^ (k - Nat.succ x_1)) • iteratedDeriv (n - x_1) (⇑f) x =
      (Nat.choose n x_1 * Nat.descFactorial k (x_1 + 1)) • x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x

State before:
case succ.h.refine_1
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∀ x_1 ∈ Finset.range (Nat.succ n),
    (Nat.choose n x_1 * Nat.descFactorial k x_1) •
        (↑(k - x_1) * x ^ (k - Nat.succ x_1)) • iteratedDeriv (n - x_1) (⇑f) x =
      (Nat.choose n x_1 * Nat.descFactorial k (x_1 + 1)) • x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x
Tactic:
intro i _
State after:
case succ.h.refine_1
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
i : ℕ
a✝ : i ∈ Finset.range (Nat.succ n)
⊢ (Nat.choose n i * Nat.descFactorial k i) • (↑(k - i) * x ^ (k - Nat.succ i)) • iteratedDeriv (n - i) (⇑f) x =
    (Nat.choose n i * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - i) (⇑f) x

State before:
case succ.h.refine_1
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
i : ℕ
a✝ : i ∈ Finset.range (Nat.succ n)
⊢ (Nat.choose n i * Nat.descFactorial k i) • (↑(k - i) * x ^ (k - Nat.succ i)) • iteratedDeriv (n - i) (⇑f) x =
    (Nat.choose n i * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - i) (⇑f) x
Tactic:
rw [← nsmul_eq_mul, smul_assoc, smul_smul]
State after:
case succ.h.refine_1
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
i : ℕ
a✝ : i ∈ Finset.range (Nat.succ n)
⊢ (Nat.choose n i * Nat.descFactorial k i * (k - i)) • x ^ (k - Nat.succ i) • iteratedDeriv (n - i) (⇑f) x =
    (Nat.choose n i * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - i) (⇑f) x

State before:
case succ.h.refine_1
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
i : ℕ
a✝ : i ∈ Finset.range (Nat.succ n)
⊢ (Nat.choose n i * Nat.descFactorial k i * (k - i)) • x ^ (k - Nat.succ i) • iteratedDeriv (n - i) (⇑f) x =
    (Nat.choose n i * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - i) (⇑f) x
Tactic:
rw [Nat.descFactorial_succ, mul_comm (k - i), mul_assoc]
State after:
no goals

State before:
case succ.h.refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
      (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x =
    ∑ x_1 in Finset.range (Nat.succ n),
        (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x
Tactic:
conv => rhs; rw [Finset.sum_range_succ]
State after:
case succ.h.refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
      (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
          (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
            x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
        (Nat.choose n (Nat.succ n) * Nat.descFactorial k (n + 1)) • x ^ (k - (n + 1)) • iteratedDeriv (n - n) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x

State before:
case succ.h.refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
      (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
          (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
            x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
        (Nat.choose n (Nat.succ n) * Nat.descFactorial k (n + 1)) • x ^ (k - (n + 1)) • iteratedDeriv (n - n) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x
Tactic:
simp only [Nat.choose_succ_self, zero_mul, zero_smul, add_zero]
State after:
case succ.h.refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
      (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
        (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x

State before:
case succ.h.refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ x_1 in Finset.range (Nat.succ n),
      (Nat.choose n x_1 * Nat.descFactorial k x_1) • x ^ (k - x_1) • iteratedDeriv (n - x_1 + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
        (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x
Tactic:
rw [Finset.sum_range_succ']
State after:
case succ.h.refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ k_1 in Finset.range n,
        (Nat.choose n (k_1 + 1) * Nat.descFactorial k (k_1 + 1)) •
          x ^ (k - (k_1 + 1)) • iteratedDeriv (n - (k_1 + 1) + 1) (⇑f) x +
      (Nat.choose n 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (n - 0 + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
        (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x

State before:
case succ.h.refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ k_1 in Finset.range n,
        (Nat.choose n (k_1 + 1) * Nat.descFactorial k (k_1 + 1)) •
          x ^ (k - (k_1 + 1)) • iteratedDeriv (n - (k_1 + 1) + 1) (⇑f) x +
      (Nat.choose n 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (n - 0 + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
        (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      (Nat.choose (Nat.succ n) 0 * Nat.descFactorial k 0) • x ^ (k - 0) • iteratedDeriv (Nat.succ n - 0) (⇑f) x
Tactic:
simp only [Nat.choose_zero_right, Nat.descFactorial_zero, mul_one, Nat.sub_zero, one_smul]
State after:
case succ.h.refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ k_1 in Finset.range n,
        (Nat.choose n (k_1 + 1) * Nat.descFactorial k (k_1 + 1)) •
          x ^ (k - (k_1 + 1)) • iteratedDeriv (n - (k_1 + 1) + 1) (⇑f) x +
      x ^ k • iteratedDeriv (n + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
        (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      x ^ k • iteratedDeriv (Nat.succ n) (⇑f) x

State before:
case succ.h.refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ k_1 in Finset.range n,
        (Nat.choose n (k_1 + 1) * Nat.descFactorial k (k_1 + 1)) •
          x ^ (k - (k_1 + 1)) • iteratedDeriv (n - (k_1 + 1) + 1) (⇑f) x +
      x ^ k • iteratedDeriv (n + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
        (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
          x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x +
      x ^ k • iteratedDeriv (Nat.succ n) (⇑f) x
Tactic:
rw [add_left_inj]
State after:
case succ.h.refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ k_1 in Finset.range n,
      (Nat.choose n (k_1 + 1) * Nat.descFactorial k (k_1 + 1)) •
        x ^ (k - (k_1 + 1)) • iteratedDeriv (n - (k_1 + 1) + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
      (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
        x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x

State before:
case succ.h.refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∑ k_1 in Finset.range n,
      (Nat.choose n (k_1 + 1) * Nat.descFactorial k (k_1 + 1)) •
        x ^ (k - (k_1 + 1)) • iteratedDeriv (n - (k_1 + 1) + 1) (⇑f) x =
    ∑ x_1 in Finset.range n,
      (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
        x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x
Tactic:
refine Finset.sum_congr rfl ?_
State after:
case succ.h.refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∀ x_1 ∈ Finset.range n,
    (Nat.choose n (x_1 + 1) * Nat.descFactorial k (x_1 + 1)) •
        x ^ (k - (x_1 + 1)) • iteratedDeriv (n - (x_1 + 1) + 1) (⇑f) x =
      (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
        x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x

State before:
case succ.h.refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
⊢ ∀ x_1 ∈ Finset.range n,
    (Nat.choose n (x_1 + 1) * Nat.descFactorial k (x_1 + 1)) •
        x ^ (k - (x_1 + 1)) • iteratedDeriv (n - (x_1 + 1) + 1) (⇑f) x =
      (Nat.choose n (Nat.succ x_1) * Nat.descFactorial k (x_1 + 1)) •
        x ^ (k - (x_1 + 1)) • iteratedDeriv (n - x_1) (⇑f) x
Tactic:
intro i hi
State after:
case succ.h.refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
i : ℕ
hi : i ∈ Finset.range n
⊢ (Nat.choose n (i + 1) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - (i + 1) + 1) (⇑f) x =
    (Nat.choose n (Nat.succ i) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - i) (⇑f) x

State before:
case succ.h.refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
i : ℕ
hi : i ∈ Finset.range n
⊢ (Nat.choose n (i + 1) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - (i + 1) + 1) (⇑f) x =
    (Nat.choose n (Nat.succ i) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - i) (⇑f) x
Tactic:
replace hi : i.succ ≤ n := by simpa [Finset.mem_range] using hi
State after:
case succ.h.refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
i : ℕ
hi : Nat.succ i ≤ n
⊢ (Nat.choose n (i + 1) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - (i + 1) + 1) (⇑f) x =
    (Nat.choose n (Nat.succ i) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - i) (⇑f) x

State before:
case succ.h.refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
i : ℕ
hi : Nat.succ i ≤ n
⊢ (Nat.choose n (i + 1) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - (i + 1) + 1) (⇑f) x =
    (Nat.choose n (Nat.succ i) * Nat.descFactorial k (i + 1)) • x ^ (k - (i + 1)) • iteratedDeriv (n - i) (⇑f) x
Tactic:
simp [Nat.add_one, ← Nat.succ_sub hi]
State after:
no goals

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k : ℕ
f : 𝓢(ℝ, F)
n : ℕ
IH :
  (iteratedDeriv n fun y => y ^ k • f y) = fun x =>
    ∑ i in Finset.range (Nat.succ n),
      Nat.choose n i • Nat.descFactorial k i • x ^ (k - i) • iteratedDeriv (n - i) (⇑f) x
x : ℝ
hf : ∀ (i : ℕ), Differentiable ℝ (iteratedDeriv i ⇑f)
i : ℕ
hi : i ∈ Finset.range n
⊢ Nat.succ i ≤ n
Tactic:
simpa [Finset.mem_range] using hi
State after:
no goals