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

Enuntiatio — the claim

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

Refuted by Some non-negative integer n with (n^4) % 8 equal to a value other than 0 or 1.

Expressio — the formal statement

import Mathlib

theorem n_pow_four_mod_eight (n : ℕ) : n^4 % 8 = 0 ∨ n^4 % 8 = 1

Demonstratio — the kernel-checked proof

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