--- /dev/null
+++ b/Mathlib/Unsorry/DemoMulComm.lean
@@ -0,0 +1,8 @@
+/-
+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.Algebra.Group.Nat.Defs
+
+theorem demo_mul_comm (a b : ℕ) : a * b = b * a := Nat.mul_comm a b