From b8e530f6e08a1bf96a76ac5ee7f65808dfb9b885 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sun, 22 Oct 2023 16:13:36 +0100 Subject: [PATCH] reinstate IGiveUp --- Game/Levels/Power/L10FLT.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Game/Levels/Power/L10FLT.lean b/Game/Levels/Power/L10FLT.lean index da6c096..53b20fd 100644 --- a/Game/Levels/Power/L10FLT.lean +++ b/Game/Levels/Power/L10FLT.lean @@ -37,7 +37,7 @@ 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"