rw [intGal_apply_coe]
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ ↑((intGal ↑(galConj K p)) (↑x + ↑y * ↑(hζ.unit' ^ i))) = ↑(↑x + ↑y * ↑(hζ.unit' ^ (-i)))
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ ↑(galConj K p) ↑(↑x + ↑y * ↑(hζ.unit' ^ i)) = ↑(↑x + ↑y * ↑(hζ.unit' ^ (-i)))