[GOAL]
⊢ ∀ (x y : ZMod 4),
    OneHom.toFun
        { toFun := ![0, 1, 0, -1], map_one' := (_ : Matrix.vecCons 0 ![1, 0, -1] 1 = Matrix.vecCons 0 ![1, 0, -1] 1) }
        (x * y) =
      OneHom.toFun
          { toFun := ![0, 1, 0, -1], map_one' := (_ : Matrix.vecCons 0 ![1, 0, -1] 1 = Matrix.vecCons 0 ![1, 0, -1] 1) }
          x *
        OneHom.toFun
          { toFun := ![0, 1, 0, -1], map_one' := (_ : Matrix.vecCons 0 ![1, 0, -1] 1 = Matrix.vecCons 0 ![1, 0, -1] 1) }
          y
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a : ZMod 4),
    ¬IsUnit a →
      OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := ![0, 1, 0, -1],
                  map_one' := (_ : Matrix.vecCons 0 ![1, 0, -1] 1 = Matrix.vecCons 0 ![1, 0, -1] 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : ZMod 4),
                    OneHom.toFun
                        { toFun := ![0, 1, 0, -1],
                          map_one' := (_ : Matrix.vecCons 0 ![1, 0, -1] 1 = Matrix.vecCons 0 ![1, 0, -1] 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := ![0, 1, 0, -1],
                            map_one' := (_ : Matrix.vecCons 0 ![1, 0, -1] 1 = Matrix.vecCons 0 ![1, 0, -1] 1) }
                          x *
                        OneHom.toFun
                          { toFun := ![0, 1, 0, -1],
                            map_one' := (_ : Matrix.vecCons 0 ![1, 0, -1] 1 = Matrix.vecCons 0 ![1, 0, -1] 1) }
                          y) })
          a =
        0
[PROOFSTEP]
decide
[GOAL]
⊢ MulChar.IsQuadratic χ₄
[PROOFSTEP]
intro a
[GOAL]
a : ZMod 4
⊢ ↑χ₄ a = 0 ∨ ↑χ₄ a = 1 ∨ ↑χ₄ a = -1
[PROOFSTEP]
fin_cases a
[GOAL]
case head
⊢ ↑χ₄ { val := 0, isLt := (_ : 0 < 3 + 1) } = 0 ∨
    ↑χ₄ { val := 0, isLt := (_ : 0 < 3 + 1) } = 1 ∨ ↑χ₄ { val := 0, isLt := (_ : 0 < 3 + 1) } = -1
case tail.head
⊢ ↑χ₄ { val := 1, isLt := (_ : (fun a => a < 3 + 1) 1) } = 0 ∨
    ↑χ₄ { val := 1, isLt := (_ : (fun a => a < 3 + 1) 1) } = 1 ∨
      ↑χ₄ { val := 1, isLt := (_ : (fun a => a < 3 + 1) 1) } = -1
case tail.tail.head
⊢ ↑χ₄ { val := 2, isLt := (_ : (fun a => (fun a => a < 3 + 1) a) 2) } = 0 ∨
    ↑χ₄ { val := 2, isLt := (_ : (fun a => (fun a => a < 3 + 1) a) 2) } = 1 ∨
      ↑χ₄ { val := 2, isLt := (_ : (fun a => (fun a => a < 3 + 1) a) 2) } = -1
case tail.tail.tail.head
⊢ ↑χ₄ { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 3 + 1) a) a) 3) } = 0 ∨
    ↑χ₄ { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 3 + 1) a) a) 3) } = 1 ∨
      ↑χ₄ { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 3 + 1) a) a) 3) } = -1
[PROOFSTEP]
all_goals decide
[GOAL]
case head
⊢ ↑χ₄ { val := 0, isLt := (_ : 0 < 3 + 1) } = 0 ∨
    ↑χ₄ { val := 0, isLt := (_ : 0 < 3 + 1) } = 1 ∨ ↑χ₄ { val := 0, isLt := (_ : 0 < 3 + 1) } = -1
[PROOFSTEP]
decide
[GOAL]
case tail.head
⊢ ↑χ₄ { val := 1, isLt := (_ : (fun a => a < 3 + 1) 1) } = 0 ∨
    ↑χ₄ { val := 1, isLt := (_ : (fun a => a < 3 + 1) 1) } = 1 ∨
      ↑χ₄ { val := 1, isLt := (_ : (fun a => a < 3 + 1) 1) } = -1
