For every non-negative integer n, the residue of n^2 + n modulo 6 is always one of 0, 2, or 3 (it is never 1, 4, or 5).

Enuntiatio — the claim

For every non-negative integer n, the residue of n^2 + n modulo 6 is always one of 0, 2, or 3 (it is never 1, 4, or 5).

Refuted by Some non-negative integer n makes (n^2 + n) % 6 equal to 1, 4, or 5.

Expressio — the formal statement

import Mathlib

theorem sq_add_self_mod_six (n : ℕ) : (n^2 + n) % 6 = 0 ∨ (n^2 + n) % 6 = 2 ∨ (n^2 + n) % 6 = 3

Demonstratio — the kernel-checked proof

by
  have h₁ : (n^2 + n) % 6 = 0 ∨ (n^2 + n) % 6 = 2 ∨ (n^2 + n) % 6 = 3 := by
    have h₂ : n % 6 = 0 ∨ n % 6 = 1 ∨ n % 6 = 2 ∨ n % 6 = 3 ∨ n % 6 = 4 ∨ n % 6 = 5 := by
      omega
    rcases h₂ with (h₂ | h₂ | h₂ | h₂ | h₂ | h₂)
    · -- Case n ≡ 0 mod 6
      have h₃ : (n^2 + n) % 6 = 0 := by
        have h₄ : n % 6 = 0 := h₂
        have h₅ : (n^2 + n) % 6 = 0 := by
          have h₆ : n % 6 = 0 := h₄
          have h₇ : (n^2 + n) % 6 = 0 := by
            simp [h₆, pow_two, Nat.add_mod, Nat.mul_mod, Nat.mod_mod]
            <;> norm_num <;> ring_nf at * <;> omega
          exact h₇
        exact h₅
      exact Or.inl h₃
    · -- Case n ≡ 1 mod 6
      have h₃ : (n^2 + n) % 6 = 2 := by
        have h₄ : n % 6 = 1 := h₂
        have h₅ : (n^2 + n) % 6 = 2 := by
          have h₆ : n % 6 = 1 := h₄
          have h₇ : (n^2 + n) % 6 = 2 := by
            simp [h₆, pow_two, Nat.add_mod, Nat.mul_mod, Nat.mod_mod]
            <;> norm_num <;> ring_nf at * <;> omega
          exact h₇
        exact h₅
      exact Or.inr (Or.inl h₃)
    · -- Case n ≡ 2 mod 6
      have h₃ : (n^2 + n) % 6 = 0 := by
        have h₄ : n % 6 = 2 := h₂
        have h₅ : (n^2 + n) % 6 = 0 := by
          have h₆ : n % 6 = 2 := h₄
          have h₇ : (n^2 + n) % 6 = 0 := by
            simp [h₆, pow_two, Nat.add_mod, Nat.mul_mod, Nat.mod_mod]
            <;> norm_num <;> ring_nf at * <;> omega
          exact h₇
        exact h₅
      exact Or.inl h₃
    · -- Case n ≡ 3 mod 6
      have h₃ : (n^2 + n) % 6 = 0 := by
        have h₄ : n % 6 = 3 := h₂
        have h₅ : (n^2 + n) % 6 = 0 := by
          have h₆ : n % 6 = 3 := h₄
          have h₇ : (n^2 + n) % 6 = 0 := by
            simp [h₆, pow_two, Nat.add_mod, Nat.mul_mod, Nat.mod_mod]
            <;> norm_num <;> ring_nf at * <;> omega
          exact h₇
        exact h₅
      exact Or.inl h₃
    · -- Case n ≡ 4 mod 6
      have h₃ : (n^2 + n) % 6 = 2 := by
        have h₄ : n % 6 = 4 := h₂
        have h₅ : (n^2 + n) % 6 = 2 := by
          have h₆ : n % 6 = 4 := h₄
          have h₇ : (n^2 + n) % 6 = 2 := by
            simp [h₆, pow_two, Nat.add_mod, Nat.mul_mod, Nat.mod_mod]
            <;> norm_num <;> ring_nf at * <;> omega
          exact h₇
        exact h₅
      exact Or.inr (Or.inl h₃)
    · -- Case n ≡ 5 mod 6
      have h₃ : (n^2 + n) % 6 = 0 := by
        have h₄ : n % 6 = 5 := h₂
        have h₅ : (n^2 + n) % 6 = 0 := by
          have h₆ : n % 6 = 5 := h₄
          have h₇ : (n^2 + n) % 6 = 0 := by
            simp [h₆, pow_two, Nat.add_mod, Nat.mul_mod, Nat.mod_mod]
            <;> norm_num <;> ring_nf at * <;> omega
          exact h₇
        exact h₅
      exact Or.inl h₃
  exact h₁