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

Enuntiatio — the claim

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

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

Expressio — the formal statement

import Mathlib

theorem residue_n_sq_plus_3n_mod6 (n : ℕ) : (n^2 + 3*n) % 6 = 0 ∨ (n^2 + 3*n) % 6 = 4 ∨ (n^2 + 3*n) % 6 = 2

Demonstratio — the kernel-checked proof

by
  have aux1 (n : ℕ) : (n^2 + 3*n) % 6 = ((n % 6)^2 + 3*(n % 6)) % 6 := by
    have h : (n^2 + 3*n) % 6 = ((n % 6)^2 + 3*(n % 6)) % 6 := 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₁) <;>
        simp [h₁, pow_two, Nat.add_mod, Nat.mul_mod, Nat.mod_mod, Nat.mod_eq_of_lt]
      <;>
        (try omega) <;>
        (try ring_nf at * <;> omega) <;>
        (try norm_num at * <;> omega)
    exact h
  rw [aux1]
  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₁) <;> simp [h₁] <;> omega