[PROOFSTEP]
decide
[GOAL]
case tail.tail.head
⊢ ↑χ₄ { val := 2, isLt := (_ : (fun a => (fun a => a < 3 + 1) a) 2) } = 0 ∨
    ↑χ₄ { val := 2, isLt := (_ : (fun a => (fun a => a < 3 + 1) a) 2) } = 1 ∨
      ↑χ₄ { val := 2, isLt := (_ : (fun a => (fun a => a < 3 + 1) a) 2) } = -1
[PROOFSTEP]
decide
[GOAL]
case tail.tail.tail.head
⊢ ↑χ₄ { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 3 + 1) a) a) 3) } = 0 ∨
    ↑χ₄ { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 3 + 1) a) a) 3) } = 1 ∨
      ↑χ₄ { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 3 + 1) a) a) 3) } = -1
[PROOFSTEP]
decide
[GOAL]
n : ℕ
⊢ ↑χ₄ ↑n = ↑χ₄ ↑(n % 4)
[PROOFSTEP]
rw [← ZMod.nat_cast_mod n 4]
[GOAL]
n : ℤ
⊢ ↑χ₄ ↑n = ↑χ₄ ↑(n % 4)
[PROOFSTEP]
rw [← ZMod.int_cast_mod n 4]
[GOAL]
n : ℤ
⊢ ↑χ₄ ↑(n % ↑4) = ↑χ₄ ↑(n % 4)
[PROOFSTEP]
norm_cast
[GOAL]
n : ℤ
⊢ ↑χ₄ ↑n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1
[PROOFSTEP]
have help : ∀ m : ℤ, 0 ≤ m → m < 4 → χ₄ m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1 := by decide
[GOAL]
n : ℤ
⊢ ∀ (m : ℤ), 0 ≤ m → m < 4 → ↑χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1
[PROOFSTEP]
decide
[GOAL]
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 4 → ↑χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1
⊢ ↑χ₄ ↑n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1
[PROOFSTEP]
rw [← Int.emod_emod_of_dvd n (by norm_num : (2 : ℤ) ∣ 4), ← ZMod.int_cast_mod n 4]
[GOAL]
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 4 → ↑χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1
⊢ 2 ∣ 4
[PROOFSTEP]
norm_num
[GOAL]
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 4 → ↑χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1
⊢ ↑χ₄ ↑(n % ↑4) = if n % 4 % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1
[PROOFSTEP]
exact help (n % 4) (Int.emod_nonneg n (by norm_num)) (Int.emod_lt n (by norm_num))
[GOAL]
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 4 → ↑χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1
⊢ 4 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 4 → ↑χ₄ ↑m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1
⊢ 4 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
⊢ ↑χ₄ ↑n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1
[PROOFSTEP]
exact_mod_cast χ₄_int_eq_if_mod_four n
[GOAL]
n : ℕ
hn : n % 2 = 1
⊢ ↑χ₄ ↑n = (-1) ^ (n / 2)
[PROOFSTEP]
rw [χ₄_nat_eq_if_mod_four]
[GOAL]
n : ℕ
hn : n % 2 = 1
⊢ (if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1) = (-1) ^ (n / 2)
[PROOFSTEP]
simp only [hn, Nat.one_ne_zero, if_false]
[GOAL]
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n / 2)
[PROOFSTEP]
conv_rhs =>
  -- Porting note: was `nth_rw`
  arg 2; rw [← Nat.div_add_mod n 4]
  enter [1, 1, 1]; rw [(by norm_num : 4 = 2 * 2)]
[GOAL]
n : ℕ
hn : n % 2 = 1
| (-1) ^ (n / 2)
[PROOFSTEP]
  arg 2; rw [← Nat.div_add_mod n 4]
  enter [1, 1, 1]; rw [(by norm_num : 4 = 2 * 2)]
[GOAL]
n : ℕ
hn : n % 2 = 1
| (-1) ^ (n / 2)
[PROOFSTEP]
  arg 2; rw [← Nat.div_add_mod n 4]
  enter [1, 1, 1]; rw [(by norm_num : 4 = 2 * 2)]
