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