For every non-negative integer n, the fourth power n^4 leaves remainder 0 or 1 when divided by 5 (never 2, 3, or 4).

Enuntiatio — the claim

For every non-negative integer n, the fourth power n^4 leaves remainder 0 or 1 when divided by 5 (never 2, 3, or 4).

Refuted by Some non-negative integer n with n^4 % 5 equal to 2, 3, or 4.

Expressio — the formal statement

import Mathlib

theorem n_fourth_mod_five (n : ℕ) : n^4 % 5 = 0 ∨ n^4 % 5 = 1

Demonstratio — the kernel-checked proof

by
  have h : n % 5 = 0 ∨ n % 5 = 1 ∨ n % 5 = 2 ∨ n % 5 = 3 ∨ n % 5 = 4 := by
    omega
  rcases h with (h | h | h | h | h)
  · -- Case n ≡ 0 mod 5
    have h₁ : n^4 % 5 = 0 := by
      have h₂ : n % 5 = 0 := h
      have h₃ : n^4 % 5 = 0 := by
        have h₄ : n % 5 = 0 := h₂
        have h₅ : n^4 % 5 = 0 := by
          simp [h₄, pow_succ, Nat.mul_mod, Nat.pow_mod]
        exact h₅
      exact h₃
    exact Or.inl h₁
  · -- Case n ≡ 1 mod 5
    have h₁ : n^4 % 5 = 1 := by
      have h₂ : n % 5 = 1 := h
      have h₃ : n^4 % 5 = 1 := by
        have h₄ : n % 5 = 1 := h₂
        have h₅ : n^4 % 5 = 1 := by
          simp [h₄, pow_succ, Nat.mul_mod, Nat.pow_mod]
        exact h₅
      exact h₃
    exact Or.inr h₁
  · -- Case n ≡ 2 mod 5
    have h₁ : n^4 % 5 = 1 := by
      have h₂ : n % 5 = 2 := h
      have h₃ : n^4 % 5 = 1 := by
        have h₄ : n % 5 = 2 := h₂
        have h₅ : n^4 % 5 = 1 := by
          simp [h₄, pow_succ, Nat.mul_mod, Nat.pow_mod]
        exact h₅
      exact h₃
    exact Or.inr h₁
  · -- Case n ≡ 3 mod 5
    have h₁ : n^4 % 5 = 1 := by
      have h₂ : n % 5 = 3 := h
      have h₃ : n^4 % 5 = 1 := by
        have h₄ : n % 5 = 3 := h₂
        have h₅ : n^4 % 5 = 1 := by
          simp [h₄, pow_succ, Nat.mul_mod, Nat.pow_mod]
        exact h₅
      exact h₃
    exact Or.inr h₁
  · -- Case n ≡ 4 mod 5
    have h₁ : n^4 % 5 = 1 := by
      have h₂ : n % 5 = 4 := h
      have h₃ : n^4 % 5 = 1 := by
        have h₄ : n % 5 = 4 := h₂
        have h₅ : n^4 % 5 = 1 := by
          simp [h₄, pow_succ, Nat.mul_mod, Nat.pow_mod]
        exact h₅
      exact h₃
    exact Or.inr h₁