[GOAL]
n : ℕ
hn : n % 2 = 1
| (-1) ^ (n / 2)
[PROOFSTEP]
arg 2
[GOAL]
n : ℕ
hn : n % 2 = 1
| n / 2
[PROOFSTEP]
rw [← Nat.div_add_mod n 4]
[GOAL]
n : ℕ
hn : n % 2 = 1
| (4 * (n / 4) + n % 4) / 2
[PROOFSTEP]
enter [1, 1, 1]
[GOAL]
n : ℕ
hn : n % 2 = 1
| 4
[PROOFSTEP]
rw [(by norm_num : 4 = 2 * 2)]
[GOAL]
n : ℕ
hn : n % 2 = 1
⊢ 4 = 2 * 2
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ ((2 * 2 * (n / 4) + n % 4) / 2)
[PROOFSTEP]
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]
[GOAL]
n : ℕ
hn : n % 2 = 1
⊢ 0 < 2
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
hn : n % 2 = 1
⊢ (if n % 4 = 1 then 1 else -1) = (-1) ^ (n % 4 / 2)
[PROOFSTEP]
have help : ∀ m : ℕ, m < 4 → m % 2 = 1 → ite (m = 1) (1 : ℤ) (-1) = (-1) ^ (m / 2) := by decide
[GOAL]
n : ℕ
hn : n % 2 = 1
⊢ ∀ (m : ℕ), m < 4 → m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)
[PROOFSTEP]
decide
[GOAL]
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)
[PROOFSTEP]
exact help (n % 4) (Nat.mod_lt n (by norm_num)) ((Nat.mod_mod_of_dvd n (by norm_num : 2 ∣ 4)).trans hn)
[GOAL]
n : ℕ
hn : n % 2 = 1
help : ∀ (m : ℕ), m < 4 → m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)
⊢ 4 > 0
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
hn : n % 2 = 1
help : ∀ (m : ℕ), m < 4 → m % 2 = 1 → (if m = 1 then 1 else -1) = (-1) ^ (m / 2)
⊢ 2 ∣ 4
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
hn : n % 4 = 1
⊢ ↑χ₄ ↑n = 1
[PROOFSTEP]
rw [χ₄_nat_mod_four, hn]
[GOAL]
n : ℕ
hn : n % 4 = 1
⊢ ↑χ₄ ↑1 = 1
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
hn : n % 4 = 3
⊢ ↑χ₄ ↑n = -1
[PROOFSTEP]
rw [χ₄_nat_mod_four, hn]
[GOAL]
n : ℕ
hn : n % 4 = 3
⊢ ↑χ₄ ↑3 = -1
[PROOFSTEP]
rfl
[GOAL]
n : ℤ
hn : n % 4 = 1
⊢ ↑χ₄ ↑n = 1
[PROOFSTEP]
rw [χ₄_int_mod_four, hn]
[GOAL]
n : ℤ
hn : n % 4 = 1
⊢ ↑χ₄ ↑1 = 1
[PROOFSTEP]
rfl
[GOAL]
n : ℤ
hn : n % 4 = 3
⊢ ↑χ₄ ↑n = -1
[PROOFSTEP]
rw [χ₄_int_mod_four, hn]
[GOAL]
n : ℤ
hn : n % 4 = 3
⊢ ↑χ₄ ↑3 = -1
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
hn : n % 4 = 1
⊢ (-1) ^ (n / 2) = 1
[PROOFSTEP]
rw [← χ₄_eq_neg_one_pow (Nat.odd_of_mod_four_eq_one hn), ← nat_cast_mod, hn]
[GOAL]
n : ℕ
hn : n % 4 = 1
⊢ ↑χ₄ ↑1 = 1
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
hn : n % 4 = 3
⊢ (-1) ^ (n / 2) = -1
[PROOFSTEP]
rw [← χ₄_eq_neg_one_pow (Nat.odd_of_mod_four_eq_three hn), ← nat_cast_mod, hn]
[GOAL]
n : ℕ
hn : n % 4 = 3
⊢ ↑χ₄ ↑3 = -1
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ (x y : ZMod 8),
    OneHom.toFun
        { toFun := ![0, 1, 0, -1, 0, -1, 0, 1],
          map_one' := (_ : Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 1 = Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 1) }
        (x * y) =
      OneHom.toFun
          { toFun := ![0, 1, 0, -1, 0, -1, 0, 1],
            map_one' :=
              (_ : Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 1 = Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 1) }
          x *
        OneHom.toFun
          { toFun := ![0, 1, 0, -1, 0, -1, 0, 1],
            map_one' :=
              (_ : Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 1 = Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 1) }
          y
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a : ZMod 8),
    ¬IsUnit a →
      OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := ![0, 1, 0, -1, 0, -1, 0, 1],
                  map_one' :=
                    (_ : Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 1 = Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : ZMod 8),
                    OneHom.toFun
                        { toFun := ![0, 1, 0, -1, 0, -1, 0, 1],
                          map_one' :=
                            (_ :
                              Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 1 =
                                Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := ![0, 1, 0, -1, 0, -1, 0, 1],
                            map_one' :=
                              (_ :
                                Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 1 =
                                  Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 1) }
                          x *
                        OneHom.toFun
                          { toFun := ![0, 1, 0, -1, 0, -1, 0, 1],
                            map_one' :=
                              (_ :
                                Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 1 =
                                  Matrix.vecCons 0 ![1, 0, -1, 0, -1, 0, 1] 1) }
                          y) })
          a =
        0
