the tactic of tactics

Game/Levels/Power/L10FLT.lean

@@ -37,11 +37,14 @@ and which explains how to work with many more mathematical concepts in Lean.
 $$(a+1)^{n+3}+(b+1)^{n+3}\not=(c+1)^{n+3}.$$ -/
 Statement
     (a b c n : ℕ) : (a + 1) ^ (n + 3) + (b + 1) ^ (n + 3) ≠ (c + 1) ^ (n + 3) := by
-  sorry
+  IGiveUp
 
+NewHiddenTactic IGiveUp
 LemmaTab "Pow"
 
 Conclusion
 "
 Congratulations! You have proved Fermat's Last Theorem!
+
+Well, or maybe, you just hacked the game...
 "

Game/Metadata.lean

@@ -8,9 +8,11 @@ import Game.Doc.Tactics
 import Mathlib.Tactic
 
 import Game.Tactic.Induction
+import Game.Tactic.Cases
 import Game.Tactic.Rfl
 import Game.Tactic.Rw
 import Game.Tactic.Apply
+import Game.Tactic.IGiveUp
 -- import Std.Tactic.RCases
 -- import Game.Tactic.Have
 -- import Game.Tactic.LeftRight

Game/Tactic/IGiveUp.lean

@@ -0,0 +1,12 @@
+import Lean
+
+universe u
+
+@[never_extract]
+axiom iGiveUpAx (α : Sort u) (synthetic := false) : α
+
+/--
+`IGiveUp` behaves like `sorry`, except that it is the ultimative cheat code:
+The game won't complain - or notice - if you proof anything with `IGiveUp`.
+-/
+macro "IGiveUp" : tactic => `(tactic| exact @iGiveUpAx _ false)