Theorem: RuesDiffMod (NazgandLean4/RootOfUnityExponentialSum.lean)

State before:
n : ℕ+
m : ℤ
⊢ RuesDiff n m = RuesDiff n (m % ↑↑n)
Tactic:
rw [RuesDiffMPeriodic n (m % n) (m / n)]
State after:
n : ℕ+
m : ℤ
⊢ RuesDiff n m = RuesDiff n (m % ↑↑n + m / ↑↑n * ↑↑n)

State before:
n : ℕ+
m : ℤ
⊢ RuesDiff n m = RuesDiff n (m % ↑↑n + m / ↑↑n * ↑↑n)
Tactic:
nth_rw 1 [←Int.ediv_add_emod' m n]
State after:
n : ℕ+
m : ℤ
⊢ RuesDiff n (m / ↑↑n * ↑↑n + m % ↑↑n) = RuesDiff n (m % ↑↑n + m / ↑↑n * ↑↑n)

State before:
n : ℕ+
m : ℤ
⊢ RuesDiff n (m / ↑↑n * ↑↑n + m % ↑↑n) = RuesDiff n (m % ↑↑n + m / ↑↑n * ↑↑n)
Tactic:
suffices h₀ : m / ↑↑n * ↑↑n + m % ↑↑n = m % ↑↑n + m / ↑↑n * ↑↑n
State after:
n : ℕ+
m : ℤ
h₀ : m / ↑↑n * ↑↑n + m % ↑↑n = m % ↑↑n + m / ↑↑n * ↑↑n
⊢ RuesDiff n (m / ↑↑n * ↑↑n + m % ↑↑n) = RuesDiff n (m % ↑↑n + m / ↑↑n * ↑↑n)

case h₀
n : ℕ+
m : ℤ
⊢ m / ↑↑n * ↑↑n + m % ↑↑n = m % ↑↑n + m / ↑↑n * ↑↑n

State before:
n : ℕ+
m : ℤ
h₀ : m / ↑↑n * ↑↑n + m % ↑↑n = m % ↑↑n + m / ↑↑n * ↑↑n
⊢ RuesDiff n (m / ↑↑n * ↑↑n + m % ↑↑n) = RuesDiff n (m % ↑↑n + m / ↑↑n * ↑↑n)

case h₀
n : ℕ+
m : ℤ
⊢ m / ↑↑n * ↑↑n + m % ↑↑n = m % ↑↑n + m / ↑↑n * ↑↑n
Tactic:
exact congrArg (RuesDiff n) h₀
State after:
case h₀
n : ℕ+
m : ℤ
⊢ m / ↑↑n * ↑↑n + m % ↑↑n = m % ↑↑n + m / ↑↑n * ↑↑n

State before:
case h₀
n : ℕ+
m : ℤ
⊢ m / ↑↑n * ↑↑n + m % ↑↑n = m % ↑↑n + m / ↑↑n * ↑↑n
Tactic:
ring_nf
State after:
no goals