[PROOFSTEP]
decide
[GOAL]
⊢ MulChar.IsQuadratic χ₈
[PROOFSTEP]
intro a
[GOAL]
a : ZMod 8
⊢ ↑χ₈ a = 0 ∨ ↑χ₈ a = 1 ∨ ↑χ₈ a = -1
[PROOFSTEP]
fin_cases a
[GOAL]
case head
⊢ ↑χ₈ { val := 0, isLt := (_ : 0 < 7 + 1) } = 0 ∨
    ↑χ₈ { val := 0, isLt := (_ : 0 < 7 + 1) } = 1 ∨ ↑χ₈ { val := 0, isLt := (_ : 0 < 7 + 1) } = -1
case tail.head
⊢ ↑χ₈ { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } = 0 ∨
    ↑χ₈ { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } = 1 ∨
      ↑χ₈ { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } = -1
case tail.tail.head
⊢ ↑χ₈ { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } = 0 ∨
    ↑χ₈ { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } = 1 ∨
      ↑χ₈ { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } = -1
case tail.tail.tail.head
⊢ ↑χ₈ { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } = 0 ∨
    ↑χ₈ { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } = 1 ∨
      ↑χ₈ { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } = -1
case tail.tail.tail.tail.head
⊢ ↑χ₈ { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } = 0 ∨
    ↑χ₈ { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } = 1 ∨
      ↑χ₈ { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } = -1
case tail.tail.tail.tail.tail.head
⊢ ↑χ₈ { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } = 0 ∨
    ↑χ₈ { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } = 1 ∨
      ↑χ₈ { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } = -1
case tail.tail.tail.tail.tail.tail.head
⊢ ↑χ₈
        { val := 6,
          isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } =
      0 ∨
    ↑χ₈
          { val := 6,
            isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } =
        1 ∨
      ↑χ₈
          { val := 6,
            isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } =
        -1
case tail.tail.tail.tail.tail.tail.tail.head
⊢ ↑χ₈
        { val := 7,
          isLt :=
            (_ :
              (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a) 7) } =
      0 ∨
    ↑χ₈
          { val := 7,
            isLt :=
              (_ :
                (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a)
                  7) } =
        1 ∨
      ↑χ₈
          { val := 7,
            isLt :=
              (_ :
                (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a)
                  7) } =
        -1
[PROOFSTEP]
all_goals decide
[GOAL]
case head
⊢ ↑χ₈ { val := 0, isLt := (_ : 0 < 7 + 1) } = 0 ∨
    ↑χ₈ { val := 0, isLt := (_ : 0 < 7 + 1) } = 1 ∨ ↑χ₈ { val := 0, isLt := (_ : 0 < 7 + 1) } = -1
[PROOFSTEP]
decide
[GOAL]
case tail.head
⊢ ↑χ₈ { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } = 0 ∨
    ↑χ₈ { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } = 1 ∨
      ↑χ₈ { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } = -1
