∀ {K : Type u_1} {Γ₀ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀)
  [inst_2 : IsDiscreteValuationRing ↥v.integer] {ϖ : ↥v.integer},
  Irreducible ϖ → ∀ (n : ℕ), ↑(IsLocalRing.maximalIdeal ↥v.integer ^ n) = {y | v ↑y ≤ v ↑ϖ ^ n}