awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K ε x a : ℝ
h : K * gronwallBound δ K ε (x - a) + ε = (K * gronwallBound δ K ε (x - a) + ε) * 1
⊢ K * gronwallBound δ K ε (x - a) + ε = (K * gronwallBound δ K ε (id x - a) + ε) * 1
have h₁ : K * gronwallBound δ K ε (x - a) + ε = K * gronwallBound δ K ε (x - a) + ε
Tactic: rw [id, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K ε : ℝ
⊢ gronwallBound δ K ε 0 = δ
have pos : ∀ (hK : K = 0), gronwallBound δ K ε 0 = δ
Tactic: by_cases hK : K = 0
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K ε : ℝ
pos : ∀ (hK : K = 0), gronwallBound δ K ε 0 = δ
⊢ gronwallBound δ K ε 0 = δ
have neg : ∀ (hK : ¬K = 0), gronwallBound δ K ε 0 = δ
Tactic: by_cases hK : K = 0
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K x : ℝ
⊢ gronwallBound δ K 0 x = δ * rexp (K * x)
have pos : ∀ (hK : K = 0), gronwallBound δ K 0 x = δ * rexp (K * x)
Tactic: by_cases hK : K = 0
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K x : ℝ
pos : ∀ (hK : K = 0), gronwallBound δ K 0 x = δ * rexp (K * x)
⊢ gronwallBound δ K 0 x = δ * rexp (K * x)
have neg : ∀ (hK : ¬K = 0), gronwallBound δ K 0 x = δ * rexp (K * x)
Tactic: by_cases hK : K = 0
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K x : ℝ
⊢ Continuous (Y := ℝ) fun (ε : ℝ) ↦ gronwallBound δ K ε x
have pos : ∀ (hK : K = 0), Continuous (Y := ℝ) fun (ε : ℝ) ↦ gronwallBound δ K ε x
Tactic: by_cases hK : K = 0
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K x : ℝ
pos : ∀ (hK : K = 0), Continuous (Y := ℝ) fun (ε : ℝ) ↦ gronwallBound δ K ε x
⊢ Continuous (Y := ℝ) fun (ε : ℝ) ↦ gronwallBound δ K ε x
have neg : ∀ (hK : ¬K = 0), Continuous (Y := ℝ) fun (ε : ℝ) ↦ gronwallBound δ K ε x
Tactic: by_cases hK : K = 0
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K x : ℝ
hK : K = 0
⊢ Continuous (Y := ℝ) fun (ε : ℝ) ↦ gronwallBound δ K ε x
have pos : Continuous (Y := ℝ) fun (ε : ℝ) ↦ δ + ε * x
Tactic: simp only [gronwallBound_K0, hK]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K x : ℝ
hK : ¬K = 0
⊢ Continuous (Y := ℝ) fun (ε : ℝ) ↦ gronwallBound δ K ε x
have neg : Continuous (Y := ℝ) fun (ε : ℝ) ↦ δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)
Tactic: simp only [gronwallBound_of_K_ne_0 hK]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
hK : 0 ≤ K
x₁ x₂ : ℝ
hx : x₁ ≤ x₂
⊢ (if K = 0 then δ + ε * x₁ else δ * rexp (K * x₁) + ε / K * (rexp (K * x₁) - 1)) ≤
    if K = 0 then δ + ε * x₂ else δ * rexp (K * x₂) + ε / K * (rexp (K * x₂) - 1)
have pos : ∀ (hK₀ : K = 0), δ + ε * x₁ ≤ δ + ε * x₂
Tactic: split_ifs with hK₀
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
hK : 0 ≤ K
x₁ x₂ : ℝ
hx : x₁ ≤ x₂
pos : ∀ (hK₀ : K = 0), δ + ε * x₁ ≤ δ + ε * x₂
⊢ (if K = 0 then δ + ε * x₁ else δ * rexp (K * x₁) + ε / K * (rexp (K * x₁) - 1)) ≤
    if K = 0 then δ + ε * x₂ else δ * rexp (K * x₂) + ε / K * (rexp (K * x₂) - 1)
