awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.ODE.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
hγ : IsIntegralCurve γ v
⊢ Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] γ

Tactic:
continuous_iff_continuousAt.mpr (hγ.isIntegralCurveAt · |>.continuousAt)

Premises used: Iff.mpr, IsIntegralCurve.isIntegralCurveAt, IsIntegralCurveAt.continuousAt, continuous_iff_continuousAt
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n : ℕ
⊢ u n₀ ≤ u n₀ * ∏ i ∈ Ico n₀ n₀, c i + ∑ k ∈ Ico n₀ n₀, b k * ∏ i ∈ Ico (k + 1) n₀, c i

Tactic:
simp
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
⊢ 0 ≤ c k

Tactic:
have hck : 0 ≤ c k := hc k hk
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
rw :
  ∑ i ∈ Ico n₀ k, c k * (b i * ∏ i ∈ Ico (i + 1) k, c i) + b k =
    ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) (k + 1), c i + b k
⊢ c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k =
    ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i

Tactic:
rw [sum_Ico_succ_top hk, mul_sum, Ico_self, prod_empty, mul_one]

Premises used: Finset.mul_sum, Finset.prod_empty, Finset.Ico_self, Finset.sum_Ico_succ_top, mul_one
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
⊢ ∑ i ∈ Ico n₀ k, c k * (b i * ∏ i ∈ Ico (i + 1) k, c i) + b k =
    ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) (k + 1), c i + b k

Tactic:
congr_arg (· + b k) (sum_congr rfl fun j hj ↦ ?_)

Premises used: congr_arg, HAdd.hAdd, Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
refine : ∀ (j : ℕ) (hj : j ∈ Ico n₀ k), c k * (b j * ∏ i ∈ Ico (j + 1) k, c i) = b j * ∏ i ∈ Ico (j + 1) (k + 1), c i
⊢ ∑ i ∈ Ico n₀ k, c k * (b i * ∏ i ∈ Ico (i + 1) k, c i) + b k =
    ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) (k + 1), c i + b k

Tactic:
refine congr_arg (· + b k) (sum_congr rfl fun j hj ↦ ?_)

Premises used: congr_arg, HAdd.hAdd, Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
j : ℕ
hj : j ∈ Ico n₀ k
⊢ n₀ ≤ j ∧ j < k

Tactic:
have := mem_Ico.mp hj
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
j : ℕ
hj : j ∈ Ico n₀ k
this : n₀ ≤ j ∧ j < k
⊢ j + 1 ≤ k

Tactic:
omega
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
j : ℕ
hj : j ∈ Ico n₀ k
rw : c k * (b j * ∏ i ∈ Ico (j + 1) k, c i) = b j * ((∏ k ∈ Ico (j + 1) k, c k) * c k)
⊢ c k * (b j * ∏ i ∈ Ico (j + 1) k, c i) = b j * ∏ i ∈ Ico (j + 1) (k + 1), c i

Tactic:
rw [prod_Ico_succ_top (by have := mem_Ico.mp hj; omega)]

Premises used: Finset.prod_Ico_succ_top
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
j : ℕ
hj : j ∈ Ico n₀ k
⊢ c k * (b j * ∏ i ∈ Ico (j + 1) k, c i) = b j * ((∏ k ∈ Ico (j + 1) k, c k) * c k)

Tactic:
ring
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
⊢ c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k =
    ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i

Tactic:
have heq : c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k =
        ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i := by
      rw [sum_Ico_succ_top hk, mul_sum, Ico_self, prod_empty, mul_one]
      refine congr_arg (· + b k) (sum_congr rfl fun j hj ↦ ?_)
      rw [prod_Ico_succ_top (by have := mem_Ico.mp hj; omega)]; ring
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
heq :
  c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k =
    ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i
⊢ u (k + 1) ≤ c k * u k + b k

Tactic:
hu k hk
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
heq :
  c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k =
    ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i
bc : 0 ≤ c k
⊢ c k * u k + b k ≤ c k * (u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i) + b k

Tactic:
gcongr
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
heq :
  c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k =
    ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i
rw :
  c k * (u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i) + b k =
    u n₀ * ((∏ x ∈ Ico n₀ k, c x) * c k) + (c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k)
⊢ c k * (u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i) + b k =
    u n₀ * ∏ i ∈ Ico n₀ (k + 1), c i + ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i

