Theorem: iteratedDeriv_pow (ForML/Util.lean)

State before:
case zero
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n : ℕ
⊢ (iteratedDeriv Nat.zero fun x => x ^ n) = fun x => ↑(Nat.descFactorial n Nat.zero) * x ^ (n - Nat.zero)
Tactic:
simp
State after:
no goals

State before:
case succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
⊢ (iteratedDeriv (Nat.succ i) fun x => x ^ n) = fun x => ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)
Tactic:
rw [iteratedDeriv_succ, IH]
State after:
case succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
⊢ (deriv fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)) = fun x =>
    ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)

State before:
case succ
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
⊢ (deriv fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)) = fun x =>
    ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)
Tactic:
funext x
State after:
case succ.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ deriv (fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)) x = ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)

State before:
case succ.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ deriv (fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)) x = ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)
Tactic:
rw [deriv_const_mul _ (differentiableAt_pow (n - i)), deriv_pow]
State after:
case succ.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ ↑(Nat.descFactorial n i) * (↑(n - i) * x ^ (n - i - 1)) = ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)

State before:
case succ.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ ↑(Nat.descFactorial n i) * (↑(n - i) * x ^ (n - i - 1)) = ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)
Tactic:
rw [← mul_assoc]
State after:
case succ.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ ↑(Nat.descFactorial n i) * ↑(n - i) * x ^ (n - i - 1) = ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)

State before:
case succ.h
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ ↑(Nat.descFactorial n i) * ↑(n - i) * x ^ (n - i - 1) = ↑(Nat.descFactorial n (Nat.succ i)) * x ^ (n - Nat.succ i)
Tactic:
refine congrArg₂ _ ?_ ?_
State after:
case succ.h.refine_1
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ ↑(Nat.descFactorial n i) * ↑(n - i) = ↑(Nat.descFactorial n (Nat.succ i))

case succ.h.refine_2
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ x ^ (n - i - 1) = x ^ (n - Nat.succ i)

State before:
case succ.h.refine_1
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ ↑(Nat.descFactorial n i) * ↑(n - i) = ↑(Nat.descFactorial n (Nat.succ i))
Tactic:
simp [mul_comm (↑(n - i) : 𝕜)]
State after:
no goals

State before:
case succ.h.refine_2
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
n i : ℕ
IH : (iteratedDeriv i fun x => x ^ n) = fun x => ↑(Nat.descFactorial n i) * x ^ (n - i)
x : 𝕜
⊢ x ^ (n - i - 1) = x ^ (n - Nat.succ i)
Tactic:
simp [Nat.sub_succ']
State after:
no goals