rw [hγ, _root_.map_add, _root_.map_mul, map_natCast, map_intCast, add_sub_add_right_eq_sub,
  ← mul_sub]
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
γ : 𝓞 K
hγ : α ^ ↑p = ↑↑p * γ + ↑a
⊢ ↑↑p ∣ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p)
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
γ : 𝓞 K
hγ : α ^ ↑p = ↑↑p * γ + ↑a
⊢ ↑↑p ∣ ↑↑p * (γ - (intGal ↑(galConj K p)) γ)