chore(Algebra/Module/ZLattice/Summable): automated extraction from leanprover-community#39646 (leanprover-community#40752)

Author: Yaël Dillies <yael.dillies@gmail.com>

Co-authored-by: YaelDillies <14090593+YaelDillies@users.noreply.github.com>

Author: 2 people

Mathlib/Algebra/Module/ZLattice/Summable.lean

@@ -147,9 +147,7 @@ lemma sum_piFinset_Icc_rpow_le {ι : Type*} [Fintype ι] [DecidableEq ι]
         rw [← Real.rpow_natCast, ← Real.rpow_add (by positivity), Nat.cast_sub hd]
         norm_cast
     _ ≤ 2 * d * 3 ^ (d - 1) * ε ^ r * ∑ k ∈ range (n + 1), (k : ℝ) ^ (d - 1 + r) := by
-        gcongr
-        rw [Finset.sum_range_succ', le_add_iff_nonneg_right]
-        positivity
+        grw [Finset.sum_range_succ', Nat.cast_zero, ← Real.rpow_nonneg le_rfl, add_zero]
     _ ≤ 2 * d * 3 ^ (d - 1) * ε ^ r * ∑' k : ℕ, (k : ℝ) ^ (d - 1 + r) := by
         gcongr
         refine Summable.sum_le_tsum _ (fun _ _ ↦ by positivity) (Real.summable_nat_rpow.mpr ?_)