awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K ε x : ℝ
hK : ¬K = 0
h :
  K * (δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)) + ε =
    δ * (rexp (K * x) * (K * 1)) + ε / K * (rexp (K * x) * (K * 1))
⊢ K * (δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)) + ε =
    δ * (rexp (K * id x) * (K * 1)) + ε / K * (rexp (K * id x) * (K * 1))

Tactic:
simp only [id]

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

Tactic:
field
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K ε x a : ℝ
⊢ HasDerivAt (gronwallBound δ K ε ∘ fun (x : ℝ) ↦ id x - a) ((K * gronwallBound δ K ε (id x - a) + ε) * 1) x

Tactic:
(hasDerivAt_gronwallBound δ K ε _).comp x ((hasDerivAt_id x).sub_const a)

Premises used: HasDerivAt.comp, HasDerivAt.sub_const, hasDerivAt_id, hasDerivAt_gronwallBound
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K ε x a : ℝ
h : K * gronwallBound δ K ε (x - a) + ε = (K * gronwallBound δ K ε (id x - a) + ε) * 1
⊢ HasDerivAt (fun (y : ℝ) ↦ gronwallBound δ K ε (y - a)) (K * gronwallBound δ K ε (x - a) + ε) x

Tactic:
convert! (hasDerivAt_gronwallBound δ K ε _).comp x ((hasDerivAt_id x).sub_const a) using 1

Premises used: HasDerivAt.comp, HasDerivAt.sub_const, hasDerivAt_id, hasDerivAt_gronwallBound
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K ε x a : ℝ
h : K * gronwallBound δ K ε (x - a) + ε = (K * gronwallBound δ K ε (x - a) + ε) * 1
h₁ h₂ : K * gronwallBound δ K ε (x - a) + ε = K * gronwallBound δ K ε (x - a) + ε
⊢ K * gronwallBound δ K ε (x - a) + ε = (K * gronwallBound δ K ε (id x - a) + ε) * 1

Tactic:
rw [id, mul_one]

Premises used: id, mul_one
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K ε : ℝ
pos : ∀ (hK : K = 0), gronwallBound δ K ε 0 = δ
neg : ∀ (hK : ¬K = 0), gronwallBound δ K ε 0 = δ
⊢ gronwallBound δ K ε 0 = δ

Tactic:
by_cases hK : K = 0
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K ε : ℝ
hK : K = 0
⊢ gronwallBound δ K ε 0 = δ

Tactic:
simp only [gronwallBound, if_pos hK, mul_zero, add_zero]

Premises used: gronwallBound, if_pos, MulZeroClass.mul_zero, add_zero
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K ε : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K ε 0 = δ

Tactic:
simp only [gronwallBound, if_neg hK, mul_zero, exp_zero, sub_self, mul_one,
      add_zero]

Premises used: sub_self, gronwallBound, MulZeroClass.mul_zero, Real.exp_zero, mul_one, add_zero, if_neg
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K x : ℝ
pos : ∀ (hK : K = 0), gronwallBound δ K 0 x = δ * rexp (K * x)
neg : ∀ (hK : ¬K = 0), gronwallBound δ K 0 x = δ * rexp (K * x)
⊢ gronwallBound δ K 0 x = δ * rexp (K * x)

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

Tactic:
simp only [gronwallBound_K0, hK, zero_mul, exp_zero, add_zero, mul_one]

Premises used: MulZeroClass.zero_mul, gronwallBound_K0, Real.exp_zero, mul_one, add_zero
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K x : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K 0 x = δ * rexp (K * x)

Tactic:
simp only [gronwallBound_of_K_ne_0 hK, zero_div, zero_mul, add_zero]

Premises used: gronwallBound_of_K_ne_0, MulZeroClass.zero_mul, zero_div, add_zero
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
K x : ℝ
⊢ gronwallBound 0 K 0 x = 0

Tactic:
simp only [gronwallBound_ε0, zero_mul]

