Summable of valuation le pow

theorem summable_of_valuation_le_pow {ι : Type*} {q : k} (hq : valuation k q < 1)    {f : ι → k} (e : ι → ℕ) (he : ∀ N, {i | e i < N}.Finite)    (hf : ∀ i, valuation k (f i) ≤ valuation k q ^ e i) : Summable f := by  -- `Summable` only sees the topology, but the completeness criterion below is stated for  -- uniform spaces: equip `k` with its canonical uniformity  let : UniformSpace k := IsTopologicalAddGroup.rightUniformSpace k  have : IsUniformAddGroup k := isUniformAddGroup_of_addCommGroup  apply NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero  rw [(IsValuativeTopology.hasBasis_nhds (0 : k)).tendsto_right_iff]  intro γ _  obtain ⟨N, hN⟩ := exists_pow_valuation_lt q hq γ  rw [Filter.eventually_cofinite]  refine (he N).subset fun i hi ↦ ?_  simp only [Set.mem_setOf_eq, sub_zero] at hi  exact lt_of_not_ge fun hge ↦    hi (lt_of_le_of_lt ((hf i).trans (pow_le_pow_right_of_le_one' hq.le hge)) hN)