Tactic:
rw [← heq, ← prod_Ico_mul_eq_prod_Ico_add_one hk]

Premises used: Finset.prod_Ico_mul_eq_prod_Ico_add_one
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
heq :
  c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k =
    ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i
⊢ c k * (u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i) + b k =
    u n₀ * ((∏ x ∈ Ico n₀ k, c x) * c k) + (c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k)

Tactic:
ring
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n k : ℕ
hk : n₀ ≤ k
ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i
hck : 0 ≤ c k
heq :
  c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k =
    ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i
calc : c k * u k + b k ≤ c k * (u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i) + b k
calc₁ :
  c k * (u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i) + b k =
    u n₀ * ∏ i ∈ Ico n₀ (k + 1), c i + ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i
⊢ u (k + 1) ≤ u n₀ * ∏ i ∈ Ico n₀ (k + 1), c i + ∑ k_1 ∈ Ico n₀ (k + 1), b k_1 * ∏ i ∈ Ico (k_1 + 1) (k + 1), c i

Tactic:
calc u (k + 1)
      _ ≤ c k * u k + b k := hu k hk
      _ ≤ c k * (u n₀ * ∏ i ∈ Ico n₀ k, c i +
            ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i) + b k := by gcongr
      _ = u n₀ * ∏ i ∈ Ico n₀ (k + 1), c i +
            ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i := by
          rw [← heq, ← prod_Ico_mul_eq_prod_Ico_add_one hk]; ring

Premises used: HMul.hMul, Finset.Ico, Finset.prod, HAdd.hAdd, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
u b c : ℕ → R
n₀ : ℕ
hu : ∀ n ≥ n₀, u (n + 1) ≤ c n * u n + b n
hc : ∀ n ≥ n₀, 0 ≤ c n
n : ℕ
hn : n₀ ≤ n
base : u n₀ ≤ u n₀ * ∏ i ∈ Ico n₀ n₀, c i + ∑ k ∈ Ico n₀ n₀, b k * ∏ i ∈ Ico (k + 1) n₀, c i
succ :
  ∀ (k : ℕ) (hk : n₀ ≤ k)
    (ih : u k ≤ u n₀ * ∏ i ∈ Ico n₀ k, c i + ∑ k_1 ∈ Ico n₀ k, b k_1 * ∏ i ∈ Ico (k_1 + 1) k, c i),
    u (k + 1) ≤ u n₀ * ∏ i ∈ Ico n₀ (k + 1), c i + ∑ k_1 ∈ Ico n₀ (k + 1), b k_1 * ∏ i ∈ Ico (k_1 + 1) (k + 1), c i
⊢ u n ≤ u n₀ * ∏ i ∈ Ico n₀ n, c i + ∑ k ∈ Ico n₀ n, b k * ∏ i ∈ Ico (k + 1) n, c i

Tactic:
induction n, hn using Nat.le_induction with
  | base => simp
  | succ k hk ih =>
    have hck : 0 ≤ c k := hc k hk
    have heq : c k * ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i + b k =
        ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i := by
      rw [sum_Ico_succ_top hk, mul_sum, Ico_self, prod_empty, mul_one]
      refine congr_arg (· + b k) (sum_congr rfl fun j hj ↦ ?_)
      rw [prod_Ico_succ_top (by have := mem_Ico.mp hj; omega)]; ring
    calc u (k + 1)
      _ ≤ c k * u k + b k := hu k hk
      _ ≤ c k * (u n₀ * ∏ i ∈ Ico n₀ k, c i +
            ∑ j ∈ Ico n₀ k, b j * ∏ i ∈ Ico (j + 1) k, c i) + b k := by gcongr
      _ = u n₀ * ∏ i ∈ Ico n₀ (k + 1), c i +
            ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i := by
          rw [← heq, ← prod_Ico_mul_eq_prod_Ico_add_one hk]; ring
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n₀ ≤ n
⊢ ∀ n ≥ n₀, 0 ≤ 1 + c n

