rw [SModEq.sub_mem, mul_one, add_sub_cancel_left, mul_comm, mem_span_singleton']
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
⊢ ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      pb.gen * ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred ≡
    ↑((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
⊢ ∃ a, a * pb.gen = (∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred) * pb.gen