Premises used: MulZeroClass.zero_mul, gronwallBound_ε0
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K x : ℝ
pos : ∀ (hK : K = 0), Continuous (Y := ℝ) fun (ε : ℝ) ↦ gronwallBound δ K ε x
neg : ∀ (hK : ¬K = 0), Continuous (Y := ℝ) fun (ε : ℝ) ↦ gronwallBound δ K ε x
⊢ Continuous (Y := ℝ) fun (ε : ℝ) ↦ gronwallBound δ K ε x

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

Tactic:
simp only [gronwallBound_K0, hK]

Premises used: gronwallBound_K0
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K x : ℝ
hK : K = 0
⊢ Continuous (Y := ℝ) fun (ε : ℝ) ↦ δ + ε * x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K x : ℝ
hK : ¬K = 0
neg : Continuous (Y := ℝ) fun (ε : ℝ) ↦ δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)
⊢ Continuous (Y := ℝ) fun (ε : ℝ) ↦ gronwallBound δ K ε 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
⊢ Continuous (Y := ℝ) fun (ε : ℝ) ↦ δ * rexp (K * x) + ε / K * (rexp (K * x) - 1)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
hK : 0 ≤ K
x₁ x₂ : ℝ
hx : x₁ ≤ x₂
pos : ∀ (hK₀ : K = 0), δ + ε * x₁ ≤ δ + ε * x₂
neg :
  ∀ (hK₀ : ¬K = 0), δ * rexp (K * x₁) + ε / K * (rexp (K * x₁) - 1) ≤ δ * rexp (K * x₂) + ε / K * (rexp (K * x₂) - 1)
⊢ (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)

Tactic:
split_ifs with hK₀
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
hK : 0 ≤ K
x₁ x₂ : ℝ
hx : x₁ ≤ x₂
hK₀ : K = 0
pos : 0 ≤ ε
⊢ δ + ε * x₁ ≤ δ + ε * x₂

Tactic:
gcongr
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
hK : 0 ≤ K
x₁ x₂ : ℝ
hx : x₁ ≤ x₂
hK₀ : ¬K = 0
⊢ 0 < K

Tactic:
positivity
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
δ K ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
hK : 0 ≤ K
x₁ x₂ : ℝ
hx : x₁ ≤ x₂
hK₀ : ¬K = 0
⊢ 0 < K

Tactic:
have hK_pos : 0 < K := by positivity
-- Module: Mathlib.Analysis.ODE.Gronwall
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
neg₂ : 0 ≤ ε / K
neg₃ : 0 ≤ K
⊢ δ * rexp (K * x₁) + ε / K * (rexp (K * x₁) - 1) ≤ δ * rexp (K * x₂) + ε / K * (rexp (K * x₂) - 1)

Tactic:
gcongr
-- Module: Mathlib.Analysis.ODE.Gronwall
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)
⊢ ε' ∈ Ioi ε → f x ≤ gronwallBound δ K ε' (x - a)

Tactic:
(hε' : ε < ε')
-- Module: Mathlib.Analysis.ODE.Gronwall
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
bound₁ : ∀ x ∈ Ico a b, f x = gronwallBound δ K ε' (x - a) → f' x < K * gronwallBound δ K ε' (x - a) + ε'
a₁ : x ∈ Icc a b
apply : ℝ → ℝ
⊢ f x ≤ gronwallBound δ K ε' (x - a)

Tactic:
apply image_le_of_liminf_slope_right_lt_deriv_boundary hf hf'

Premises used: image_le_of_liminf_slope_right_lt_deriv_boundary
-- Module: Mathlib.Analysis.ODE.Gronwall
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 ε' 0
ha₂ ha₃ ha₄ ha₅ : f a ≤ δ
⊢ f a ≤ gronwallBound δ K ε' (a - a)

Tactic:
rwa [sub_self, gronwallBound_x0]

