Update Mathlib/Analysis/ODE/DiscreteGronwall.lean

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

Author: dennj

Mathlib/Analysis/ODE/DiscreteGronwall.lean

@@ -125,27 +125,12 @@ theorem discrete_gronwall {n₀ : ℕ} (hun₀ : 0 ≤ u n₀)
 /-- Discrete Grönwall inequality: uniform bound over an interval.
 
 Provides a uniform bound for all `n ∈ [n₀, n₁)`. -/
-theorem discrete_gronwall_Ico
-    {n₀ n₁ : ℕ}
-    (hun₀ : 0 ≤ u n₀)
+theorem discrete_gronwall_Ico {n₀ n₁ : ℕ} (hun₀ : 0 ≤ u n₀)
     (hu : ∀ n ≥ n₀, u (n + 1) ≤ (1 + c n) * u n + b n)
-    (hc : ∀ n ≥ n₀, 0 ≤ c n)
-    (hb : ∀ n ≥ n₀, 0 ≤ b n) :
-    ∀ n ∈ Ico n₀ n₁,
-      u n ≤ (u n₀ + ∑ k ∈ Ico n₀ n₁, b k) * exp (∑ i ∈ Ico n₀ n₁, c i) := by
-  intro n hn
-  simp only [mem_Ico] at hn
-  have hsum_b : ∑ k ∈ Ico n₀ n, b k ≤ ∑ k ∈ Ico n₀ n₁, b k :=
-    sum_le_sum_of_subset_of_nonneg (Ico_subset_Ico_right (by omega))
-      fun i hi _ ↦ by simp only [mem_Ico] at hi; exact hb i (by omega)
-  have hsum_c : ∑ i ∈ Ico n₀ n, c i ≤ ∑ i ∈ Ico n₀ n₁, c i :=
-    sum_le_sum_of_subset_of_nonneg (Ico_subset_Ico_right (by omega))
-      fun i hi _ ↦ by simp only [mem_Ico] at hi; exact hc i (by omega)
-  have hsum_b₁_nonneg : 0 ≤ ∑ k ∈ Ico n₀ n₁, b k :=
-    sum_nonneg fun i hi ↦ by simp only [mem_Ico] at hi; exact hb i (by omega)
+    (hc : ∀ n ≥ n₀, 0 ≤ c n) (hb : ∀ n ≥ n₀, 0 ≤ b n) ⦃n : ℕ⦄ (hn : n ∈ Ico n₀ n₁) :
+    u n ≤ (u n₀ + ∑ k ∈ Ico n₀ n₁, b k) * exp (∑ i ∈ Ico n₀ n₁, c i) := by
+  have hsum_b₁_nonneg : 0 ≤ ∑ k ∈ Ico n₀ n₁, b k := sum_nonneg <| by grind
   calc u n
     _ ≤ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * exp (∑ i ∈ Ico n₀ n, c i) :=
-        discrete_gronwall hun₀ hu hc hb n hn.1
-    _ ≤ (u n₀ + ∑ k ∈ Ico n₀ n₁, b k) * exp (∑ i ∈ Ico n₀ n₁, c i) :=
-        mul_le_mul (by linarith) (exp_le_exp_of_le hsum_c) (by positivity)
-          (add_nonneg hun₀ hsum_b₁_nonneg)
+      discrete_gronwall hun₀ hu hc hb (by grind)
+    _ ≤ (u n₀ + ∑ k ∈ Ico n₀ n₁, b k) * exp (∑ i ∈ Ico n₀ n₁, c i) := by gcongr <;> grind