internlm/Lean-Github huggingface dataset:
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof 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]
Proof 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
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof 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']
Proof 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
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof 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]
Proof 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
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof 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]
Proof 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
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof 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]
Proof 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
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof 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]
Proof 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
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof 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]
Proof 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)
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof 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₂ _ ?_ ?_
Proof 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
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof 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 ?_
Proof 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
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof 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 _
Proof 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
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof 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]
Proof 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
Theorem: SchwartzMap.Real.iteratedDeriv_pow_smul
Proof 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]
Proof state after:
no goals