[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


[GOAL]
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ HomologicalComplex.Hom.f (AlgebraicTopology.inclusionOfMooreComplexMap X) (n + 1) ≫
      SimplicialObject.δ X (Fin.succ j) =
    0
[PROOFSTEP]
dsimp [AlgebraicTopology.inclusionOfMooreComplexMap, NormalizedMooreComplex.objX]
[GOAL]
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ arrow (Finset.inf Finset.univ fun k => kernelSubobject (SimplicialObject.δ X (Fin.succ k))) ≫
      SimplicialObject.δ X (Fin.succ j) =
    0
[PROOFSTEP]
rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ j (by simp only [Finset.mem_univ])), assoc,
  kernelSubobject_arrow_comp, comp_zero]
[GOAL]
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
j : Fin (n + 1)
x✝ : n + 1 ≤ ↑j + (n + 1)
⊢ j ∈ Finset.univ
[PROOFSTEP]
simp only [Finset.mem_univ]
[GOAL]
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ Factors (NormalizedMooreComplex.objX X n) (HomologicalComplex.Hom.f PInfty n)
[PROOFSTEP]
rcases n with _ | n
[GOAL]
case zero
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ Factors (NormalizedMooreComplex.objX X Nat.zero) (HomologicalComplex.Hom.f PInfty Nat.zero)
[PROOFSTEP]
apply top_factors
[GOAL]
case succ
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ Factors (NormalizedMooreComplex.objX X (Nat.succ n)) (HomologicalComplex.Hom.f PInfty (Nat.succ n))
[PROOFSTEP]
rw [PInfty_f, NormalizedMooreComplex.objX, finset_inf_factors]
[GOAL]
case succ
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
⊢ ∀ (i : Fin (n + 1)),
    i ∈ Finset.univ →
      Factors (kernelSubobject (SimplicialObject.δ X (Fin.succ i)))
        (HomologicalComplex.Hom.f (P (Nat.succ n)) (Nat.succ n))
[PROOFSTEP]
intro i _
[GOAL]
case succ
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
i : Fin (n + 1)
a✝ : i ∈ Finset.univ
⊢ Factors (kernelSubobject (SimplicialObject.δ X (Fin.succ i))) (HomologicalComplex.Hom.f (P (Nat.succ n)) (Nat.succ n))
[PROOFSTEP]
apply kernelSubobject_factors
[GOAL]
case succ.w
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
n : ℕ
i : Fin (n + 1)
a✝ : i ∈ Finset.univ
⊢ HomologicalComplex.Hom.f (P (Nat.succ n)) (Nat.succ n) ≫ SimplicialObject.δ X (Fin.succ i) = 0
[PROOFSTEP]
exact (HigherFacesVanish.of_P (n + 1) n) i le_add_self
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.88673, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ (fun n =>
          factorThru (NormalizedMooreComplex.objX X n) (HomologicalComplex.Hom.f PInfty n)
            (_ : Factors (NormalizedMooreComplex.objX X n) (HomologicalComplex.Hom.f PInfty n)))
        (n + 1) ≫
      NormalizedMooreComplex.objD X n =
    AlternatingFaceMapComplex.objD X n ≫
      (fun n =>
          factorThru (NormalizedMooreComplex.objX X n) (HomologicalComplex.Hom.f PInfty n)
            (_ : Factors (NormalizedMooreComplex.objX X n) (HomologicalComplex.Hom.f PInfty n)))
        n
[PROOFSTEP]
rw [← cancel_mono (NormalizedMooreComplex.objX X n).arrow, assoc, assoc, factorThru_arrow, ←
  inclusionOfMooreComplexMap_f, ← normalizedMooreComplex_objD, ← (inclusionOfMooreComplexMap X).comm (n + 1) n,
  inclusionOfMooreComplexMap_f, factorThru_arrow_assoc, ← alternatingFaceMapComplex_obj_d]
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.88673, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ HomologicalComplex.Hom.f PInfty (n + 1) ≫ HomologicalComplex.d ((alternatingFaceMapComplex A).obj X) (n + 1) n =
    HomologicalComplex.d ((alternatingFaceMapComplex A).obj X) (n + 1) n ≫ HomologicalComplex.Hom.f PInfty n
[PROOFSTEP]
exact PInfty.comm (n + 1) n
[GOAL]
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ PInftyToNormalizedMooreComplex X ≫ inclusionOfMooreComplexMap X = PInfty
[PROOFSTEP]
aesop_cat
[GOAL]
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X✝ X Y : SimplicialObject A
f : X ⟶ Y
⊢ AlternatingFaceMapComplex.map f ≫ PInftyToNormalizedMooreComplex Y =
    PInftyToNormalizedMooreComplex X ≫ NormalizedMooreComplex.map f
