have :
  ∀ i : (univ : Finset (Fin pb.dim)).erase ⟨0, pb.dim_pos⟩,
    ↑((pb.basis.repr x) i) * pb.gen ^ ((i : Fin pb.dim) : ℕ) =
      ↑((pb.basis.repr x) i) * pb.gen ^ (i : ℕ).pred.succ := by
  rintro ⟨i, hi⟩
  congr 1
  rw [succ_pred_eq_of_pos]
  rw [Subtype.coe_mk]
  refine' Nat.pos_of_ne_zero fun h => _
  cases' i with i₁ hi₁
  simp only [Subtype.coe_mk] at h
  simp only [mem_univ, not_true, mem_erase, ne_eq, Fin.mk.injEq, and_true] at hi
  exact hi 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
⊢ 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
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}]