have := stuff hp hreg hζ e hy hz η₁ hη₁ η₂ hη₂
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
u₃ : (𝓞 K)ˣ
hu₃ : π * ↑u₃ = ↑η₂ - ↑η₁
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
case intro.intro.intro
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
this✝ : Fact (↑p).Prime := hpri
η₁ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit', ⋯⟩
η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) } := ⟨↑η₀ * ↑hζ.unit' * ↑hζ.unit', ⋯⟩
hη₁ : η₁ ≠ η₀
hη₂ : η₂ ≠ η₀
hη : η₂ ≠ η₁
u₁ : (𝓞 K)ˣ
hu₁ : π * ↑u₁ = ↑η₂ - ↑η₀
u₂ : (𝓞 K)ˣ
hu₂ : π * ↑u₂ = ↑η₀ - ↑η₁
u₃ : (𝓞 K)ˣ
hu₃ : π * ↑u₃ = ↑η₂ - ↑η₁
this :
  (↑η₂ - ↑η₀) * ↑(ε η₁ hη₁) * (α η₁ hη₁ * β η₂ hη₂) ^ ↑p + (↑η₀ - ↑η₁) * ↑(ε η₂ hη₂) * (α η₂ hη₂ * β η₁ hη₁) ^ ↑p =
    (↑η₂ - ↑η₁) * (π ^ m * (β η₁ hη₁ * β η₂ hη₂)) ^ ↑p
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p