obtain ⟨t, _, rfl⟩ := (zeta_spec p ℚ K).eq_pow_of_pow_eq_one hζ.pow_eq_one p.pos
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
⊢ (galConj K p) ζ = ζ⁻¹
case intro.intro
K : Type u_1
p : ℕ+
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
t : ℕ
left✝ : t < ↑p
hζ : IsPrimitiveRoot (zeta p ℚ K ^ t) ↑p
⊢ (galConj K p) (zeta p ℚ K ^ t) = (zeta p ℚ K ^ t)⁻¹