[PROOFSTEP]
aesop_cat
[GOAL]
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ PInfty ≫ PInftyToNormalizedMooreComplex X = PInftyToNormalizedMooreComplex X
[PROOFSTEP]
aesop_cat
[GOAL]
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X ≫ PInfty = inclusionOfMooreComplexMap X
[PROOFSTEP]
ext (_ | n)
[GOAL]
case h.zero
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X ≫ PInfty) Nat.zero =
    HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) Nat.zero
[PROOFSTEP]
dsimp
[GOAL]
case h.zero
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0 ≫ 𝟙 (X.obj (Opposite.op (SimplexCategory.mk 0))) =
    HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0
[PROOFSTEP]
simp only [comp_id]
[GOAL]
case h.succ
A : Type u_1
inst✝¹ : Category.{u_2, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
n : ℕ
⊢ HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X ≫ PInfty) (Nat.succ n) =
    HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) (Nat.succ n)
[PROOFSTEP]
exact (HigherFacesVanish.inclusionOfMooreComplexMap n).comp_P_eq_self
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.108671, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
Z✝ : ChainComplex A ℕ
x✝¹ x✝ : Z✝ ⟶ (normalizedMooreComplex A).obj X
hf : x✝¹ ≫ inclusionOfMooreComplexMap X = x✝ ≫ inclusionOfMooreComplexMap X
⊢ x✝¹ = x✝
[PROOFSTEP]
ext n
[GOAL]
case h
A : Type u_1
inst✝¹ : Category.{?u.108671, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
Z✝ : ChainComplex A ℕ
x✝¹ x✝ : Z✝ ⟶ (normalizedMooreComplex A).obj X
hf : x✝¹ ≫ inclusionOfMooreComplexMap X = x✝ ≫ inclusionOfMooreComplexMap X
n : ℕ
⊢ HomologicalComplex.Hom.f x✝¹ n = HomologicalComplex.Hom.f x✝ n
[PROOFSTEP]
dsimp
[GOAL]
case h
A : Type u_1
inst✝¹ : Category.{?u.108671, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
Z✝ : ChainComplex A ℕ
x✝¹ x✝ : Z✝ ⟶ (normalizedMooreComplex A).obj X
hf : x✝¹ ≫ inclusionOfMooreComplexMap X = x✝ ≫ inclusionOfMooreComplexMap X
n : ℕ
⊢ HomologicalComplex.Hom.f x✝¹ n = HomologicalComplex.Hom.f x✝ n
[PROOFSTEP]
ext
[GOAL]
case h.h
A : Type u_1
inst✝¹ : Category.{?u.108671, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
Z✝ : ChainComplex A ℕ
x✝¹ x✝ : Z✝ ⟶ (normalizedMooreComplex A).obj X
hf : x✝¹ ≫ inclusionOfMooreComplexMap X = x✝ ≫ inclusionOfMooreComplexMap X
n : ℕ
⊢ HomologicalComplex.Hom.f x✝¹ n ≫ arrow (NormalizedMooreComplex.objX X n) =
    HomologicalComplex.Hom.f x✝ n ≫ arrow (NormalizedMooreComplex.objX X n)
[PROOFSTEP]
exact HomologicalComplex.congr_hom hf n
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.109759, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X ≫ PInftyToNormalizedMooreComplex X = 𝟙 ((normalizedMooreComplex A).obj X)
[PROOFSTEP]
simp only [← cancel_mono (inclusionOfMooreComplexMap X), assoc, id_comp,
  PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, inclusionOfMooreComplexMap_comp_PInfty]
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ PInftyToNormalizedMooreComplex X =
    (N₁.obj X).p ≫
      PInftyToNormalizedMooreComplex X ≫ ((normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ)).obj X).p
[PROOFSTEP]
erw [comp_id, PInfty_comp_PInftyToNormalizedMooreComplex]
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X Y : SimplicialObject A
f : X ⟶ Y
⊢ N₁.map f ≫ (fun X => Karoubi.Hom.mk (PInftyToNormalizedMooreComplex X)) Y =
    (fun X => Karoubi.Hom.mk (PInftyToNormalizedMooreComplex X)) X ≫
      (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ)).map f
[PROOFSTEP]
simp only [Functor.comp_map, normalizedMooreComplex_map, PInftyToNormalizedMooreComplex_naturality, Karoubi.hom_ext_iff,
  Karoubi.comp_f, N₁_map_f, PInfty_comp_PInftyToNormalizedMooreComplex_assoc, toKaroubi_map_f, assoc]
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X =
    ((normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ)).obj X).p ≫ inclusionOfMooreComplexMap X ≫ (N₁.obj X).p
