simp only [_root_.map_add, map_intCast, _root_.map_mul, AlgHom.coe_coe, zpow_neg, map_units_inv,
  add_right_inj, mul_eq_mul_left_iff, Int.cast_eq_zero]
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)))
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) ((algebraMap (𝓞 K) K) ↑(hζ.unit' ^ i)) = ((algebraMap (𝓞 K) K) ↑(hζ.unit' ^ i))⁻¹ ∨ y = 0