n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → ↑χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ ↑χ₈ ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1
n : ℤ
⊢ ↑χ₈ ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1
have help :
  ∀ m : ℤ, 0 ≤ m → m < 8 → χ₈ m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1 := by
  decide
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → ↑χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ ↑χ₈ ↑(n % ↑8) = if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → ↑χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ ↑χ₈ ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1
rw [← Int.emod_emod_of_dvd n (by norm_num : (2 : ℤ) ∣ 8), ← ZMod.int_cast_mod n 8]
no goals
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → ↑χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ ↑χ₈ ↑(n % ↑8) = if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1
exact help (n % 8) (Int.emod_nonneg n (by norm_num)) (Int.emod_lt n (by norm_num))
no goals
n : ℤ
⊢ ∀ (m : ℤ), 0 ≤ m → m < 8 → ↑χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
decide
no goals
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → ↑χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ 2 ∣ 8
norm_num
no goals
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → ↑χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ 8 ≠ 0
norm_num
no goals
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → ↑χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
⊢ 8 ≠ 0
norm_num