-- Module: Mathlib.NumberTheory.FLT.Three
Goal:
let let₁ let₂ let₃ : FermatLastTheoremFor 3
let₄ :
  let K := CyclotomicField 3 ℚ;
  ∀ (this : NumberField K), FermatLastTheoremFor 3
let₅ :
  let K := CyclotomicField 3 ℚ;
  let hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := ⋯;
  ∀ (this : NumberField K), FermatLastTheoremForThreeGen hζ
let₆ :
  let K := CyclotomicField 3 ℚ;
  let hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := ⋯;
  ∀ (this : NumberField K) (a b c : NumberField.RingOfIntegers K) (u : (NumberField.RingOfIntegers K)ˣ) (hc : c ≠ 0)
    (ha : ¬hζ.toInteger - 1 ∣ a) (hb : ¬hζ.toInteger - 1 ∣ b) (hcdvd : hζ.toInteger - 1 ∣ c) (coprime : IsCoprime a b)
    (H :
      HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = (↑u : NumberField.RingOfIntegers K) * HPow.hPow (β := ℕ) c 3),
    False
let₇ :
  let K := CyclotomicField 3 ℚ;
  let hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := ⋯;
  ∀ (this : NumberField K) (a b c : NumberField.RingOfIntegers K) (u : (NumberField.RingOfIntegers K)ˣ) (hc : c ≠ 0)
    (ha : ¬hζ.toInteger - 1 ∣ a) (hb : ¬hζ.toInteger - 1 ∣ b) (hcdvd : hζ.toInteger - 1 ∣ c) (coprime : IsCoprime a b)
    (H :
      HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = (↑u : NumberField.RingOfIntegers K) * HPow.hPow (β := ℕ) c 3),
    False
let₈ :
  let K := CyclotomicField 3 ℚ;
  let hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := ⋯;
  ∀ (this : NumberField K) (a b c : NumberField.RingOfIntegers K) (u : (NumberField.RingOfIntegers K)ˣ) (hc : c ≠ 0)
    (ha : ¬hζ.toInteger - 1 ∣ a) (hb : ¬hζ.toInteger - 1 ∣ b) (hcdvd : hζ.toInteger - 1 ∣ c) (coprime : IsCoprime a b)
    (H : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = (↑u : NumberField.RingOfIntegers K) * HPow.hPow (β := ℕ) c 3)
    (S : FermatLastTheoremForThreeGen.Solution hζ), False
let₉ :
  let K := CyclotomicField 3 ℚ;
  let hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := ⋯;
  ∀ (this : NumberField K) (a b c : NumberField.RingOfIntegers K) (u : (NumberField.RingOfIntegers K)ˣ) (hc : c ≠ 0)
    (ha : ¬hζ.toInteger - 1 ∣ a) (hb : ¬hζ.toInteger - 1 ∣ b) (hcdvd : hζ.toInteger - 1 ∣ c) (coprime : IsCoprime a b)
    (H : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = (↑u : NumberField.RingOfIntegers K) * HPow.hPow (β := ℕ) c 3)
    (S Smin : FermatLastTheoremForThreeGen.Solution hζ) (hSmin : Smin.isMinimal), False
let₁₀ :
  let K := CyclotomicField 3 ℚ;
  let hζ : IsPrimitiveRoot (IsCyclotomicExtension.zeta 3 ℚ K) 3 := ⋯;
  ∀ (this : NumberField K) (a b c : NumberField.RingOfIntegers K) (u : (NumberField.RingOfIntegers K)ˣ) (hc : c ≠ 0)
    (ha : ¬hζ.toInteger - 1 ∣ a) (hb : ¬hζ.toInteger - 1 ∣ b) (hcdvd : hζ.toInteger - 1 ∣ c) (coprime : IsCoprime a b)
    (H : HPow.hPow (β := ℕ) a 3 + HPow.hPow (β := ℕ) b 3 = (↑u : NumberField.RingOfIntegers K) * HPow.hPow (β := ℕ) c 3)
    (S Smin : FermatLastTheoremForThreeGen.Solution hζ) (hSmin : Smin.isMinimal)
    (Sfin : FermatLastTheoremForThreeGen.Solution hζ) (hSfin : Sfin.multiplicity < Smin.multiplicity), False
⊢ FermatLastTheoremFor 3

Tactic:
classical
  let K := CyclotomicField 3 ℚ
  let hζ := IsCyclotomicExtension.zeta_spec 3 ℚ K
  have : NumberField K := IsCyclotomicExtension.numberField {3} ℚ _
  apply FermatLastTheoremForThree_of_FermatLastTheoremThreeGen hζ
  intro a b c u hc ha hb hcdvd coprime H
  let S' : FermatLastTheoremForThreeGen.Solution' hζ :=
  { a := a
    b := b
    c := c
    u := u
    ha := ha
    hb := hb
    hc := hc
    coprime := coprime
    hcdvd := hcdvd
    H := H }
  obtain ⟨S, -⟩ := FermatLastTheoremForThreeGen.exists_Solution_of_Solution' S'
  obtain ⟨Smin, hSmin⟩ := S.exists_minimal
  obtain ⟨Sfin, hSfin⟩ := Smin.exists_Solution_multiplicity_lt
  linarith [hSmin Sfin]