theorem FermatLastTheorem.of_odd_primesFermatLastTheorem.of_odd_primes (hprimes : ∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p) : FermatLastTheoremTo prove Fermat's Last Theorem, it suffices to prove it for odd prime exponents.

  (hprimes∀ (p : ℕ), Nat.Prime p → Odd p → FermatLastTheoremFor p :
    ∀ (pℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
),
      Nat.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number.  pℕ →
        OddOdd.{u_2} {α : Type u_2} [Semiring α] (a : α) : PropAn element `a` of a semiring is odd if there exists `k` such `a = 2*k + 1`.  pℕ → FermatLastTheoremForFermatLastTheoremFor (n : ℕ) : PropStatement of Fermat's Last Theorem over the naturals for a given exponent.  pℕ) :
  FermatLastTheoremFermatLastTheorem : PropStatement of Fermat's Last Theorem: `a ^ n + b ^ n = c ^ n` has no nontrivial natural solution
when `n ≥ 3`.

This is now a theorem of Wiles and Taylor--Wiles; see
https://github.com/ImperialCollegeLondon/FLT for an ongoing Lean formalisation of
a proof. 

theorem fermatLastTheoremThreefermatLastTheoremThree : FermatLastTheoremFor 3Fermat's Last Theorem for `n = 3`: if `a b c : ℕ` are all non-zero then
`a ^ 3 + b ^ 3 ≠ c ^ 3`.  :
  FermatLastTheoremForFermatLastTheoremFor (n : ℕ) : PropStatement of Fermat's Last Theorem over the naturals for a given exponent.  3

theorem FermatLastTheorem.of_p_ge_5FermatLastTheorem.of_p_ge_5 (H : ∀ p ≥ 5, Nat.Prime p → FermatLastTheoremFor p) : FermatLastTheoremIf Fermat's Last Theorem is true for primes `p ≥ 5`, then FLT is true. 
  (H∀ p ≥ 5, Nat.Prime p → FermatLastTheoremFor p :
    ∀ pℕ ≥ 5,
      Nat.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number.  pℕ →
        FermatLastTheoremForFermatLastTheoremFor (n : ℕ) : PropStatement of Fermat's Last Theorem over the naturals for a given exponent.  pℕ) :
  FermatLastTheoremFermatLastTheorem : PropStatement of Fermat's Last Theorem: `a ^ n + b ^ n = c ^ n` has no nontrivial natural solution
when `n ≥ 3`.

This is now a theorem of Wiles and Taylor--Wiles; see
https://github.com/ImperialCollegeLondon/FLT for an ongoing Lean formalisation of
a proof. 

theorem FreyPackage.of_not_FermatLastTheorem_p_ge_5FreyPackage.of_not_FermatLastTheorem_p_ge_5 {a b c : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) {p : ℕ}
  (pp : Nat.Prime p) (hp5 : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p) : Nonempty FreyPackageGiven a counterexample a^p+b^p=c^p to Fermat's Last Theorem with p>=5,
there exists a Frey package. 
  {aℤ bℤ cℤ : ℤInt : TypeThe integers.

This type is special-cased by the compiler and overridden with an efficient implementation. The
runtime has a special representation for `Int` that stores “small” signed numbers directly, while
larger numbers use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits
than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit
architectures).
} (haa ≠ 0 : aℤ ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. 0) (hbb ≠ 0 : bℤ ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. 0)
  (hcc ≠ 0 : cℤ ≠Ne.{u} {α : Sort u} (a b : α) : Prop`a ≠ b`, or `Ne a b` is defined as `¬ (a = b)` or `a = b → False`,
and asserts that `a` and `b` are not equal.


Conventions for notations in identifiers:

 * The recommended spelling of `≠` in identifiers is `ne`. 0) {pℕ : ℕNat : TypeThe natural numbers, starting at zero.

This type is special-cased by both the kernel and the compiler, and overridden with an efficient
implementation. Both use a fast arbitrary-precision arithmetic library (usually
[GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.
} (ppNat.Prime p : Nat.PrimeNat.Prime (p : ℕ) : Prop`Nat.Prime p` means that `p` is a prime number, that is, a natural number
at least 2 whose only divisors are `p` and `1`.
The theorem `Nat.prime_def` witnesses this description of a prime number.  pℕ)
  (hp55 ≤ p : 5 ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. pℕ)
  (Ha ^ p + b ^ p = c ^ p : aℤ ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. pℕ +HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `+` in identifiers is `add`. bℤ ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. pℕ =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. cℤ ^HPow.hPow.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HPow α β γ] : α → β → γ`a ^ b` computes `a` to the power of `b`.
The meaning of this notation is type-dependent. 

Conventions for notations in identifiers:

 * The recommended spelling of `^` in identifiers is `pow`. pℕ) :
  NonemptyNonempty.{u} (α : Sort u) : Prop`Nonempty α` is a typeclass that says that `α` is not an empty type,
that is, there exists an element in the type. It differs from `Inhabited α`
in that `Nonempty α` is a `Prop`, which means that it does not actually carry
an element of `α`, only a proof that *there exists* such an element.
Given `Nonempty α`, you can construct an element of `α` *nonconstructively*
using `Classical.choice`.
 FreyPackageFreyPackage : TypeA *Frey Package* is a 4-tuple (a,b,c,p) of integers
satisfying $a^p+b^p=c^p$ and some other inequalities
and congruences. These facts guarantee that all of
the all the results in section 4.1 of Serre's paper [serre]
apply to the curve $Y^2=X(X-a^p)(X+b^p).$

theorem Mazur_FreyMazur_Frey (P : FreyPackage) : (P.freyCurve.galoisRep P.p ⋯).IsIrreducible (PFreyPackage : FreyPackageFreyPackage : TypeA *Frey Package* is a 4-tuple (a,b,c,p) of integers
satisfying $a^p+b^p=c^p$ and some other inequalities
and congruences. These facts guarantee that all of
the all the results in section 4.1 of Serre's paper [serre]
apply to the curve $Y^2=X(X-a^p)(X+b^p).$
) :
  (PFreyPackage.freyCurveFreyPackage.freyCurve (P : FreyPackage) : WeierstrassCurve ℚThe elliptic curve over `ℚ` associated to a Frey package. The conditions imposed
upon a Frey package guarantee that the running hypotheses in
Section 4.1 of [Serre] all hold. We put the curve into the form where the
equation is semistable at 2, rather than the usual `Y^2=X(X-a^p)(X+b^p)` form.
The change of variables is `X=4x` and `Y=8y+4x`, and then divide through by 64. .galoisRepWeierstrassCurve.galoisRep.{u} {K : Type u} [Field K] (E : WeierstrassCurve K) [E.IsElliptic] [DecidableEq K]
  [DecidableEq (AlgebraicClosure K)] (n : ℕ) (hn : 0 < n) :
  GaloisRep K (ZMod n) ((E.map (algebraMap K (AlgebraicClosure K))).n_torsion n)The continuous Galois representation associated to an elliptic curve over a field.  PFreyPackage.pFreyPackage.p (self : FreyPackage) : ℕThe prime number `p` in the Frey package. 
      ⋯).IsIrreducibleGaloisRep.IsIrreducible.{uK, u_4, u_7} {K : Type uK} [Field K] {M : Type u_4} [AddCommGroup M] {k : Type u_7} [Field k]
  [TopologicalSpace k] [Module k M] (ρ : GaloisRep K k M) : PropIrreducibility of a Galois representation over a field. 

theorem Wiles_FreyWiles_Frey (P : FreyPackage) : ¬(P.freyCurve.galoisRep P.p ⋯).IsIrreducible (PFreyPackage : FreyPackageFreyPackage : TypeA *Frey Package* is a 4-tuple (a,b,c,p) of integers
satisfying $a^p+b^p=c^p$ and some other inequalities
and congruences. These facts guarantee that all of
the all the results in section 4.1 of Serre's paper [serre]
apply to the curve $Y^2=X(X-a^p)(X+b^p).$
) :
  ¬Not (a : Prop) : Prop`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.(PFreyPackage.freyCurveFreyPackage.freyCurve (P : FreyPackage) : WeierstrassCurve ℚThe elliptic curve over `ℚ` associated to a Frey package. The conditions imposed
upon a Frey package guarantee that the running hypotheses in
Section 4.1 of [Serre] all hold. We put the curve into the form where the
equation is semistable at 2, rather than the usual `Y^2=X(X-a^p)(X+b^p)` form.
The change of variables is `X=4x` and `Y=8y+4x`, and then divide through by 64. .galoisRepWeierstrassCurve.galoisRep.{u} {K : Type u} [Field K] (E : WeierstrassCurve K) [E.IsElliptic] [DecidableEq K]
  [DecidableEq (AlgebraicClosure K)] (n : ℕ) (hn : 0 < n) :
  GaloisRep K (ZMod n) ((E.map (algebraMap K (AlgebraicClosure K))).n_torsion n)The continuous Galois representation associated to an elliptic curve over a field.  PFreyPackage.pFreyPackage.p (self : FreyPackage) : ℕThe prime number `p` in the Frey package. 
        ⋯).IsIrreducibleGaloisRep.IsIrreducible.{uK, u_4, u_7} {K : Type uK} [Field K] {M : Type u_4} [AddCommGroup M] {k : Type u_7} [Field k]
  [TopologicalSpace k] [Module k M] (ρ : GaloisRep K k M) : PropIrreducibility of a Galois representation over a field. 

theorem FreyPackage.falseFreyPackage.false (P : FreyPackage) : FalseThere is no Frey package. This profound result is proved using
work of Mazur and Wiles/Ribet to rule out all possibilities for the
$p$-torsion in the corresponding Frey curve.  (PFreyPackage : FreyPackageFreyPackage : TypeA *Frey Package* is a 4-tuple (a,b,c,p) of integers
satisfying $a^p+b^p=c^p$ and some other inequalities
and congruences. These facts guarantee that all of
the all the results in section 4.1 of Serre's paper [serre]
apply to the curve $Y^2=X(X-a^p)(X+b^p).$
) :
  FalseFalse : Prop`False` is the empty proposition. Thus, it has no introduction rules.
It represents a contradiction. `False` elimination rule, `False.rec`,
expresses the fact that anything follows from a contradiction.
This rule is sometimes called ex falso (short for ex falso sequitur quodlibet),
or the principle of explosion.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)

theorem Wiles_Taylor_WilesWiles_Taylor_Wiles : FermatLastTheoremFermat's Last Theorem is true  : FermatLastTheoremFermatLastTheorem : PropStatement of Fermat's Last Theorem: `a ^ n + b ^ n = c ^ n` has no nontrivial natural solution
when `n ≥ 3`.

This is now a theorem of Wiles and Taylor--Wiles; see
https://github.com/ImperialCollegeLondon/FLT for an ongoing Lean formalisation of
a proof.