refine' ⟨(pb.basis.repr x) ⟨0, pb.dim_pos⟩, _⟩
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
⊢ ∃ n, x ≡ ↑n [SMOD span {pb.gen}]
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]