--- /dev/null
+++ b/Mathlib/Unsorry/ThreeFourthPowersZmodSixteenMem.lean
@@ -0,0 +1,14 @@
+/-
+Copyright (c) 2026 Chris Barlow. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Barlow
+-/
+import Mathlib
+
+theorem three_fourth_powers_zmod_sixteen_mem (a b c : ℤ) :
+    ((a^4 + b^4 + c^4 : ℤ) : ZMod 16) ∈ ({0, 1, 2, 3} : Set (ZMod 16)) := by
+  first
+    | (push_cast; generalize (a : ZMod 16) = z0; generalize (b : ZMod 16) = z1; generalize (c : ZMod 16) = z2; revert z0 z1 z2; decide)
+    | (generalize (a : ZMod 16) = z0; generalize (b : ZMod 16) = z1; generalize (c : ZMod 16) = z2; revert z0 z1 z2; decide)
+    | (push_cast; decide)
+    | decide