Update Mathlib/Analysis/ODE/DiscreteGronwall.lean

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

Author: dennj

Mathlib/Analysis/ODE/DiscreteGronwall.lean

@@ -111,16 +111,16 @@ theorem discrete_gronwall {n₀ : ℕ} (hun₀ : 0 ≤ u n₀)
   calc u n
     _ ≤ u n₀ * ∏ i ∈ Ico n₀ n, (1 + c i) +
           ∑ k ∈ Ico n₀ n, b k * ∏ i ∈ Ico (k + 1) n, (1 + c i) :=
-        discrete_gronwall_prod_general hu (fun m hm => by linarith [hc m hm]) n hn
+        discrete_gronwall_prod_general hu (by grind) hn
     _ ≤ u n₀ * ∏ i ∈ Ico n₀ n, (1 + c i) +
           ∑ k ∈ Ico n₀ n, b k * ∏ i ∈ Ico n₀ n, (1 + c i) := by
         gcongr with j hj
-        · simp only [mem_Ico] at hj; exact hb j (by omega)
-        · exact prod_one_add_Ico_mono hc j hj
+        · grind
+        · exact prod_one_add_Ico_mono hc hj
     _ = (u n₀ + ∑ k ∈ Ico n₀ n, b k) * ∏ i ∈ Ico n₀ n, (1 + c i) := by rw [add_mul, sum_mul]
-    _ ≤ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * exp (∑ i ∈ Ico n₀ n, c i) :=
-        mul_le_mul_of_nonneg_left hprod_le_exp (add_nonneg hun₀
-          (sum_nonneg fun i hi ↦ by simp only [mem_Ico] at hi; exact hb i (by omega)))
+    _ ≤ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * exp (∑ i ∈ Ico n₀ n, c i) := by
+        gcongr
+        exact add_nonneg hun₀ (sum_nonneg <| by grind)
 
 /-- Discrete Grönwall inequality: uniform bound over an interval.