Premises used: sub_self, gronwallBound_x0
-- Module: Mathlib.Analysis.ODE.Gronwall
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ε' : ε < ε'
⊢ ∀ (x : ℝ), HasDerivAt (fun (x : ℝ) ↦ gronwallBound δ K ε' (x - a)) (K * gronwallBound δ K ε' (x - a) + ε') x

Tactic:
fun x => hasDerivAt_gronwallBound_shift δ K ε' x a

Premises used: hasDerivAt_gronwallBound_shift
-- Module: Mathlib.Analysis.ODE.Gronwall
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ε' : ε < ε'
⊢ ∀ (x : ℝ), HasDerivAt (fun (x : ℝ) ↦ gronwallBound δ K ε' (x - a)) (K * gronwallBound δ K ε' (x - a) + ε') x

Tactic:
exact fun x => hasDerivAt_gronwallBound_shift δ K ε' x a

Premises used: hasDerivAt_gronwallBound_shift
-- Module: Mathlib.Analysis.ODE.Gronwall
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ε' : ε < ε'
⊢ ∀ x ∈ Ico a b, f x = gronwallBound δ K ε' (x - a) → f' x < K * gronwallBound δ K ε' (x - a) + ε'

Tactic:
grind
-- Module: Mathlib.Analysis.ODE.Gronwall
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ε' : ε < ε'
⊢ x ∈ Icc a b

Tactic:
hx
-- Module: Mathlib.Analysis.ODE.Gronwall
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ε' : ε < ε'
⊢ x ∈ Icc a b

Tactic:
exact hx
-- Module: Mathlib.Analysis.ODE.Gronwall
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, ∀ ε' ∈ 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
-- Module: Mathlib.Analysis.ODE.Gronwall
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 ≤ gronwallBound δ K ε (x - a)

Tactic:
continuousWithinAt_const.closure_le _ _ (H x hx)

Premises used: ContinuousWithinAt.closure_le, continuousWithinAt_const
-- Module: Mathlib.Analysis.ODE.Gronwall
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 ε)
convert_3 : ContinuousWithinAt (Y := ℝ) (fun (y : ℝ) ↦ gronwallBound δ K y (x - a)) (Ioi ε) ε
⊢ f x ≤ (fun (ε' : ℝ) ↦ gronwallBound δ K ε' (x - a)) ε

Tactic:
convert! continuousWithinAt_const.closure_le _ _ (H x hx)

Premises used: ContinuousWithinAt.closure_le, continuousWithinAt_const
-- Module: Mathlib.Analysis.ODE.Gronwall
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
⊢ ε ∈ closure (Ioi ε)

Tactic:
simp only [closure_Ioi, self_mem_Ici]

Premises used: Set.self_mem_Ici, closure_Ioi
-- Module: Mathlib.Analysis.ODE.Gronwall
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
⊢ ContinuousWithinAt (Y := ℝ) (fun (y : ℝ) ↦ gronwallBound δ K y (x - a)) (Ioi ε) ε

Tactic:
(gronwallBound_continuous_ε δ K (x - a)).continuousWithinAt

Premises used: HSub.hSub, gronwallBound_continuous_ε, Continuous.continuousWithinAt
-- Module: Mathlib.Analysis.ODE.Gronwall
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
⊢ ContinuousWithinAt (Y := ℝ) (fun (y : ℝ) ↦ gronwallBound δ K y (x - a)) (Ioi ε) ε

Tactic:
exact (gronwallBound_continuous_ε δ K (x - a)).continuousWithinAt

Premises used: HSub.hSub, gronwallBound_continuous_ε, Continuous.continuousWithinAt
-- Module: Mathlib.Analysis.ODE.Gronwall
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‖ ≤ δ
bound : ∀ x ∈ Ico a b, ‖f' x‖ ≤ K * ‖f x‖ + ε
⊢ ∀ x ∈ Icc a b, ‖f x‖ ≤ gronwallBound δ K ε (x - a)

Tactic:
le_gronwallBound_of_liminf_deriv_right_le (continuous_norm.comp_continuousOn hf)
    (fun x hx _r hr => (hf' x hx).liminf_right_slope_norm_le hr) ha bound

Premises used: HasDerivWithinAt.liminf_right_slope_norm_le, Continuous.comp_continuousOn, le_gronwallBound_of_liminf_deriv_right_le, continuous_norm
-- Module: Mathlib.Analysis.ODE.Gronwall
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
apply : ‖f x‖ ≤ 0
⊢ f x = 0

Tactic:
apply norm_le_zero_iff.mp

Premises used: norm_le_zero_iff, Iff.mp
-- Module: Mathlib.Analysis.ODE.Gronwall
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 a‖ ≤ 0

Tactic:
simp [ha]
-- Module: Mathlib.Analysis.ODE.Gronwall
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
⊢ ∀ x ∈ Ico a b, ‖f' x‖ ≤ K * ‖f x‖ + 0

Tactic:
simpa using bound
-- Module: Mathlib.Analysis.ODE.Gronwall
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
rw rw₁ : Eq (α := ℝ) 0 0
⊢ gronwallBound 0 K 0 (x - a) = 0

Tactic:
rw [gronwallBound_ε0_δ0]

Premises used: gronwallBound_ε0_δ0
-- Module: Mathlib.Analysis.ODE.Gronwall
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
calc : gronwallBound 0 K 0 (x - a) = 0
⊢ ‖f x‖ ≤ 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]

Premises used: gronwallBound, HSub.hSub, norm_le_gronwallBound_of_norm_deriv_right_le, OfNat.ofNat
-- Module: Mathlib.Analysis.ODE.Gronwall
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) ≤ δ
simp : ∀ (ha : ‖f a - g a‖ ≤ δ), ∀ t ∈ Icc a b, ‖f t - g t‖ ≤ gronwallBound δ (↑K : ℝ) (εf + εg) (t - a)
⊢ ∀ t ∈ Icc a b, dist (f t) (g t) ≤ gronwallBound δ (↑K : ℝ) (εf + εg) (t - a)

Tactic:
simp only [dist_eq_norm] at ha ⊢

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.ODE.Gronwall
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 ∈ 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)
-- Module: Mathlib.Analysis.ODE.Gronwall
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
apply : ∀ x ∈ Ico a b, ‖f' x - g' x‖ ≤ (↑K : ℝ) * ‖f x - g x‖ + (εf + εg)
⊢ ∀ t ∈ Icc a b, ‖f t - g t‖ ≤ gronwallBound δ (↑K : ℝ) (εf + εg) (t - a)

Tactic:
apply norm_le_gronwallBound_of_norm_deriv_right_le (hf.sub hg) h_deriv ha

Premises used: ContinuousOn.sub, norm_le_gronwallBound_of_norm_deriv_right_le
-- Module: Mathlib.Analysis.ODE.Gronwall
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
⊢ 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))
-- Module: Mathlib.Analysis.ODE.Gronwall
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))
⊢ 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)
-- Module: Mathlib.Analysis.ODE.Gronwall
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_1 : 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))
this : dist (v t (f t)) (v t (g t)) ≤ (↑K : ℝ) * dist (f t) (g t)
⊢ ‖f' t - g' t‖ ≤ (↑K : ℝ) * ‖f t - g t‖ + (εf + εg)

