Theorem: RuesDiffIteratedDeriv (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
k : ℕ
n : ℕ+
m : ℤ
⊢ iteratedDeriv k (RuesDiff n m) = RuesDiff n (↑k + m)
Tactic:
induction' k with K Kih
State after:
case zero
n : ℕ+
m : ℤ
⊢ iteratedDeriv 0 (RuesDiff n m) = RuesDiff n (↑0 + m)

case succ
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
⊢ iteratedDeriv (K + 1) (RuesDiff n m) = RuesDiff n (↑(K + 1) + m)

State before:
case zero
n : ℕ+
m : ℤ
⊢ iteratedDeriv 0 (RuesDiff n m) = RuesDiff n (↑0 + m)
Tactic:
simp only [Nat.zero_eq, iteratedDeriv_zero, CharP.cast_eq_zero, zero_add]
State after:
no goals

State before:
case succ
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
⊢ iteratedDeriv (K + 1) (RuesDiff n m) = RuesDiff n (↑(K + 1) + m)
Tactic:
have h₀ := congrArg deriv Kih
State after:
case succ
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
h₀ : deriv (iteratedDeriv K (RuesDiff n m)) = deriv (RuesDiff n (↑K + m))
⊢ iteratedDeriv (K + 1) (RuesDiff n m) = RuesDiff n (↑(K + 1) + m)

State before:
case succ
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
h₀ : deriv (iteratedDeriv K (RuesDiff n m)) = deriv (RuesDiff n (↑K + m))
⊢ iteratedDeriv (K + 1) (RuesDiff n m) = RuesDiff n (↑(K + 1) + m)
Tactic:
rw [iteratedDeriv_succ, h₀, RuesDiffDeriv]
State after:
case succ
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
h₀ : deriv (iteratedDeriv K (RuesDiff n m)) = deriv (RuesDiff n (↑K + m))
⊢ RuesDiff n (↑K + m + 1) = RuesDiff n (↑(K + 1) + m)

State before:
case succ
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
h₀ : deriv (iteratedDeriv K (RuesDiff n m)) = deriv (RuesDiff n (↑K + m))
⊢ RuesDiff n (↑K + m + 1) = RuesDiff n (↑(K + 1) + m)
Tactic:
have h₁ : ↑K + m + 1 = ↑(Nat.succ K) + m := by
  simp only [Nat.cast_succ]
  ring
State after:
case succ
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
h₀ : deriv (iteratedDeriv K (RuesDiff n m)) = deriv (RuesDiff n (↑K + m))
h₁ : ↑K + m + 1 = ↑K.succ + m
⊢ RuesDiff n (↑K + m + 1) = RuesDiff n (↑(K + 1) + m)

State before:
case succ
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
h₀ : deriv (iteratedDeriv K (RuesDiff n m)) = deriv (RuesDiff n (↑K + m))
h₁ : ↑K + m + 1 = ↑K.succ + m
⊢ RuesDiff n (↑K + m + 1) = RuesDiff n (↑(K + 1) + m)
Tactic:
rw [h₁]
State after:
no goals

State before:
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
h₀ : deriv (iteratedDeriv K (RuesDiff n m)) = deriv (RuesDiff n (↑K + m))
⊢ ↑K + m + 1 = ↑K.succ + m
Tactic:
simp only [Nat.cast_succ]
State after:
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
h₀ : deriv (iteratedDeriv K (RuesDiff n m)) = deriv (RuesDiff n (↑K + m))
⊢ ↑K + m + 1 = ↑K + 1 + m

State before:
n : ℕ+
m : ℤ
K : ℕ
Kih : iteratedDeriv K (RuesDiff n m) = RuesDiff n (↑K + m)
h₀ : deriv (iteratedDeriv K (RuesDiff n m)) = deriv (RuesDiff n (↑K + m))
⊢ ↑K + m + 1 = ↑K + 1 + m
Tactic:
ring
State after:
no goals