[PROOFSTEP]
decide
[GOAL]
case tail.tail.head
⊢ ↑χ₈ { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } = 0 ∨
    ↑χ₈ { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } = 1 ∨
      ↑χ₈ { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } = -1
[PROOFSTEP]
decide
[GOAL]
case tail.tail.tail.head
⊢ ↑χ₈ { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } = 0 ∨
    ↑χ₈ { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } = 1 ∨
      ↑χ₈ { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } = -1
[PROOFSTEP]
decide
[GOAL]
case tail.tail.tail.tail.head
⊢ ↑χ₈ { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } = 0 ∨
    ↑χ₈ { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } = 1 ∨
      ↑χ₈ { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } = -1
[PROOFSTEP]
decide
[GOAL]
case tail.tail.tail.tail.tail.head
⊢ ↑χ₈ { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } = 0 ∨
    ↑χ₈ { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } = 1 ∨
      ↑χ₈ { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } = -1
[PROOFSTEP]
decide
[GOAL]
case tail.tail.tail.tail.tail.tail.head
⊢ ↑χ₈
        { val := 6,
          isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } =
      0 ∨
    ↑χ₈
          { val := 6,
            isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } =
        1 ∨
      ↑χ₈
          { val := 6,
            isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } =
        -1
[PROOFSTEP]
decide
[GOAL]
case tail.tail.tail.tail.tail.tail.tail.head
⊢ ↑χ₈
        { val := 7,
          isLt :=
            (_ :
              (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a) 7) } =
      0 ∨
    ↑χ₈
          { val := 7,
            isLt :=
              (_ :
                (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a)
                  7) } =
        1 ∨
      ↑χ₈
          { val := 7,
            isLt :=
              (_ :
                (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a)
                  7) } =
        -1
[PROOFSTEP]
decide
[GOAL]
n : ℕ
⊢ ↑χ₈ ↑n = ↑χ₈ ↑(n % 8)
[PROOFSTEP]
rw [← ZMod.nat_cast_mod n 8]
[GOAL]
n : ℤ
⊢ ↑χ₈ ↑n = ↑χ₈ ↑(n % 8)
[PROOFSTEP]
rw [← ZMod.int_cast_mod n 8]
[GOAL]
n : ℤ
⊢ ↑χ₈ ↑(n % ↑8) = ↑χ₈ ↑(n % 8)
[PROOFSTEP]
norm_cast
[GOAL]
n : ℤ
⊢ ↑χ₈ ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1
[PROOFSTEP]
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
[GOAL]
n : ℤ
⊢ ∀ (m : ℤ), 0 ≤ m → m < 8 → ↑χ₈ ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 then 1 else -1
[PROOFSTEP]
decide
[GOAL]
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
[PROOFSTEP]
rw [← Int.emod_emod_of_dvd n (by norm_num : (2 : ℤ) ∣ 8), ← ZMod.int_cast_mod n 8]
[GOAL]
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
[PROOFSTEP]
norm_num
[GOAL]
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
[PROOFSTEP]
exact help (n % 8) (Int.emod_nonneg n (by norm_num)) (Int.emod_lt n (by norm_num))
[GOAL]
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
[PROOFSTEP]
norm_num
[GOAL]
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
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
⊢ ↑χ₈ ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 7 then 1 else -1
[PROOFSTEP]
exact_mod_cast χ₈_int_eq_if_mod_eight n
[GOAL]
⊢ ∀ (x y : ZMod 8),
    OneHom.toFun
        { toFun := ![0, 1, 0, 1, 0, -1, 0, -1],
          map_one' := (_ : Matrix.vecCons 0 ![1, 0, 1, 0, -1, 0, -1] 1 = Matrix.vecCons 0 ![1, 0, 1, 0, -1, 0, -1] 1) }
        (x * y) =
      OneHom.toFun
          { toFun := ![0, 1, 0, 1, 0, -1, 0, -1],
            map_one' :=
              (_ : Matrix.vecCons 0 ![1, 0, 1, 0, -1, 0, -1] 1 = Matrix.vecCons 0 ![1, 0, 1, 0, -1, 0, -1] 1) }
          x *
        OneHom.toFun
          { toFun := ![0, 1, 0, 1, 0, -1, 0, -1],
            map_one' :=
              (_ : Matrix.vecCons 0 ![1, 0, 1, 0, -1, 0, -1] 1 = Matrix.vecCons 0 ![1, 0, 1, 0, -1, 0, -1] 1) }
          y
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a : ZMod 8),
    ¬IsUnit a →
      OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := ![0, 1, 0, 1, 0, -1, 0, -1],
                  map_one' :=
                    (_ : Matrix.vecCons 0 ![1, 0, 1, 0, -1, 0, -1] 1 = Matrix.vecCons 0 ![1, 0, 1, 0, -1, 0, -1] 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : ZMod 8),
                    OneHom.toFun
                        { toFun := ![0, 1, 0, 1, 0, -1, 0, -1],
                          map_one' :=
                            (_ :
                              Matrix.vecCons 0 ![1, 0, 1, 0, -1, 0, -1] 1 =
                                Matrix.vecCons 0 ![1, 0, 1, 0, -1, 0, -1] 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := ![0, 1, 0, 1, 0, -1, 0, -1],
                            map_one' :=
                              (_ :
                                Matrix.vecCons 0 ![1, 0, 1, 0, -1, 0, -1] 1 =
                                  Matrix.vecCons 0 ![1, 0, 1, 0, -1, 0, -1] 1) }
                          x *
                        OneHom.toFun
                          { toFun := ![0, 1, 0, 1, 0, -1, 0, -1],
                            map_one' :=
                              (_ :
                                Matrix.vecCons 0 ![1, 0, 1, 0, -1, 0, -1] 1 =
                                  Matrix.vecCons 0 ![1, 0, 1, 0, -1, 0, -1] 1) }
                          y) })
          a =
        0
