have hα : Algebra.adjoin K {(α : L)} = ⊤ := by
  rw [eq_top_iff, ← Algebra.adjoin_root_eq_top_of_isSplittingField
    ⟨ζ, (mem_primitiveRoots p.pos).mpr hζ⟩ (X_pow_sub_C_irreducible_of_prime hpri.out hu)
    (rootOfSplitsXPowSubC_pow p.pos (u : K) L), Algebra.adjoin_le_iff, Set.singleton_subset_iff]
  exact mem_adjoin_polyRoot hp hζ u hcong _ _ 0
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
⊢ IsUnramified (𝓞 K) (𝓞 L)
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 {↑α} = ⊤
⊢ IsUnramified (𝓞 K) (𝓞 L)