rw [← map_pow, galConj_zeta_runity_pow hζ, inv_pow]
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
u : (𝓞 K)ˣ
hp : (↑p).Prime
this✝ :
  ↑((Units.map ↑(algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1}))) ((unitGalConj K p) u))⁻¹ =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)⁻¹
this : Fact (↑p).Prime
a : 𝓞 K ≃ₗ[ℤ] Fin hζ.integralPowerBasis'.dim →₀ ℤ := hζ.integralPowerBasis'.basis.repr
φn : ℕ := hζ.integralPowerBasis'.dim
hu : ∑ x : Fin hζ.integralPowerBasis'.dim, (hζ.integralPowerBasis'.basis.repr ↑u) x • hζ.toInteger ^ ↑x = ↑u
hu' : ∑ x : Fin φn, (a ↑u) x • (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ↑((unitGalConj K p) u)
x : Fin φn
⊢ (galConj K p) ζ ^ ↑x = (ζ ^ ↑x)⁻¹
no goals