[PROOFSTEP]
erw [inclusionOfMooreComplexMap_comp_PInfty, id_comp]
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X Y : SimplicialObject A
f : X ⟶ Y
⊢ (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ)).map f ≫
      (fun X => Karoubi.Hom.mk (inclusionOfMooreComplexMap X)) Y =
    (fun X => Karoubi.Hom.mk (inclusionOfMooreComplexMap X)) X ≫ N₁.map f
[PROOFSTEP]
ext
[GOAL]
case h.h
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X Y : SimplicialObject A
f : X ⟶ Y
i✝ : ℕ
⊢ HomologicalComplex.Hom.f
      ((normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ)).map f ≫
          (fun X => Karoubi.Hom.mk (inclusionOfMooreComplexMap X)) Y).f
      i✝ =
    HomologicalComplex.Hom.f ((fun X => Karoubi.Hom.mk (inclusionOfMooreComplexMap X)) X ≫ N₁.map f).f i✝
[PROOFSTEP]
simp only [Functor.comp_map, normalizedMooreComplex_map, Karoubi.comp_f, toKaroubi_map_f, HomologicalComplex.comp_f,
  NormalizedMooreComplex.map_f, inclusionOfMooreComplexMap_f, factorThru_arrow, N₁_map_f,
  inclusionOfMooreComplexMap_comp_PInfty_assoc, AlternatingFaceMapComplex.map_f]
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ ((NatTrans.mk fun X => Karoubi.Hom.mk (PInftyToNormalizedMooreComplex X)) ≫
      NatTrans.mk fun X => Karoubi.Hom.mk (inclusionOfMooreComplexMap X)) =
    𝟙 N₁
[PROOFSTEP]
ext X : 3
[GOAL]
case w.h.h
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ (NatTrans.app
        ((NatTrans.mk fun X => Karoubi.Hom.mk (PInftyToNormalizedMooreComplex X)) ≫
          NatTrans.mk fun X => Karoubi.Hom.mk (inclusionOfMooreComplexMap X))
        X).f =
    (NatTrans.app (𝟙 N₁) X).f
[PROOFSTEP]
simp only [PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, NatTrans.comp_app, Karoubi.comp_f, N₁_obj_p,
  NatTrans.id_app, Karoubi.id_eq]
[GOAL]
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X : SimplicialObject A
⊢ ((NatTrans.mk fun X => Karoubi.Hom.mk (inclusionOfMooreComplexMap X)) ≫
      NatTrans.mk fun X => Karoubi.Hom.mk (PInftyToNormalizedMooreComplex X)) =
    𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ))
[PROOFSTEP]
ext X : 3
[GOAL]
case w.h.h
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ (NatTrans.app
        ((NatTrans.mk fun X => Karoubi.Hom.mk (inclusionOfMooreComplexMap X)) ≫
          NatTrans.mk fun X => Karoubi.Hom.mk (PInftyToNormalizedMooreComplex X))
        X).f =
    (NatTrans.app (𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ))) X).f
[PROOFSTEP]
rw [← cancel_mono (inclusionOfMooreComplexMap X)]
[GOAL]
case w.h.h
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ (NatTrans.app
          ((NatTrans.mk fun X => Karoubi.Hom.mk (inclusionOfMooreComplexMap X)) ≫
            NatTrans.mk fun X => Karoubi.Hom.mk (PInftyToNormalizedMooreComplex X))
          X).f ≫
      inclusionOfMooreComplexMap X =
    (NatTrans.app (𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ))) X).f ≫ inclusionOfMooreComplexMap X
[PROOFSTEP]
simp only [NatTrans.comp_app, Karoubi.comp_f, assoc, NatTrans.id_app, Karoubi.id_eq,
  PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, inclusionOfMooreComplexMap_comp_PInfty]
[GOAL]
case w.h.h
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X =
    ((normalizedMooreComplex A ⋙ toKaroubi (ChainComplex A ℕ)).obj X).p ≫ inclusionOfMooreComplexMap X
[PROOFSTEP]
dsimp only [Functor.comp_obj, toKaroubi]
[GOAL]
case w.h.h
A : Type u_1
inst✝¹ : Category.{?u.110631, u_1} A
inst✝ : Abelian A
X✝ X : SimplicialObject A
⊢ inclusionOfMooreComplexMap X = 𝟙 ((normalizedMooreComplex A).obj X) ≫ inclusionOfMooreComplexMap X
[PROOFSTEP]
erw [id_comp]