Theorem: RuesDiffNthIteratedDeriv (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
n : ℕ+
m : ℤ
⊢ iteratedDeriv (↑n) (RuesDiff n m) = RuesDiff n m
Tactic:
rw [RuesDiffIteratedDeriv, RuesDiffMPeriodic n m 1]
State after:
n : ℕ+
m : ℤ
⊢ RuesDiff n (↑↑n + m) = RuesDiff n (m + 1 * ↑↑n)

State before:
n : ℕ+
m : ℤ
⊢ RuesDiff n (↑↑n + m) = RuesDiff n (m + 1 * ↑↑n)
Tactic:
simp only [one_mul]
State after:
n : ℕ+
m : ℤ
⊢ RuesDiff n (↑↑n + m) = RuesDiff n (m + ↑↑n)

State before:
n : ℕ+
m : ℤ
⊢ RuesDiff n (↑↑n + m) = RuesDiff n (m + ↑↑n)
Tactic:
ring_nf
State after:
no goals