have hη₂ : η₂ ≠ η₀ := by
  rw [← Subtype.coe_injective.ne_iff]
  show (η₀ * hζ.unit' * hζ.unit' : 𝓞 K) ≠ η₀
  rw [Ne, mul_assoc, ← pow_two, mul_right_eq_self₀, not_or]
  exact ⟨hζ.unit'_coe.pow_ne_one_of_pos_of_lt zero_lt_two
    (hpri.out.two_le.lt_or_eq.resolve_right (PNat.coe_injective.ne hp.symm)),
    ne_zero_of_mem_nthRootsFinset (η₀ : _).prop⟩
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η₁ : η₁ ≠ η₀
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
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η₂ : η₂ ≠ η₀
⊢ ∃ x' y' z' ε₁ ε₂ ε₃, ¬π ∣ x' ∧ ¬π ∣ y' ∧ ¬π ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p