rw [PowerBasis.coe_basis, ← insert_erase (mem_univ (⟨0, pb.dim_pos⟩ : Fin pb.dim)), sum_insert] at H
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H : ∑ i : Fin pb.dim, (pb.basis.repr x) i • pb.basis i = x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]

K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H : ∑ i ∈ insert ⟨0, ⋯⟩ (univ.erase ⟨0, ⋯⟩), (pb.basis.repr x) i • (fun i => pb.gen ^ ↑i) i = x
⊢ ⟨0, ⋯⟩ ∉ univ.erase ⟨0, ⋯⟩