rw [Subtype.coe_mk]
case mk.e_a
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
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ 0 < ↑↑⟨i, hi⟩
case mk.e_a
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
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ 0 < ↑i