obtain ⟨a, ha⟩ := exists_int_sub_pow_prime_dvd p α
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
⊢ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p) ∈ Ideal.span {↑↑p}
case 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 : ℤ
ha : α ^ ↑p - ↑a ∈ Ideal.span {↑↑p}
⊢ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p) ∈ Ideal.span {↑↑p}