Tactic:
grind
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n₀ ≤ n
bc : ∀ i ∈ Ico n₀ n, 0 ≤ b i
bc₁ : ∀ i ∈ Ico n₀ n, ∀ i_1 ∈ Ico (i + 1) n, 0 ≤ 1 + c i_1
bc₂ : ∀ i ∈ Ico n₀ n, ∀ i_1 ∈ Ico n₀ n, i_1 ∉ Ico (i + 1) n → 1 ≤ 1 + c i_1
bc₃ : ∀ i ∈ Ico n₀ n, n₀ ≤ i + 1
⊢ u n₀ * ∏ i ∈ Ico n₀ n, (1 + c i) + ∑ k ∈ Ico n₀ n, b k * ∏ i ∈ Ico (k + 1) n, (1 + c i) ≤
    u n₀ * ∏ i ∈ Ico n₀ n, (1 + c i) + ∑ k ∈ Ico n₀ n, b k * ∏ i ∈ Ico n₀ n, (1 + c i)

Tactic:
gcongr
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n₀ ≤ n
i : ℕ
h : i ∈ Ico n₀ n
⊢ 0 ≤ b i

Tactic:
grind
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n₀ ≤ n
i : ℕ
h : i ∈ Ico n₀ n
⊢ ∀ i_1 ∈ Ico (i + 1) n, 0 ≤ 1 + c i_1

Tactic:
grind
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n₀ ≤ n
i : ℕ
h : i ∈ Ico n₀ n
⊢ ∀ i_1 ∈ Ico n₀ n, i_1 ∉ Ico (i + 1) n → 1 ≤ 1 + c i_1

Tactic:
grind
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n₀ ≤ n
i : ℕ
h : i ∈ Ico n₀ n
⊢ n₀ ≤ i + 1

Tactic:
grind
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n₀ ≤ n
rw :
  u n₀ * ∏ i ∈ Ico n₀ n, (1 + c i) + ∑ k ∈ Ico n₀ n, b k * ∏ i ∈ Ico n₀ n, (1 + c i) =
    u n₀ * ∏ i ∈ Ico n₀ n, (1 + c i) + HMul.hMul (α := ℝ) (∑ k ∈ Ico n₀ n, b k) (∏ i ∈ Ico n₀ n, (1 + c i))
rw₁ rw₂ :
  u n₀ * ∏ i ∈ Ico n₀ n, (1 + c i) + ∑ k ∈ Ico n₀ n, b k * ∏ i ∈ Ico n₀ n, (1 + c i) =
    u n₀ * ∏ i ∈ Ico n₀ n, (1 + c i) + ∑ i ∈ Ico n₀ n, b i * ∏ i ∈ Ico n₀ n, (1 + c i)
⊢ u n₀ * ∏ i ∈ Ico n₀ n, (1 + c i) + ∑ k ∈ Ico n₀ n, b k * ∏ i ∈ Ico n₀ n, (1 + c i) =
    (u n₀ + ∑ k ∈ Ico n₀ n, b k) * ∏ i ∈ Ico n₀ n, (1 + c i)

Tactic:
rw [add_mul, sum_mul]

Premises used: add_mul, Finset.sum_mul
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n₀ ≤ n
ha : 0 ≤ u n₀ + ∑ k ∈ Ico n₀ n, b k
hbc : ∏ i ∈ Ico n₀ n, (1 + c i) ≤ rexp (∑ i ∈ Ico n₀ n, c i)
⊢ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * ∏ i ∈ Ico n₀ n, (1 + c i) ≤ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * rexp (∑ i ∈ Ico n₀ n, c i)

Tactic:
gcongr
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n₀ ≤ n
⊢ ∀ i ∈ Ico n₀ n, 0 ≤ b i

Tactic:
grind
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n₀ ≤ n
⊢ 0 ≤ u n₀ + ∑ k ∈ Ico n₀ n, b k

Tactic:
exact add_nonneg hun₀ <| sum_nonneg <| by grind

Premises used: add_nonneg, Finset.sum_nonneg
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n₀ ≤ n
⊢ 0 ≤ u n₀ + ∑ k ∈ Ico n₀ n, b k

Tactic:
try exact add_nonneg hun₀ <| sum_nonneg <| by grind

Premises used: add_nonneg, Finset.sum_nonneg
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n₀ ≤ n
⊢ ∀ i ∈ Ico n₀ n, 0 ≤ 1 + c i

Tactic:
grind
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n₀ ≤ n
⊢ ∀ i ∈ Ico n₀ n, 1 + c i ≤ rexp (c i)

