∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {I : Ideal R} (h : Submodule.IsPrincipal I),
  I ≠ ⊥ →
    ∀ (n : ℕ),
      I = Ideal.span {⋯.choose} →
        ∀ (hϖ : ⋯.choose ^ n ∈ I ^ n),
          I = ((I • ⊤).mkQ ∘ₗ LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ⋯.choose ^ n) ⋯).ker