[PROOFSTEP]
decide
[GOAL]
⊢ MulChar.IsQuadratic χ₈'
[PROOFSTEP]
intro a
[GOAL]
a : ZMod 8
⊢ ↑χ₈' a = 0 ∨ ↑χ₈' a = 1 ∨ ↑χ₈' a = -1
[PROOFSTEP]
fin_cases a
[GOAL]
case head
⊢ ↑χ₈' { val := 0, isLt := (_ : 0 < 7 + 1) } = 0 ∨
    ↑χ₈' { val := 0, isLt := (_ : 0 < 7 + 1) } = 1 ∨ ↑χ₈' { val := 0, isLt := (_ : 0 < 7 + 1) } = -1
case tail.head
⊢ ↑χ₈' { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } = 0 ∨
    ↑χ₈' { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } = 1 ∨
      ↑χ₈' { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } = -1
case tail.tail.head
⊢ ↑χ₈' { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } = 0 ∨
    ↑χ₈' { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } = 1 ∨
      ↑χ₈' { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } = -1
case tail.tail.tail.head
⊢ ↑χ₈' { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } = 0 ∨
    ↑χ₈' { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } = 1 ∨
      ↑χ₈' { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } = -1
case tail.tail.tail.tail.head
⊢ ↑χ₈' { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } = 0 ∨
    ↑χ₈' { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } = 1 ∨
      ↑χ₈' { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } = -1
case tail.tail.tail.tail.tail.head
⊢ ↑χ₈' { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } = 0 ∨
    ↑χ₈' { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } = 1 ∨
      ↑χ₈' { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } = -1
case tail.tail.tail.tail.tail.tail.head
⊢ ↑χ₈'
        { val := 6,
          isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } =
      0 ∨
    ↑χ₈'
          { val := 6,
            isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } =
        1 ∨
      ↑χ₈'
          { val := 6,
            isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } =
        -1
case tail.tail.tail.tail.tail.tail.tail.head
⊢ ↑χ₈'
        { val := 7,
          isLt :=
            (_ :
              (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a) 7) } =
      0 ∨
    ↑χ₈'
          { val := 7,
            isLt :=
              (_ :
                (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a)
                  7) } =
        1 ∨
      ↑χ₈'
          { val := 7,
            isLt :=
              (_ :
                (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a)
                  7) } =
        -1
[PROOFSTEP]
all_goals decide
[GOAL]
case head
⊢ ↑χ₈' { val := 0, isLt := (_ : 0 < 7 + 1) } = 0 ∨
    ↑χ₈' { val := 0, isLt := (_ : 0 < 7 + 1) } = 1 ∨ ↑χ₈' { val := 0, isLt := (_ : 0 < 7 + 1) } = -1
