rw [Units.val_mul, map_mul, ← this, Units.mul_inv_eq_one, Units.coe_map , MonoidHom.coe_coe]
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)⁻¹
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑(u * ((unitGalConj K p) u)⁻¹) = 1
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)⁻¹
⊢ (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑u =
    (algebraMap (𝓞 K) (𝓞 K ⧸ Ideal.span {↑hζ.unit' - 1})) ↑((unitGalConj K p) u)