Has Sum geometric succ

theorem hasSum_geometric_succ {x : k} (hx : valuation k x < 1) :    HasSum (fun j : ℕ ↦ x ^ (j + 1)) (x / (1 - x)) := by  have hx1 : x ≠ 1 := by    rintro rfl    simp at hx  have hx1' : x - 1 ≠ 0 := sub_ne_zero.mpr hx1  have h1x : (1 : k) - x ≠ 0 := sub_ne_zero.mpr (Ne.symm hx1)  obtain ⟨S, hS⟩ : Summable fun j : ℕ ↦ x ^ (j + 1) :=    summable_of_valuation_le_pow hx (fun j ↦ j + 1)      (fun N ↦ (Set.finite_Iio N).subset fun j hj ↦ Set.mem_Iio.mpr (Nat.lt_of_succ_lt hj))      fun j ↦ le_of_eq (map_pow _ _ _)  suffices hlim : Filter.Tendsto (fun n : ℕ ↦ ∑ j ∈ Finset.range n, x ^ (j + 1))      Filter.atTop (𝓝 (x / (1 - x))) from    tendsto_nhds_unique hS.tendsto_sum_nat hlim ▸ hS  have hps : ∀ n : ℕ, ∑ j ∈ Finset.range n, x ^ (j + 1) = x * ((x ^ n - 1) / (x - 1)) := by    intro n    rw [← geom_sum_eq hx1 n, Finset.mul_sum]    exact Finset.sum_congr rfl fun j _ ↦ by ring  simp only [hps]  have h := (((tendsto_pow_nhds_zero hx).sub_const 1).div_const (x - 1)).const_mul x  convert h using 2  rw [zero_sub]  field_simp  ring