[PROOFSTEP]
decide
[GOAL]
case tail.head
⊢ ↑χ₈' { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } = 0 ∨
    ↑χ₈' { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } = 1 ∨
      ↑χ₈' { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } = -1
[PROOFSTEP]
decide
[GOAL]
case tail.tail.head
⊢ ↑χ₈' { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } = 0 ∨
    ↑χ₈' { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } = 1 ∨
      ↑χ₈' { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } = -1
[PROOFSTEP]
decide
[GOAL]
case tail.tail.tail.head
⊢ ↑χ₈' { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } = 0 ∨
    ↑χ₈' { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } = 1 ∨
      ↑χ₈' { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } = -1
[PROOFSTEP]
decide
[GOAL]
case tail.tail.tail.tail.head
⊢ ↑χ₈' { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } = 0 ∨
    ↑χ₈' { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } = 1 ∨
      ↑χ₈' { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } = -1
[PROOFSTEP]
decide
[GOAL]
case tail.tail.tail.tail.tail.head
⊢ ↑χ₈' { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } = 0 ∨
    ↑χ₈' { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } = 1 ∨
      ↑χ₈' { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } = -1
[PROOFSTEP]
decide
[GOAL]
case tail.tail.tail.tail.tail.tail.head
⊢ ↑χ₈'
        { val := 6,
          isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } =
      0 ∨
    ↑χ₈'
          { val := 6,
            isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } =
        1 ∨
      ↑χ₈'
          { val := 6,
            isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } =
        -1
[PROOFSTEP]
decide
[GOAL]
case tail.tail.tail.tail.tail.tail.tail.head
⊢ ↑χ₈'
        { val := 7,
          isLt :=
            (_ :
              (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a) 7) } =
      0 ∨
    ↑χ₈'
          { val := 7,
            isLt :=
              (_ :
                (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a)
                  7) } =
        1 ∨
      ↑χ₈'
          { val := 7,
            isLt :=
              (_ :
                (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a)
                  7) } =
        -1
[PROOFSTEP]
decide
[GOAL]
n : ℤ
⊢ ↑χ₈' ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1
[PROOFSTEP]
have help : ∀ m : ℤ, 0 ≤ m → m < 8 → χ₈' m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1 := by decide
[GOAL]
n : ℤ
⊢ ∀ (m : ℤ), 0 ≤ m → m < 8 → ↑χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1
[PROOFSTEP]
decide
[GOAL]
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → ↑χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1
⊢ ↑χ₈' ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1
[PROOFSTEP]
rw [← Int.emod_emod_of_dvd n (by norm_num : (2 : ℤ) ∣ 8), ← ZMod.int_cast_mod n 8]
[GOAL]
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → ↑χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1
⊢ 2 ∣ 8
[PROOFSTEP]
norm_num
[GOAL]
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → ↑χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1
⊢ ↑χ₈' ↑(n % ↑8) = if n % 8 % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1
[PROOFSTEP]
exact help (n % 8) (Int.emod_nonneg n (by norm_num)) (Int.emod_lt n (by norm_num))
[GOAL]
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → ↑χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1
⊢ 8 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
n : ℤ
help : ∀ (m : ℤ), 0 ≤ m → m < 8 → ↑χ₈' ↑m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1
⊢ 8 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
⊢ ↑χ₈' ↑n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1
[PROOFSTEP]
exact_mod_cast χ₈'_int_eq_if_mod_eight n
[GOAL]
a : ZMod 8
⊢ ↑χ₈' a = ↑χ₄ ↑a * ↑χ₈ a
[PROOFSTEP]
fin_cases a
[GOAL]
case head
⊢ ↑χ₈' { val := 0, isLt := (_ : 0 < 7 + 1) } =
    ↑χ₄ ↑{ val := 0, isLt := (_ : 0 < 7 + 1) } * ↑χ₈ { val := 0, isLt := (_ : 0 < 7 + 1) }
case tail.head
⊢ ↑χ₈' { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } =
    ↑χ₄ ↑{ val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } * ↑χ₈ { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) }
case tail.tail.head
⊢ ↑χ₈' { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } =
    ↑χ₄ ↑{ val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } *
      ↑χ₈ { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) }