Tactic:
grind [dist_eq_norm]

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
K : ℝ≥0
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hv : ∀ (t : ℝ), LipschitzWith K (v 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
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
ha : dist (f a) (g a) ≤ δ
⊢ ∀ t ∈ Icc a b, dist (f t) (g t) ≤ gronwallBound δ (↑K : ℝ) (εf + εg) (t - a)

Tactic:
have hfs : ∀ t ∈ Ico a b, f t ∈ @univ E := fun _ _ => trivial
  dist_le_of_approx_trajectories_ODE_of_mem (fun t _ => (hv t).lipschitzOnWith) hf hf'
    f_bound hfs hg hg' g_bound (fun _ _ => trivial) ha

Premises used: trivial, dist_le_of_approx_trajectories_ODE_of_mem, LipschitzWith.lipschitzOnWith
-- Module: Mathlib.Analysis.ODE.Gronwall
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
rw rw₁ : LE.le (α := ℝ) 0 0
⊢ dist (v t (f t)) (v t (f t)) ≤ 0

Tactic:
rw [dist_self]

Premises used: dist_self
-- Module: Mathlib.Analysis.ODE.Gronwall
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 ∈ 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]
-- Module: Mathlib.Analysis.ODE.Gronwall
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
rw rw₁ : LE.le (α := ℝ) 0 0
⊢ dist (v t (g t)) (v t (g t)) ≤ 0

Tactic:
rw [dist_self]

Premises used: dist_self