From 657fbc5d39544c7b1b7157b0fdd82045fcf5fada Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Thu, 31 Oct 2024 12:24:41 -0700
Subject: [PATCH] Tidy up FLT.lean (#188)

---
 FLT.lean | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

diff --git a/FLT.lean b/FLT.lean
index f72385de..ca557983 100644
--- a/FLT.lean
+++ b/FLT.lean
@@ -1,5 +1,4 @@
-import FLT.FLT_files -- **FIXME** need this hack to make check_decls work in leanblueprint
-import FLT.Basic.Reductions
+import FLT.FLT_files -- import the project files
 
 /-!
 
@@ -12,6 +11,13 @@ a proof of Mathlib's version `FermatLastTheorem`
 of the statement (which is a statement about the
 nonnegative integers `ℕ`.)
 
+Note that many of the files imported by this file contain
+"sorried" theorems, that is, theorems whose proofs
+are not yet complete. So whilst the below looks
+like a complete proof of Fermat's Last Theorem, it
+currently relies on many incomplete proofs along the way,
+and is likely to do so for several years.
+
 -/
 
 /-- Fermat's Last Theorem for positive naturals. -/
@@ -20,3 +26,11 @@ theorem PNat.pow_add_pow_ne_pow
     (n : ℕ) (hn : n > 2) :
     x^n + y^n ≠ z^n :=
   PNat.pow_add_pow_ne_pow_of_FermatLastTheorem FLT.Wiles_Taylor_Wiles x y z n hn
+
+#print axioms PNat.pow_add_pow_ne_pow
+/-
+'PNat.pow_add_pow_ne_pow' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]
+-/
+
+-- The project will be complete when `sorryAx` is no longer
+-- mentioned in the output of this last command.