case tail.tail.tail.head
⊢ ↑χ₈' { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } =
    ↑χ₄ ↑{ val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } *
      ↑χ₈ { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) }
case tail.tail.tail.tail.head
⊢ ↑χ₈' { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } =
    ↑χ₄ ↑{ val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } *
      ↑χ₈ { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) }
case tail.tail.tail.tail.tail.head
⊢ ↑χ₈' { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } =
    ↑χ₄ ↑{ val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } *
      ↑χ₈ { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) }
case tail.tail.tail.tail.tail.tail.head
⊢ ↑χ₈'
      { val := 6,
        isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } =
    ↑χ₄
        ↑{ val := 6,
            isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } *
      ↑χ₈
        { val := 6,
          isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) }
case tail.tail.tail.tail.tail.tail.tail.head
⊢ ↑χ₈'
      { val := 7,
        isLt :=
          (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a) 7) } =
    ↑χ₄
        ↑{ val := 7,
            isLt :=
              (_ :
                (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a)
                  7) } *
      ↑χ₈
        { val := 7,
          isLt :=
            (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a) 7) }
[PROOFSTEP]
all_goals decide
[GOAL]
case head
⊢ ↑χ₈' { val := 0, isLt := (_ : 0 < 7 + 1) } =
    ↑χ₄ ↑{ val := 0, isLt := (_ : 0 < 7 + 1) } * ↑χ₈ { val := 0, isLt := (_ : 0 < 7 + 1) }
[PROOFSTEP]
decide
[GOAL]
case tail.head
⊢ ↑χ₈' { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } =
    ↑χ₄ ↑{ val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) } * ↑χ₈ { val := 1, isLt := (_ : (fun a => a < 7 + 1) 1) }
[PROOFSTEP]
decide
[GOAL]
case tail.tail.head
⊢ ↑χ₈' { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } =
    ↑χ₄ ↑{ val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) } *
      ↑χ₈ { val := 2, isLt := (_ : (fun a => (fun a => a < 7 + 1) a) 2) }
[PROOFSTEP]
decide
[GOAL]
case tail.tail.tail.head
⊢ ↑χ₈' { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } =
    ↑χ₄ ↑{ val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) } *
      ↑χ₈ { val := 3, isLt := (_ : (fun a => (fun a => (fun a => a < 7 + 1) a) a) 3) }
[PROOFSTEP]
decide
[GOAL]
case tail.tail.tail.tail.head
⊢ ↑χ₈' { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } =
    ↑χ₄ ↑{ val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) } *
      ↑χ₈ { val := 4, isLt := (_ : (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) 4) }
[PROOFSTEP]
decide
[GOAL]
case tail.tail.tail.tail.tail.head
⊢ ↑χ₈' { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } =
    ↑χ₄ ↑{ val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) } *
      ↑χ₈ { val := 5, isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) 5) }
[PROOFSTEP]
decide
[GOAL]
case tail.tail.tail.tail.tail.tail.head
⊢ ↑χ₈'
      { val := 6,
        isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } =
    ↑χ₄
        ↑{ val := 6,
            isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) } *
      ↑χ₈
        { val := 6,
          isLt := (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) 6) }
[PROOFSTEP]
decide
[GOAL]
case tail.tail.tail.tail.tail.tail.tail.head
⊢ ↑χ₈'
      { val := 7,
        isLt :=
          (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a) 7) } =
    ↑χ₄
        ↑{ val := 7,
            isLt :=
              (_ :
                (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a)
                  7) } *
      ↑χ₈
        { val := 7,
          isLt :=
            (_ : (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => (fun a => a < 7 + 1) a) a) a) a) a) a) 7) }
[PROOFSTEP]
decide
[GOAL]
a : ℤ
⊢ ↑χ₈' ↑a = ↑χ₄ ↑a * ↑χ₈ ↑a
[PROOFSTEP]
rw [← @cast_int_cast 8 (ZMod 4) _ 4 _ (by norm_num) a]
[GOAL]
a : ℤ
⊢ 4 ∣ 8
[PROOFSTEP]
norm_num
[GOAL]
a : ℤ
⊢ ↑χ₈' ↑a = ↑χ₄ ↑↑a * ↑χ₈ ↑a
[PROOFSTEP]
exact χ₈'_eq_χ₄_mul_χ₈ a
