simp only [Fin.val_mk, _root_.pow_zero, zsmul_eq_mul] at H
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
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H : ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 + ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, ↑((pb.basis.repr x) x_1) * pb.gen ^ ↑x_1 = x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]