Tidy up FLT.lean (#188)

Author: kbuzzard

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.