simp only [galConj, Units.coe_neg_one, autEquivPow_symm_apply, AlgEquiv.coe_algHom,
  PowerBasis.equivOfMinpoly_apply]
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑p
hζ : IsPrimitiveRoot (zeta p ℚ K) ↑p := zeta_spec p ℚ K
⊢ (galConj K p) (zeta p ℚ K) = (zeta p ℚ K)⁻¹
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ ↑p
hζ : IsPrimitiveRoot (zeta p ℚ K) ↑p := zeta_spec p ℚ K
⊢ ((IsPrimitiveRoot.powerBasis ℚ ⋯).lift (IsPrimitiveRoot.powerBasis ℚ ⋯).gen ⋯) (zeta p ℚ K) = (zeta p ℚ K)⁻¹