∀ (p k : ℕ) [hp : Fact (Nat.Prime p)] (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K], (Ideal.span {↑p}).inertiaDegIn (NumberField.RingOfIntegers K) = 1