rw [← mul_sum] at H
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 +
      ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), pb.gen * (↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred) =
    x
⊢ 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 +
      pb.gen * ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred =
    x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]