have : ∀ x : Fin φn, intGal ((galConj K p)) (⟨ζ, hζ.isIntegral p.pos⟩ ^ (x : ℕ)) =
    ⟨ζ⁻¹, hζ.inv.isIntegral p.pos⟩ ^ (x : ℕ) := by
  intro x
  ext
  simp only [map_pow, intGal_apply_coe, RingOfIntegers.map_mk, AlgHom.coe_coe, inv_pow]
  rw [← map_pow, galConj_zeta_runity_pow hζ, inv_pow]
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)
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)
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)
this : ∀ (x : Fin φn), (intGal ↑(galConj K p)) (⟨ζ, ⋯⟩ ^ ↑x) = ⟨ζ⁻¹, ⋯⟩ ^ ↑x
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)