rw [sub_mul, div_zeta_sub_one_mul_zeta_sub_one, div_zeta_sub_one_mul_zeta_sub_one]
case h.e'_4
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) }
hη : η₁ ≠ η₂
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ (div_zeta_sub_one hp hζ e η₁ - div_zeta_sub_one hp hζ e η₂) * π = y * (↑η₁ - ↑η₂)
case h.e'_4
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) }
hη : η₁ ≠ η₂
this : NumberField K := IsCyclotomicExtension.numberField {p} ℚ K
⊢ x + y * ↑η₁ - (x + y * ↑η₂) = y * (↑η₁ - ↑η₂)