rw [mul_pow, ← pow_mul, mul_comm (ε₃ : 𝓞 K), mul_assoc, ← Nat.sub_add_cancel this,
  add_comm _ (p - 1 : ℕ), pow_add, mul_assoc] at e'
case hcong.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) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * (π ^ m * z') ^ ↑p
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n
case hcong.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) }
x' y' z' : 𝓞 K
ε₁ ε₂ ε₃ : (𝓞 K)ˣ
hx' : ¬π ∣ x'
hy' : ¬π ∣ y'
hz' : ¬π ∣ z'
e' : ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = π ^ (↑p - 1) * (π ^ (m * ↑p - (↑p - 1)) * (z' ^ ↑p * ↑ε₃))
this : ↑p - 1 ≤ m * ↑p
u : (𝓞 K)ˣ
hu : ↑↑p * ↑u = π ^ (↑p - 1)
⊢ ∃ n, ↑↑p ∣ ↑(ε₁ / ε₂) - ↑n