∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : FermatLastTheoremForThreeGen.Solution' hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K],
  ∃ a' b',
    a' ^ 3 + b' ^ 3 = ↑S'.u * S'.c ^ 3 ∧
      IsCoprime a' b' ∧ ¬hζ.toInteger - 1 ∣ a' ∧ ¬hζ.toInteger - 1 ∣ b' ∧ (hζ.toInteger - 1) ^ 2 ∣ a' + b'