awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.ODE.Basic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
h : ∀ t ∈ s, IsIntegralCurveAt γ v t
t : ℝ
ht : t ∈ s
⊢ HasDerivWithinAt γ (v t (γ t)) s t
have obtain : ∀ (s' : Set ℝ) (hs' : s' ∈ 𝓝 t) (h : ∀ y ∈ s', HasDerivAt γ (v y (γ y)) y), HasDerivWithinAt γ (v t (γ t)) s t
Tactic: obtain ⟨s', hs', h⟩ := Filter.eventually_iff_exists_mem.mp (h t ht)
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (hypothesis)
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
⊢ 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
have hck : 0 ≤ c k
Tactic: have hck : 0 ≤ c k := hc k hk
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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
have 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
Tactic: rw [sum_Ico_succ_top hk, mul_sum, Ico_self, prod_empty, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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
have 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
Tactic: refine congr_arg (· + b k) (sum_congr rfl fun j hj ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (hypothesis)
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
⊢ j + 1 ≤ k
have this : n₀ ≤ j ∧ j < k
Tactic: have := mem_Ico.mp hj
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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 * ∏ i ∈ Ico (j + 1) (k + 1), c i
have rw : c k * (b j * ∏ i ∈ Ico (j + 1) k, c i) = b j * ((∏ k ∈ Ico (j + 1) k, c k) * c k)
Tactic: rw [prod_Ico_succ_top (by have := mem_Ico.mp hj; omega)]
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (hypothesis)
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
⊢ 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
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
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
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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₀ * ∏ i ∈ Ico n₀ (k + 1), c i + ∑ j ∈ Ico n₀ (k + 1), b j * ∏ i ∈ Ico (j + 1) (k + 1), c i
have 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)
Tactic: rw [← heq, ← prod_Ico_mul_eq_prod_Ico_add_one hk]
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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) ≤ 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
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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
⊢ 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
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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
⊢ u n ≤ u n₀ * ∏ i ∈ Ico n₀ n, c i + ∑ k ∈ Ico n₀ n, b k * ∏ i ∈ Ico (k + 1) n, c i
have base : 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
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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
⊢ u n ≤ u n₀ * ∏ i ∈ Ico n₀ n, c i + ∑ k ∈ Ico n₀ n, b k * ∏ i ∈ Ico (k + 1) n, c i
have 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
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
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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
⊢ 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)
have bc : ∀ i ∈ Ico n₀ n, 0 ≤ b i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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
⊢ 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)
have bc₁ : ∀ i ∈ Ico n₀ n, ∀ i_1 ∈ Ico (i + 1) n, 0 ≤ 1 + c i_1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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
⊢ 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)
have bc₂ : ∀ i ∈ Ico n₀ n, ∀ i_1 ∈ Ico n₀ n, i_1 ∉ Ico (i + 1) n → 1 ≤ 1 + c i_1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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
⊢ 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)
have bc₃ : ∀ i ∈ Ico n₀ n, n₀ ≤ i + 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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
⊢ 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)
have 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))
Tactic: rw [add_mul, sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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))
⊢ 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)
have 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)
Tactic: rw [add_mul, sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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
⊢ (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)
have ha : 0 ≤ u n₀ + ∑ k ∈ Ico n₀ n, b k
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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
⊢ (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)
have hbc : ∏ i ∈ Ico n₀ n, (1 + c i) ≤ rexp (∑ i ∈ Ico n₀ n, c i)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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
⊢ u n ≤ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * rexp (∑ i ∈ Ico n₀ n, c i)
have 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)
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])
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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)
⊢ u n ≤ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * rexp (∑ i ∈ Ico n₀ n, c i)
have 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)
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])
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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)
⊢ u n ≤ (u n₀ + ∑ k ∈ Ico n₀ n, b k) * rexp (∑ i ∈ Ico n₀ n, c i)
have 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)
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])
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (hypothesis)
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₁
⊢ u n ≤ (u n₀ + ∑ k ∈ Ico n₀ n₁, b k) * rexp (∑ i ∈ Ico n₀ n₁, c i)
have this : LE.le (α := ℝ) 0 (∑ k ∈ Ico n₀ n₁, b k)
Tactic: have : 0 ≤ ∑ k ∈ Ico n₀ n₁, b k := sum_nonneg <| by grind
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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₀ + ∑ 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)
have h₁ : ∀ i ∈ Ico n₀ n₁, i ∉ Ico n₀ n → 0 ≤ b i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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
⊢ (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)
have h₂ : n ≤ n₁
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.ODE.DiscreteGronwall (goal)
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₁
⊢ (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)
have h₃ : ∀ i ∈ Ico n₀ n₁, i ∉ Ico n₀ n → 0 ≤ c i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K ε x : ℝ
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
have pos : ∀ (hK : K = 0), HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
Tactic: by_cases hK : K = 0
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K ε x : ℝ
pos : ∀ (hK : K = 0), HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
have neg : ∀ (hK : ¬K = 0), HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
Tactic: by_cases hK : K = 0
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K ε x : ℝ
hK : K = 0
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
have pos : HasDerivAt (gronwallBound δ 0 ε) (0 * gronwallBound δ 0 ε x + ε) x
Tactic: subst K
Cleared hypotheses: K, hK
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ ε x : ℝ
⊢ HasDerivAt (gronwallBound δ 0 ε) (0 * gronwallBound δ 0 ε x + ε) x
have pos : HasDerivAt (fun (x : ℝ) ↦ δ + ε * x) ε x
Tactic: simp only [gronwallBound_K0, zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ ε x : ℝ
⊢ HasDerivAt (fun (x : ℝ) ↦ δ + ε * x) ε x
have h : ε = ε * 1
Tactic: convert! ((hasDerivAt_id x).const_mul ε).const_add δ
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ ε x : ℝ
⊢ ε = ε * 1
have h : ε = ε
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
have neg : HasDerivAt (fun (x : ℝ) ↦ δ * rexp (K * x) + ε / K * (rexp (K * x) - 1))
  (K * (δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)) + ε) x
Tactic: simp only [gronwallBound_of_K_ne_0 hK]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (fun (x : ℝ) ↦ δ * rexp (K * x) + ε / K * (rexp (K * x) - 1))
    (K * (δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)) + ε) x
have h : K * (δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)) + ε =
  δ * (rexp (K * id x) * (K * 1)) + ε / K * (rexp (K * id x) * (K * 1))
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
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K ε x : ℝ
hK : ¬K = 0
⊢ K * (δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)) + ε =
    δ * (rexp (K * id x) * (K * 1)) + ε / K * (rexp (K * id x) * (K * 1))
have h : K * (δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)) + ε =
  δ * (rexp (K * x) * (K * 1)) + ε / K * (rexp (K * x) * (K * 1))
Tactic: simp only [id]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K ε x a : ℝ
⊢ HasDerivAt (fun (y : ℝ) ↦ gronwallBound δ K ε (y - a)) (K * gronwallBound δ K ε (x - a) + ε) x
have h : K * gronwallBound δ K ε (x - a) + ε = (K * gronwallBound δ K ε (id x - a) + ε) * 1
Tactic: convert! (hasDerivAt_gronwallBound δ K ε _).comp x ((hasDerivAt_id x).sub_const a) using 1
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K ε x a : ℝ
⊢ K * gronwallBound δ K ε (x - a) + ε = (K * gronwallBound δ K ε (id x - a) + ε) * 1
have h : K * gronwallBound δ K ε (x - a) + ε = (K * gronwallBound δ K ε (x - a) + ε) * 1
Tactic: rw [id, mul_one]