Tactic:
grind [add_one_le_exp]

Premises used: Real.add_one_le_exp
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n₀ ≤ n
⊢ ∏ i ∈ Ico n₀ n, (1 + c i) ≤ rexp (∑ i ∈ Ico n₀ n, c i)

Tactic:
simpa [exp_sum] using prod_le_prod (by grind) (by grind [add_one_le_exp])

Premises used: Finset.prod_le_prod, Real.exp_sum
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n₀ ≤ n
calc :
  u n₀ * ∏ i ∈ Ico n₀ n, (1 + c i) + ∑ k ∈ Ico n₀ n, b k * ∏ i ∈ Ico (k + 1) n, (1 + c i) ≤
    u n₀ * ∏ i ∈ Ico n₀ n, (1 + c i) + ∑ k ∈ Ico n₀ n, b k * ∏ i ∈ Ico n₀ n, (1 + c i)
calc₁ :
  u n₀ * ∏ i ∈ Ico n₀ n, (1 + c i) + ∑ k ∈ Ico n₀ n, b k * ∏ i ∈ Ico n₀ n, (1 + c i) =
    (u n₀ + ∑ k ∈ Ico n₀ n, b k) * ∏ i ∈ Ico n₀ n, (1 + c i)
calc₂ :
  (u n₀ + ∑ k ∈ Ico n₀ n, b k) * ∏ i ∈ Ico n₀ n, (1 + c i) ≤ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * rexp (∑ i ∈ Ico n₀ n, c i)
⊢ u n ≤ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * rexp (∑ i ∈ Ico n₀ n, c i)

Tactic:
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 (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 <;> grind
    _ = (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) := by
        gcongr <;> try exact add_nonneg hun₀ <| sum_nonneg <| by grind
        simpa [exp_sum] using prod_le_prod (by grind) (by grind [add_one_le_exp])

Premises used: discrete_gronwall_prod_general, Finset.Ico, Real.exp, HAdd.hAdd, Finset.sum
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n ∈ Ico n₀ n₁
⊢ ∀ i ∈ Ico n₀ n₁, 0 ≤ b i

Tactic:
grind
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n ∈ Ico n₀ n₁
⊢ LE.le (α := ℝ) 0 (∑ k ∈ Ico n₀ n₁, b k)

Tactic:
have : 0 ≤ ∑ k ∈ Ico n₀ n₁, b k := sum_nonneg <| by grind
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n ∈ Ico n₀ n₁
this : LE.le (α := ℝ) 0 (∑ k ∈ Ico n₀ n₁, b k)
h₁ : ∀ i ∈ Ico n₀ n₁, i ∉ Ico n₀ n → 0 ≤ b i
h₂ : n ≤ n₁
h₃ : ∀ i ∈ Ico n₀ n₁, i ∉ Ico n₀ n → 0 ≤ c i
h₄ : n ≤ n₁
⊢ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * rexp (∑ i ∈ Ico n₀ n, c i) ≤
    (u n₀ + ∑ k ∈ Ico n₀ n₁, b k) * rexp (∑ i ∈ Ico n₀ n₁, c i)

Tactic:
gcongr
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n ∈ Ico n₀ n₁
this : LE.le (α := ℝ) 0 (∑ k ∈ Ico n₀ n₁, b k)
⊢ ∀ i ∈ Ico n₀ n₁, i ∉ Ico n₀ n → 0 ≤ b i

Tactic:
grind
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n ∈ Ico n₀ n₁
this : LE.le (α := ℝ) 0 (∑ k ∈ Ico n₀ n₁, b k)
⊢ n ≤ n₁

Tactic:
grind
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n ∈ Ico n₀ n₁
this : LE.le (α := ℝ) 0 (∑ k ∈ Ico n₀ n₁, b k)
⊢ ∀ i ∈ Ico n₀ n₁, i ∉ Ico n₀ n → 0 ≤ c i

Tactic:
grind
-- Module: Mathlib.Analysis.ODE.DiscreteGronwall
Goal:
u b c : ℕ → ℝ
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 : ℕ
hn : n ∈ Ico n₀ n₁
this : LE.le (α := ℝ) 0 (∑ k ∈ Ico n₀ n₁, b k)
⊢ u n ≤ (u n₀ + ∑ k ∈ Ico n₀ n₁, b k) * rexp (∑ i ∈ Ico n₀ n₁, c i)

Tactic:
exact (discrete_gronwall hun₀ hu hc hb (mem_Ico.mp hn).1).trans (by gcongr <;> grind)

Premises used: And.left, discrete_gronwall, Iff.mp, LE.le.trans, Finset.mem_Ico
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ ε : ℝ
⊢ gronwallBound δ 0 ε = fun (x : ℝ) ↦ δ + ε * x

Tactic:
funext fun _ => if_pos rfl

Premises used: if_pos, funext, rfl
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K ε : ℝ
hK : K ≠ 0
⊢ gronwallBound δ K ε = fun (x : ℝ) ↦ δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)

