have hμ' : algebraMap (𝓞 K) (𝓞 K ⧸ I) ((IsPrimitiveRoot.unit' hζ : 𝓞 K) ^ n) = -1 := by
  rw [← neg_eq_iff_eq_neg, ← map_neg, ← Units.val_pow_eq_pow_val, ← Units.val_neg, ← H]
  apply unit_inv_conj_not_neg_zeta_runity_aux hζ u hp
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
⊢ False
p : ℕ+
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {p} ℚ K
h : p ≠ 2
u : (𝓞 K)ˣ
n : ℕ
hp : (↑p).Prime
H : u * ((unitGalConj K p) u)⁻¹ = -hζ.unit' ^ n
hμ : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = 1
hμ' : (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) (↑hζ.unit' ^ n) = -1
⊢ False