n : ℕ
hn : n % 2 = 1
⊢ (if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1) = (-1) ^ (n / 2)
n : ℕ
hn : n % 2 = 1
⊢ ↑χ₄ ↑n = (-1) ^ (n / 2)
rw [χ₄_nat_eq_if_mod_four]
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n / 2)
n : ℕ
hn : n % 2 = 1
⊢ (if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1) = (-1) ^ (n / 2)
simp only [hn, Nat.one_ne_zero, if_false]
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ ((4 * (n / 4) + n % 4) / 2)
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n / 2)
nth_rw 3 [← Nat.div_add_mod n 4]
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ ((2 * 2 * (n / 4) + n % 4) / 2)
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ ((4 * (n / 4) + n % 4) / 2)
nth_rw 3 [(by norm_num : 4 = 2 * 2)]
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2)
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ ((2 * 2 * (n / 4) + n % 4) / 2)
rw [mul_assoc, add_comm, Nat.add_mul_div_left _ _ (by norm_num : 0 < 2), pow_add, pow_mul,
  neg_one_sq, one_pow, mul_one]
n : ℕ
hn : n % 2 = 1
help : ∀ (m : ℕ), m < 4 → m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2)
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2)
have help : ∀ m : ℕ, m < 4 → m % 2 = 1 → ite (m = 1) (1 : ℤ) (-1) = (-1) ^ (m / 2) := by decide
no goals
n : ℕ
hn : n % 2 = 1
help : ∀ (m : ℕ), m < 4 → m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2)
exact
  help (n % 4) (Nat.mod_lt n (by norm_num))
    ((Nat.mod_mod_of_dvd n (by norm_num : 2 ∣ 4)).trans hn)
no goals
n : ℕ
hn : n % 2 = 1
⊢ 4 = 2 * 2
norm_num
no goals
n : ℕ
hn : n % 2 = 1
⊢ 0 < 2
norm_num
no goals
n : ℕ
hn : n % 2 = 1
⊢ ∀ (m : ℕ), m < 4 → m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)
decide
no goals
n : ℕ
hn : n % 2 = 1
help : ∀ (m : ℕ), m < 4 → m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)
⊢ 4 > 0
norm_num
no goals
n : ℕ
hn : n % 2 = 1
help : ∀ (m : ℕ), m < 4 → m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)
⊢ 2 ∣ 4
norm_num