Tactic:
funext fun _ => if_neg hK

Premises used: funext, if_neg
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K ε x : ℝ
pos : ∀ (hK : K = 0), HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
neg : ∀ (hK : ¬K = 0), HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x

Tactic:
by_cases hK : K = 0
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K ε x : ℝ
hK : K = 0
pos : HasDerivAt (gronwallBound δ 0 ε) (0 * gronwallBound δ 0 ε x + ε) x
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x

Tactic:
subst K
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ ε x : ℝ
pos : HasDerivAt (fun (x : ℝ) ↦ δ + ε * x) ε x
⊢ HasDerivAt (gronwallBound δ 0 ε) (0 * gronwallBound δ 0 ε x + ε) x

Tactic:
simp only [gronwallBound_K0, zero_mul, zero_add]

Premises used: MulZeroClass.zero_mul, gronwallBound_K0, zero_add
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ ε x : ℝ
⊢ HasDerivAt (fun (x : ℝ) ↦ δ + ε * id x) (ε * 1) x

Tactic:
((hasDerivAt_id x).const_mul ε).const_add δ

Premises used: hasDerivAt_id, HasDerivAt.const_mul, HasDerivAt.const_add
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ ε x : ℝ
h : ε = ε * 1
⊢ HasDerivAt (fun (x : ℝ) ↦ δ + ε * x) ε x

Tactic:
convert! ((hasDerivAt_id x).const_mul ε).const_add δ

Premises used: hasDerivAt_id, HasDerivAt.const_mul, HasDerivAt.const_add
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ ε x : ℝ
h h₁ : ε = ε
⊢ ε = ε * 1

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K ε x : ℝ
hK : ¬K = 0
neg :
  HasDerivAt (fun (x : ℝ) ↦ δ * rexp (K * x) + ε / K * (rexp (K * x) - 1))
    (K * (δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)) + ε) x
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x

Tactic:
simp only [gronwallBound_of_K_ne_0 hK]

Premises used: gronwallBound_of_K_ne_0
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (HAdd.hAdd (α := ℝ → ℝ) (fun (y : ℝ) ↦ δ * rexp (K * id y)) fun (y : ℝ) ↦ ε / K * (rexp (K * id y) - 1))
    (δ * (rexp (K * id x) * (K * 1)) + ε / K * (rexp (K * id x) * (K * 1))) x

Tactic:
(((hasDerivAt_id x).const_mul K).exp.const_mul δ).add
        ((((hasDerivAt_id x).const_mul K).exp.sub_const 1).const_mul (ε / K))

Premises used: HasDerivAt.add, HasDerivAt.exp, HDiv.hDiv, HasDerivAt.sub_const, hasDerivAt_id, HasDerivAt.const_mul, OfNat.ofNat
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K ε x : ℝ
hK : ¬K = 0
h :
  K * (δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)) + ε =
    δ * (rexp (K * id x) * (K * 1)) + ε / K * (rexp (K * id x) * (K * 1))
⊢ HasDerivAt (fun (x : ℝ) ↦ δ * rexp (K * x) + ε / K * (rexp (K * x) - 1))
    (K * (δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)) + ε) x

Tactic:
convert!
      (((hasDerivAt_id x).const_mul K).exp.const_mul δ).add
        ((((hasDerivAt_id x).const_mul K).exp.sub_const 1).const_mul (ε / K)) using 1

Premises used: HasDerivAt.add, HasDerivAt.exp, HDiv.hDiv, HasDerivAt.sub_const, hasDerivAt_id, HasDerivAt.const_mul, OfNat.ofNat