rw [← zpow_natCast, ← zpow_sub₀ (hζ'.ne_zero hpri.out.ne_zero), hζ'.zpow_eq_one_iff_dvd]
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ (algebraMap (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)) (CyclotomicField ⟨p, ⋯⟩ ℚ)) ζ ^ (2 * k % ↑p).natAbs / ζ' ^ (2 * k) = 1
case h.e'_4.h.e'_6.h.e'_6.e_a.e_a.h
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ↑↑⟨p, ⋯⟩ ∣ ↑(2 * k % ↑p).natAbs - 2 * k