a : ZMod 8
⊢ ↑χ₈' a = 0 ∨ ↑χ₈' a = 1 ∨ ↑χ₈' a = -1
⊢ MulChar.IsQuadratic χ₈'
intro a
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
a : ZMod 8
⊢ ↑χ₈' a = 0 ∨ ↑χ₈' a = 1 ∨ ↑χ₈' a = -1
fin_cases a
no goals
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
all_goals decide
no goals
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
decide