rw [minpoly_polyRoot' hp hζ u hcong hu]
case isUnramifiedAt.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
⊢ (map (Ideal.Quotient.mk I) (minpoly (𝓞 K) ↑α)).Separable
case isUnramifiedAt.refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
u : (𝓞 K)ˣ
hcong : (↑hζ.unit' - 1) ^ ↑p ∣ ↑u - 1
hu : ∀ (v : K), v ^ ↑p ≠ (algebraMap (𝓞 K) K) ↑u
L : Type u_2
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsSplittingField K L (X ^ ↑p - C ((algebraMap (𝓞 K) K) ↑u))
α : 𝓞 L := polyRoot hp hζ u hcong (rootOfSplitsXPowSubC ⋯ ((algebraMap (𝓞 K) K) ↑u) L) ⋯ 0
this : FiniteDimensional K L
hα : Algebra.adjoin K {↑α} = ⊤
I : Ideal (𝓞 K)
hI : I.IsPrime
hIbot : I ≠ ⊥
⊢ (map (Ideal.Quotient.mk I) (poly hp hζ u hcong)).Separable