have neg : ∀ (hK₀ : ¬K = 0), δ * rexp (K * x₁) + ε / K * (rexp (K * x₁) - 1) ≤ δ * rexp (K * x₂) + ε / K * (rexp (K * x₂) - 1)
Tactic: split_ifs with hK₀
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (hypothesis)
Goal:
δ K ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
hK : 0 ≤ K
x₁ x₂ : ℝ
hx : x₁ ≤ x₂
hK₀ : ¬K = 0
⊢ δ * rexp (K * x₁) + ε / K * (rexp (K * x₁) - 1) ≤ δ * rexp (K * x₂) + ε / K * (rexp (K * x₂) - 1)
have hK_pos : 0 < K
Tactic: have hK_pos : 0 < K := by positivity
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
δ K ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
hK : 0 ≤ K
x₁ x₂ : ℝ
hx : x₁ ≤ x₂
hK₀ : ¬K = 0
hK_pos : 0 < K
neg : 0 ≤ δ
neg₁ : 0 ≤ K
⊢ δ * rexp (K * x₁) + ε / K * (rexp (K * x₁) - 1) ≤ δ * rexp (K * x₂) + ε / K * (rexp (K * x₂) - 1)
have neg₂ : 0 ≤ ε / K
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
⊢ ε' ∈ Ioi ε → f x ≤ gronwallBound δ K ε' (x - a)
have ε₁ : ∀ (hε' : ε < ε'), f x ≤ gronwallBound δ K ε' (x - a)
Tactic: (hε' : ε < ε')
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε < ε'
⊢ f x ≤ gronwallBound δ K ε' (x - a)
have ha₁ : f a ≤ gronwallBound δ K ε' (a - a)
Tactic: apply image_le_of_liminf_slope_right_lt_deriv_boundary hf hf'
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε < ε'
ha₁ : f a ≤ gronwallBound δ K ε' (a - a)
⊢ f x ≤ gronwallBound δ K ε' (x - a)
have hB : ∀ (x : ℝ), HasDerivAt (fun (x : ℝ) ↦ gronwallBound δ K ε' (x - a)) (K * gronwallBound δ K ε' (x - a) + ε') x
Tactic: apply image_le_of_liminf_slope_right_lt_deriv_boundary hf hf'
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε < ε'
ha₁ : f a ≤ gronwallBound δ K ε' (a - a)
hB : ∀ (x : ℝ), HasDerivAt (fun (x : ℝ) ↦ gronwallBound δ K ε' (x - a)) (K * gronwallBound δ K ε' (x - a) + ε') x
⊢ f x ≤ gronwallBound δ K ε' (x - a)
have bound₁ : ∀ x ∈ Ico a b, f x = gronwallBound δ K ε' (x - a) → f' x < K * gronwallBound δ K ε' (x - a) + ε'
Tactic: apply image_le_of_liminf_slope_right_lt_deriv_boundary hf hf'
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε < ε'
⊢ f a ≤ gronwallBound δ K ε' (a - a)
have ha₁ : f a ≤ gronwallBound δ K ε' 0
Tactic: rwa [sub_self, gronwallBound_x0]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (hypothesis)
Goal:
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
⊢ ∀ x ∈ Icc a b, f x ≤ gronwallBound δ K ε (x - a)
have H : ∀ x ∈ Icc a b, ∀ ε' ∈ Ioi ε, f x ≤ gronwallBound δ K ε' (x - a)
Tactic: have H : ∀ x ∈ Icc a b, ∀ ε' ∈ Ioi ε, f x ≤ gronwallBound δ K ε' (x - a) := by
    intro x hx ε' (hε' : ε < ε')
    apply image_le_of_liminf_slope_right_lt_deriv_boundary hf hf'
    · rwa [sub_self, gronwallBound_x0]
    · exact fun x => hasDerivAt_gronwallBound_shift δ K ε' x a
    · grind
    · exact hx
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
H : ∀ x ∈ Icc a b, ∀ ε' ∈ Ioi ε, f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ f x ≤ (fun (ε' : ℝ) ↦ gronwallBound δ K ε' (x - a)) ε
have convert_2 : ε ∈ closure (Ioi ε)
Tactic: convert! continuousWithinAt_const.closure_le _ _ (H x hx)
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ x ∈ Ico a b, f' x ≤ K * f x + ε
H : ∀ x ∈ Icc a b, ∀ ε' ∈ Ioi ε, f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
convert_2 : ε ∈ closure (Ioi ε)
⊢ f x ≤ (fun (ε' : ℝ) ↦ gronwallBound δ K ε' (x - a)) ε
have convert_3 : ContinuousWithinAt (Y := ℝ) (fun (y : ℝ) ↦ gronwallBound δ K y (x - a)) (Ioi ε) ε
Tactic: convert! continuousWithinAt_const.closure_le _ _ (H x hx)
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → E
K a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
ha : f a = 0
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ K * ‖f x‖
x : ℝ
hx : x ∈ Icc a b
⊢ f x = 0
have apply : ‖f x‖ ≤ 0
Tactic: apply norm_le_zero_iff.mp
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → E
K a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
ha : f a = 0
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ K * ‖f x‖
x : ℝ
hx : x ∈ Icc a b
⊢ gronwallBound 0 K 0 (x - a) = 0
have rw : Eq (α := ℝ) 0 0
Tactic: rw [gronwallBound_ε0_δ0]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → E
K a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ x ∈ Ico a b, HasDerivWithinAt f (f' x) (Ici x) x
ha : f a = 0
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ K * ‖f x‖
x : ℝ
hx : x ∈ Icc a b
⊢ ‖f x‖ ≤ 0
have calc : gronwallBound 0 K 0 (x - a) = 0
Tactic: calc ‖f x‖
    _ ≤ gronwallBound 0 K 0 (x - a) :=
      norm_le_gronwallBound_of_norm_deriv_right_le hf hf' (by simp [ha]) (by simpa using bound) _ hx
    _ = 0 := by rw [gronwallBound_ε0_δ0]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t
f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t
g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : dist (f a) (g a) ≤ δ
⊢ ∀ t ∈ Icc a b, dist (f t) (g t) ≤ gronwallBound δ (↑K : ℝ) (εf + εg) (t - a)
have simp : ∀ (ha : ‖f a - g a‖ ≤ δ), ∀ t ∈ Icc a b, ‖f t - g t‖ ≤ gronwallBound δ (↑K : ℝ) (εf + εg) (t - a)
Tactic: simp only [dist_eq_norm] at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t
f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t
g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : ‖f a - g a‖ ≤ δ
⊢ ∀ t ∈ Icc a b, ‖f t - g t‖ ≤ gronwallBound δ (↑K : ℝ) (εf + εg) (t - a)
have h_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt (fun (t : ℝ) ↦ f t - g t) (f' t - g' t) (Ici t) t
Tactic: have h_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt (fun t => f t - g t) (f' t - g' t) (Ici t) t :=
    fun t ht => (hf' t ht).sub (hg' t ht)
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t
f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t
g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : ‖f a - g a‖ ≤ δ
h_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt (fun (t : ℝ) ↦ f t - g t) (f' t - g' t) (Ici t) t
⊢ ∀ t ∈ Icc a b, ‖f t - g t‖ ≤ gronwallBound δ (↑K : ℝ) (εf + εg) (t - a)
have apply : ∀ x ∈ Ico a b, ‖f' x - g' x‖ ≤ (↑K : ℝ) * ‖f x - g x‖ + (εf + εg)
Tactic: apply norm_le_gronwallBound_of_norm_deriv_right_le (hf.sub hg) h_deriv ha
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t
f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t
g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : ‖f a - g a‖ ≤ δ
h_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt (fun (t : ℝ) ↦ f t - g t) (f' t - g' t) (Ici t) t
t : ℝ
ht : t ∈ Ico a b
⊢ ‖f' t - g' t‖ ≤ (↑K : ℝ) * ‖f t - g t‖ + (εf + εg)
have this : dist (f' t) (g' t) ≤ dist (f' t) (v t (f t)) + dist (g' t) (v t (g t)) + dist (v t (f t)) (v t (g t))
Tactic: have := dist_triangle4_right (f' t) (g' t) (v t (f t)) (v t (g t))
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (f' t) (Ici t) t
f_bound : ∀ t ∈ Ico a b, dist (f' t) (v t (f t)) ≤ εf
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (g' t) (Ici t) t
g_bound : ∀ t ∈ Ico a b, dist (g' t) (v t (g t)) ≤ εg
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : ‖f a - g a‖ ≤ δ
h_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt (fun (t : ℝ) ↦ f t - g t) (f' t - g' t) (Ici t) t
t : ℝ
ht : t ∈ Ico a b
this : dist (f' t) (g' t) ≤ dist (f' t) (v t (f t)) + dist (g' t) (v t (g t)) + dist (v t (f t)) (v t (g t))
⊢ ‖f' t - g' t‖ ≤ (↑K : ℝ) * ‖f t - g t‖ + (εf + εg)
have this₁ : dist (v t (f t)) (v t (g t)) ≤ (↑K : ℝ) * dist (f t) (g t)
Tactic: have := (hv t ht).dist_le_mul _ (hfs t ht) _ (hgs t ht)
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : dist (f a) (g a) ≤ δ
t : ℝ
h : t ∈ Ico a b
⊢ dist (v t (f t)) (v t (f t)) ≤ 0
have rw : LE.le (α := ℝ) 0 0
Tactic: rw [dist_self]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : dist (f a) (g a) ≤ δ
⊢ ∀ t ∈ Icc a b, dist (f t) (g t) ≤ δ * rexp ((↑K : ℝ) * (t - a))
have f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0
Tactic: have f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0 := by intros; rw [dist_self]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : dist (f a) (g a) ≤ δ
f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0
t : ℝ
h : t ∈ Ico a b
⊢ dist (v t (g t)) (v t (g t)) ≤ 0
have rw : LE.le (α := ℝ) 0 0
Tactic: rw [dist_self]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : dist (f a) (g a) ≤ δ
f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0
⊢ ∀ t ∈ Icc a b, dist (f t) (g t) ≤ δ * rexp ((↑K : ℝ) * (t - a))
have g_bound : ∀ t ∈ Ico a b, dist (v t (g t)) (v t (g t)) ≤ 0
Tactic: have g_bound : ∀ t ∈ Ico a b, dist (v t (g t)) (v t (g t)) ≤ 0 := by intros; rw [dist_self]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : dist (f a) (g a) ≤ δ
f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0
g_bound : ∀ t ∈ Ico a b, dist (v t (g t)) (v t (g t)) ≤ 0
t : ℝ
ht : t ∈ Icc a b
⊢ dist (f t) (g t) ≤ δ * rexp ((↑K : ℝ) * (t - a))
have this : dist (f t) (g t) ≤ gronwallBound δ (↑K : ℝ) (HAdd.hAdd (α := ℝ) 0 0) (t - a)
Tactic: have :=
    dist_le_of_approx_trajectories_ODE_of_mem hv hf hf' f_bound hfs hg hg' g_bound hgs ha t ht
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : dist (f a) (g a) ≤ δ
f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0
g_bound : ∀ t ∈ Ico a b, dist (v t (g t)) (v t (g t)) ≤ 0
t : ℝ
ht : t ∈ Icc a b
this : dist (f t) (g t) ≤ gronwallBound δ (↑K : ℝ) (HAdd.hAdd (α := ℝ) 0 0) (t - a)
⊢ dist (f t) (g t) ≤ δ * rexp ((↑K : ℝ) * (t - a))
have rwa : ∀ (this : dist (f t) (g t) ≤ gronwallBound δ (↑K : ℝ) 0 (t - a)), dist (f t) (g t) ≤ δ * rexp ((↑K : ℝ) * (t - a))
Tactic: rwa [zero_add, gronwallBound_ε0] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b δ : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : dist (f a) (g a) ≤ δ
f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0
g_bound : ∀ t ∈ Ico a b, dist (v t (g t)) (v t (g t)) ≤ 0
t : ℝ
ht : t ∈ Icc a b
this : dist (f t) (g t) ≤ gronwallBound δ (↑K : ℝ) (HAdd.hAdd (α := ℝ) 0 0) (t - a)
rwa : ∀ (this : dist (f t) (g t) ≤ gronwallBound δ (↑K : ℝ) 0 (t - a)), dist (f t) (g t) ≤ δ * rexp ((↑K : ℝ) * (t - a))
⊢ dist (f t) (g t) ≤ δ * rexp ((↑K : ℝ) * (t - a))
have rwa₁ : ∀ (this : dist (f t) (g t) ≤ δ * rexp ((↑K : ℝ) * (t - a))), dist (f t) (g t) ≤ δ * rexp ((↑K : ℝ) * (t - a))
Tactic: rwa [zero_add, gronwallBound_ε0] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : f a = g a
t : ℝ
ht : t ∈ Icc a b
⊢ f t = g t
have this : dist (f t) (g t) ≤ 0 * rexp ((↑K : ℝ) * (t - a))
Tactic: have := dist_le_of_trajectories_ODE_of_mem hv hf hf' hfs hg hg' hgs (dist_le_zero.2 ha) t ht
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : f a = g a
t : ℝ
ht : t ∈ Icc a b
this : dist (f t) (g t) ≤ 0 * rexp ((↑K : ℝ) * (t - a))
⊢ f t = g t
have rwa : ∀ (this : dist (f t) (g t) ≤ 0), f t = g t
Tactic: rwa [zero_mul, dist_le_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ico a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ t ∈ Ico a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ t ∈ Ico a b, g t ∈ s t
ha : f a = g a
t : ℝ
ht : t ∈ Icc a b
this : dist (f t) (g t) ≤ 0 * rexp ((↑K : ℝ) * (t - a))
rwa : ∀ (this : dist (f t) (g t) ≤ 0), f t = g t
⊢ f t = g t
have rwa₁ : ∀ (this : f t = g t), f t = g t
Tactic: rwa [zero_mul, dist_le_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
t : ℝ
ht : t ∈ Ico (-b) (-a)
⊢ -t ∈ Ioc a b
have ht₁ : -b ≤ t ∧ t < -a
Tactic: push _ ∈ _ at ht ⊢
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
t : ℝ
ht : -b ≤ t ∧ t < -a
⊢ a < -t ∧ -t ≤ b
have left : a < -t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.ODE.Gronwall (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
s : ℝ → Set E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ t ∈ Ioc a b, LipschitzOnWith K (v t) (s t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioc a b, HasDerivWithinAt f (v t (f t)) (Iic t) t
hfs : ∀ t ∈ Ioc a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioc a b, HasDerivWithinAt g (v t (g t)) (Iic t) t
hgs : ∀ t ∈ Ioc a b, g t ∈ s t
hb : f b = g b
t : ℝ
ht : -b ≤ t ∧ t < -a
left : a < -t
⊢ a < -t ∧ -t ≤ b
have right : -t ≤ b
Tactic: constructor