awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∈ 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
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
t : ℝ
ht : t ∈ Ico (-b) (-a)
h : (Neg.neg ∘ v (-t)) ((g ∘ Neg.neg) t) = (ContinuousLinearMap.toSpanSingleton ℝ (v (-t) (g (-t))) : (a : ℝ) → E) (-1)
⊢ HasDerivWithinAt (g ∘ Neg.neg) ((Neg.neg ∘ v (-t)) ((g ∘ Neg.neg) t)) (Ici t) t

Tactic:
convert!
      HasFDerivWithinAt.comp_hasDerivWithinAt t (hg' (-t) (hmt2 ht))
        (hasDerivAt_neg t).hasDerivWithinAt (hmt3 t)

Premises used: HasDerivAt.hasDerivWithinAt, HasFDerivWithinAt.comp_hasDerivWithinAt, hasDerivAt_neg, Neg.neg
-- 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 ∈ 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
hv' : ∀ t ∈ Ico (-b) (-a), LipschitzOnWith K (Neg.neg ∘ v (-t)) (s (-t))
hmt1 : MapsTo Neg.neg (Icc (-b) (-a)) (Icc a b)
hmt2 : MapsTo Neg.neg (Ico (-b) (-a)) (Ioc a b)
hmt3 : ∀ (t : ℝ), MapsTo Neg.neg (Ici t) (Iic (-t))
t : ℝ
ht : t ∈ Ico (-b) (-a)
⊢ (Neg.neg ∘ v (-t)) ((g ∘ Neg.neg) t) = (ContinuousLinearMap.toSpanSingleton ℝ (v (-t) (g (-t))) : (a : ℝ) → E) (-1)

Tactic:
simp
-- 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 t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t
hfs : ∀ t ∈ Ioo a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t
hgs : ∀ t ∈ Ioo a b, g t ∈ s t
heq : f t₀ = g t₀
rw : EqOn f g (Icc a t₀ ∪ Icc t₀ b)
⊢ EqOn f g (Icc a b)

Tactic:
rw [← Icc_union_Icc_eq_Icc (le_of_lt ht.1) (le_of_lt ht.2)]

Premises used: Set.Icc_union_Icc_eq_Icc, le_of_lt, And.right, And.left
-- 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 t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t
hfs : ∀ t ∈ Ioo a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t
hgs : ∀ t ∈ Ioo a b, g t ∈ s t
heq : f t₀ = g t₀
h₁ : EqOn f g (Icc a t₀)
h₂ : EqOn f g (Icc t₀ b)
⊢ EqOn f g (Icc a t₀ ∪ Icc t₀ b)

Tactic:
apply EqOn.union

Premises used: Set.EqOn.union
-- 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 t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t
hfs : ∀ t ∈ Ioo a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t
hgs : ∀ t ∈ Ioo a b, g t ∈ s t
heq : f t₀ = g t₀
⊢ Ioc a t₀ ⊆ Ioo a b

Tactic:
have hss : Ioc a t₀ ⊆ Ioo a b := Ioc_subset_Ioo_right ht.2
-- 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 t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t
hfs : ∀ t ∈ Ioo a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t
hgs : ∀ t ∈ Ioo a b, g t ∈ s t
heq : f t₀ = g t₀
hss : Ioc a t₀ ⊆ Ioo a b
⊢ EqOn f g (Icc a t₀)

Tactic:
ODE_solution_unique_of_mem_Icc_left (fun t ht ↦ hv t (hss ht))
      (hf.mono <| Icc_subset_Icc_right <| le_of_lt ht.2)
      (fun _ ht' ↦ (hf' _ (hss ht')).hasDerivWithinAt) (fun _ ht' ↦ (hfs _ (hss ht')))
      (hg.mono <| Icc_subset_Icc_right <| le_of_lt ht.2)
      (fun _ ht' ↦ (hg' _ (hss ht')).hasDerivWithinAt) (fun _ ht' ↦ (hgs _ (hss ht'))) heq

Premises used: HasDerivAt.hasDerivWithinAt, Set.Icc_subset_Icc_right, le_of_lt, And.right, ContinuousOn.mono, ODE_solution_unique_of_mem_Icc_left
-- 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 t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t
hfs : ∀ t ∈ Ioo a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t
hgs : ∀ t ∈ Ioo a b, g t ∈ s t
heq : f t₀ = g t₀
hss : Ioc a t₀ ⊆ Ioo a b
⊢ EqOn f g (Icc a t₀)

Tactic:
exact ODE_solution_unique_of_mem_Icc_left (fun t ht ↦ hv t (hss ht))
      (hf.mono <| Icc_subset_Icc_right <| le_of_lt ht.2)
      (fun _ ht' ↦ (hf' _ (hss ht')).hasDerivWithinAt) (fun _ ht' ↦ (hfs _ (hss ht')))
      (hg.mono <| Icc_subset_Icc_right <| le_of_lt ht.2)
      (fun _ ht' ↦ (hg' _ (hss ht')).hasDerivWithinAt) (fun _ ht' ↦ (hgs _ (hss ht'))) heq

Premises used: HasDerivAt.hasDerivWithinAt, Set.Icc_subset_Icc_right, le_of_lt, And.right, ContinuousOn.mono, ODE_solution_unique_of_mem_Icc_left
-- 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 t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t
hfs : ∀ t ∈ Ioo a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t
hgs : ∀ t ∈ Ioo a b, g t ∈ s t
heq : f t₀ = g t₀
⊢ Ico t₀ b ⊆ Ioo a b

Tactic:
have hss : Ico t₀ b ⊆ Ioo a b := Ico_subset_Ioo_left ht.1
-- 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 t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t
hfs : ∀ t ∈ Ioo a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t
hgs : ∀ t ∈ Ioo a b, g t ∈ s t
heq : f t₀ = g t₀
hss : Ico t₀ b ⊆ Ioo a b
⊢ EqOn f g (Icc t₀ b)

Tactic:
ODE_solution_unique_of_mem_Icc_right (fun t ht ↦ hv t (hss ht))
      (hf.mono <| Icc_subset_Icc_left <| le_of_lt ht.1)
      (fun _ ht' ↦ (hf' _ (hss ht')).hasDerivWithinAt) (fun _ ht' ↦ (hfs _ (hss ht')))
      (hg.mono <| Icc_subset_Icc_left <| le_of_lt ht.1)
      (fun _ ht' ↦ (hg' _ (hss ht')).hasDerivWithinAt) (fun _ ht' ↦ (hgs _ (hss ht'))) heq

Premises used: HasDerivAt.hasDerivWithinAt, le_of_lt, Set.Icc_subset_Icc_left, ODE_solution_unique_of_mem_Icc_right, And.left, ContinuousOn.mono
-- 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 t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t
hfs : ∀ t ∈ Ioo a b, f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t
hgs : ∀ t ∈ Ioo a b, g t ∈ s t
heq : f t₀ = g t₀
hss : Ico t₀ b ⊆ Ioo a b
⊢ EqOn f g (Icc t₀ b)

Tactic:
exact ODE_solution_unique_of_mem_Icc_right (fun t ht ↦ hv t (hss ht))
      (hf.mono <| Icc_subset_Icc_left <| le_of_lt ht.1)
      (fun _ ht' ↦ (hf' _ (hss ht')).hasDerivWithinAt) (fun _ ht' ↦ (hfs _ (hss ht')))
      (hg.mono <| Icc_subset_Icc_left <| le_of_lt ht.1)
      (fun _ ht' ↦ (hg' _ (hss ht')).hasDerivWithinAt) (fun _ ht' ↦ (hgs _ (hss ht'))) heq

Premises used: HasDerivAt.hasDerivWithinAt, le_of_lt, Set.Icc_subset_Icc_left, ODE_solution_unique_of_mem_Icc_right, And.left, ContinuousOn.mono
-- 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 t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t' : ℝ
ht' : t' ∈ Ioo a b
inl : ∀ (h : t' < t₀), f t' = g t'
inr : ∀ (h : t₀ ≤ t'), f t' = g t'
⊢ f t' = g t'

Tactic:
rcases lt_or_ge t' t₀ with (h | h)

Premises used: lt_or_ge
-- 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 t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t' : ℝ
ht' : t' ∈ Ioo a b
h : t' < t₀
⊢ Icc t' t₀ ⊆ Ioo a b

Tactic:
have hss : Icc t' t₀ ⊆ Ioo a b :=
      fun _ ht'' ↦ ⟨lt_of_lt_of_le ht'.1 ht''.1, lt_of_le_of_lt ht''.2 ht.2⟩
-- 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 t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t' : ℝ
ht' : t' ∈ Ioo a b
h : t' < t₀
hss : Icc t' t₀ ⊆ Ioo a b
⊢ f t' = g t'

Tactic:
ODE_solution_unique_of_mem_Icc_left
      (fun t'' ht'' ↦ hv t'' ((Ioc_subset_Icc_self.trans hss) ht''))
      (HasDerivAt.continuousOn fun _ ht'' ↦ (hf _ <| hss ht'').1)
      (fun _ ht'' ↦ (hf _ <| hss <| Ioc_subset_Icc_self ht'').1.hasDerivWithinAt)
      (fun _ ht'' ↦ (hf _ <| hss <| Ioc_subset_Icc_self ht'').2)
      (HasDerivAt.continuousOn fun _ ht'' ↦ (hg _ <| hss ht'').1)
      (fun _ ht'' ↦ (hg _ <| hss <| Ioc_subset_Icc_self ht'').1.hasDerivWithinAt)
      (fun _ ht'' ↦ (hg _ <| hss <| Ioc_subset_Icc_self ht'').2) heq
      ⟨le_rfl, le_of_lt h⟩

Premises used: HasDerivAt.hasDerivWithinAt, le_rfl, HasDerivAt.continuousOn, le_of_lt, Set.Ioc_subset_Icc_self, HasSubset.Subset.trans, And.right, And.left, And.intro, ODE_solution_unique_of_mem_Icc_left
-- 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 t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t' : ℝ
ht' : t' ∈ Ioo a b
h : t' < t₀
hss : Icc t' t₀ ⊆ Ioo a b
⊢ f t' = g t'

Tactic:
exact ODE_solution_unique_of_mem_Icc_left
      (fun t'' ht'' ↦ hv t'' ((Ioc_subset_Icc_self.trans hss) ht''))
      (HasDerivAt.continuousOn fun _ ht'' ↦ (hf _ <| hss ht'').1)
      (fun _ ht'' ↦ (hf _ <| hss <| Ioc_subset_Icc_self ht'').1.hasDerivWithinAt)
      (fun _ ht'' ↦ (hf _ <| hss <| Ioc_subset_Icc_self ht'').2)
      (HasDerivAt.continuousOn fun _ ht'' ↦ (hg _ <| hss ht'').1)
      (fun _ ht'' ↦ (hg _ <| hss <| Ioc_subset_Icc_self ht'').1.hasDerivWithinAt)
      (fun _ ht'' ↦ (hg _ <| hss <| Ioc_subset_Icc_self ht'').2) heq
      ⟨le_rfl, le_of_lt h⟩

Premises used: HasDerivAt.hasDerivWithinAt, le_rfl, HasDerivAt.continuousOn, le_of_lt, Set.Ioc_subset_Icc_self, HasSubset.Subset.trans, And.right, And.left, And.intro, ODE_solution_unique_of_mem_Icc_left
-- 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 t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t' : ℝ
ht' : t' ∈ Ioo a b
h : t₀ ≤ t'
⊢ Icc t₀ t' ⊆ Ioo a b

Tactic:
have hss : Icc t₀ t' ⊆ Ioo a b :=
      fun _ ht'' ↦ ⟨lt_of_lt_of_le ht.1 ht''.1, lt_of_le_of_lt ht''.2 ht'.2⟩
-- 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 t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t' : ℝ
ht' : t' ∈ Ioo a b
h : t₀ ≤ t'
hss : Icc t₀ t' ⊆ Ioo a b
⊢ f t' = g t'

Tactic:
ODE_solution_unique_of_mem_Icc_right
      (fun t'' ht'' ↦ hv t'' ((Ico_subset_Icc_self.trans hss) ht''))
      (HasDerivAt.continuousOn fun _ ht'' ↦ (hf _ <| hss ht'').1)
      (fun _ ht'' ↦ (hf _ <| hss <| Ico_subset_Icc_self ht'').1.hasDerivWithinAt)
      (fun _ ht'' ↦ (hf _ <| hss <| Ico_subset_Icc_self ht'').2)
      (HasDerivAt.continuousOn fun _ ht'' ↦ (hg _ <| hss ht'').1)
      (fun _ ht'' ↦ (hg _ <| hss <| Ico_subset_Icc_self ht'').1.hasDerivWithinAt)
      (fun _ ht'' ↦ (hg _ <| hss <| Ico_subset_Icc_self ht'').2) heq
      ⟨h, le_rfl⟩

Premises used: HasDerivAt.hasDerivWithinAt, le_rfl, HasDerivAt.continuousOn, Set.Ico_subset_Icc_self, ODE_solution_unique_of_mem_Icc_right, HasSubset.Subset.trans, And.right, And.left, And.intro
-- 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 t₀ : ℝ
hv : ∀ t ∈ Ioo a b, LipschitzOnWith K (v t) (s t)
ht : t₀ ∈ Ioo a b
hf : ∀ t ∈ Ioo a b, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ t ∈ Ioo a b, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t' : ℝ
ht' : t' ∈ Ioo a b
h : t₀ ≤ t'
hss : Icc t₀ t' ⊆ Ioo a b
⊢ f t' = g t'

Tactic:
exact ODE_solution_unique_of_mem_Icc_right
      (fun t'' ht'' ↦ hv t'' ((Ico_subset_Icc_self.trans hss) ht''))
      (HasDerivAt.continuousOn fun _ ht'' ↦ (hf _ <| hss ht'').1)
      (fun _ ht'' ↦ (hf _ <| hss <| Ico_subset_Icc_self ht'').1.hasDerivWithinAt)
      (fun _ ht'' ↦ (hf _ <| hss <| Ico_subset_Icc_self ht'').2)
      (HasDerivAt.continuousOn fun _ ht'' ↦ (hg _ <| hss ht'').1)
      (fun _ ht'' ↦ (hg _ <| hss <| Ico_subset_Icc_self ht'').1.hasDerivWithinAt)
      (fun _ ht'' ↦ (hg _ <| hss <| Ico_subset_Icc_self ht'').2) heq
      ⟨h, le_rfl⟩

Premises used: HasDerivAt.hasDerivWithinAt, le_rfl, HasDerivAt.continuousOn, Set.Ico_subset_Icc_self, ODE_solution_unique_of_mem_Icc_right, HasSubset.Subset.trans, And.right, And.left, And.intro
-- 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
t₀ : ℝ
hv : ∀ᶠ (t : ℝ) in 𝓝 t₀, LipschitzOnWith K (v t) (s t)
hf : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
obtain :
  ∀ (ε : ℝ) (hε : ε > 0)
    (h :
      ∀ y ∈ ball t₀ ε,
        LipschitzOnWith K (v y) (s y) ∧
          (HasDerivAt f (v y (f y)) y ∧ f y ∈ s y) ∧ HasDerivAt g (v y (g y)) y ∧ g y ∈ s y),
    f =ᶠ[𝓝 t₀] g
⊢ f =ᶠ[𝓝 t₀] g

Tactic:
obtain ⟨ε, hε, h⟩ := eventually_nhds_iff_ball.mp (hv.and (hf.and hg))

Premises used: Filter.Eventually.and, Iff.mp, Metric.eventually_nhds_iff_ball
-- 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
t₀ : ℝ
hv : ∀ᶠ (t : ℝ) in 𝓝 t₀, LipschitzOnWith K (v t) (s t)
hf : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
ε : ℝ
hε : ε > 0
h :
  ∀ y ∈ ball t₀ ε,
    LipschitzOnWith K (v y) (s y) ∧ (HasDerivAt f (v y (f y)) y ∧ f y ∈ s y) ∧ HasDerivAt g (v y (g y)) y ∧ g y ∈ s y
rw : ∃ s ∈ 𝓝 t₀, EqOn f g s
⊢ f =ᶠ[𝓝 t₀] g

Tactic:
rw [Filter.eventuallyEq_iff_exists_mem]

Premises used: Filter.eventuallyEq_iff_exists_mem
-- 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
t₀ : ℝ
hv : ∀ᶠ (t : ℝ) in 𝓝 t₀, LipschitzOnWith K (v t) (s t)
hf : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
ε : ℝ
hε : ε > 0
h :
  ∀ y ∈ ball t₀ ε,
    LipschitzOnWith K (v y) (s y) ∧ (HasDerivAt f (v y (f y)) y ∧ f y ∈ s y) ∧ HasDerivAt g (v y (g y)) y ∧ g y ∈ s y
⊢ ∃ s ∈ 𝓝 t₀, EqOn f g s

Tactic:
⟨ball t₀ ε, ball_mem_nhds _ hε, ?_⟩

Premises used: Metric.ball, Metric.ball_mem_nhds, And.intro, Exists.intro
-- 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
t₀ : ℝ
hv : ∀ᶠ (t : ℝ) in 𝓝 t₀, LipschitzOnWith K (v t) (s t)
hf : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
ε : ℝ
hε : ε > 0
h :
  ∀ y ∈ ball t₀ ε,
    LipschitzOnWith K (v y) (s y) ∧ (HasDerivAt f (v y (f y)) y ∧ f y ∈ s y) ∧ HasDerivAt g (v y (g y)) y ∧ g y ∈ s y
refine : EqOn f g (ball t₀ ε)
⊢ ∃ s ∈ 𝓝 t₀, EqOn f g s

Tactic:
refine ⟨ball t₀ ε, ball_mem_nhds _ hε, ?_⟩
-- 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
t₀ : ℝ
hv : ∀ᶠ (t : ℝ) in 𝓝 t₀, LipschitzOnWith K (v t) (s t)
hf : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
ε : ℝ
hε : ε > 0
h :
  ∀ y ∈ ball t₀ ε,
    LipschitzOnWith K (v y) (s y) ∧ (HasDerivAt f (v y (f y)) y ∧ f y ∈ s y) ∧ HasDerivAt g (v y (g y)) y ∧ g y ∈ s y
simp_rw :
  ∀
    (h :
      ∀ y ∈ Ioo (t₀ - ε) (t₀ + ε),
        LipschitzOnWith K (v y) (s y) ∧
          (HasDerivAt f (v y (f y)) y ∧ f y ∈ s y) ∧ HasDerivAt g (v y (g y)) y ∧ g y ∈ s y),
    EqOn f g (Ioo (t₀ - ε) (t₀ + ε))
⊢ EqOn f g (ball t₀ ε)

Tactic:
simp_rw [Real.ball_eq_Ioo] at *

Premises used: Real.ball_eq_Ioo
-- 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
t₀ : ℝ
hv : ∀ᶠ (t : ℝ) in 𝓝 t₀, LipschitzOnWith K (v t) (s t)
hf : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
ε : ℝ
hε : ε > 0
h :
  ∀ y ∈ Ioo (t₀ - ε) (t₀ + ε),
    LipschitzOnWith K (v y) (s y) ∧ (HasDerivAt f (v y (f y)) y ∧ f y ∈ s y) ∧ HasDerivAt g (v y (g y)) y ∧ g y ∈ s y
⊢ EqOn f g (Ioo (t₀ - ε) (t₀ + ε))

Tactic:
apply ODE_solution_unique_of_mem_Ioo (fun _ ht ↦ (h _ ht).1)
    (Real.ball_eq_Ioo t₀ ε ▸ mem_ball_self hε)
    (fun _ ht ↦ (h _ ht).2.1) (fun _ ht ↦ (h _ ht).2.2) heq

Premises used: ODE_solution_unique_of_mem_Ioo, And.right, And.left
-- Module: Mathlib.Analysis.ODE.Gronwall
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
v : ℝ → E → E
K : ℝ≥0
f g : ℝ → E
a b : ℝ
hv : ∀ (t : ℝ), LipschitzWith K (v t)
hf : ContinuousOn f (Icc a b)
hf' : ∀ t ∈ Ico a b, HasDerivWithinAt f (v t (f t)) (Ici t) t
hg : ContinuousOn g (Icc a b)
hg' : ∀ t ∈ Ico a b, HasDerivWithinAt g (v t (g t)) (Ici t) t
ha : f a = g a
⊢ EqOn f g (Icc a b)

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

Premises used: trivial, ODE_solution_unique_of_mem_Icc_right, 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
t₀ : ℝ
hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)
hf : ∀ (t : ℝ), HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ (t : ℝ), HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
h : ∀ (t : ℝ), f t = g t
⊢ f = g

Tactic:
ext 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 : ℝ → E
t₀ : ℝ
hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)
hf : ∀ (t : ℝ), HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ (t : ℝ), HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t : ℝ
h : t ∈ Ioo (min (-|t|) (-|t₀|) - 1) (max |t| |t₀| + 1) ∧ t₀ ∈ Ioo (min (-|t|) (-|t₀|) - 1) (max |t| |t₀| + 1)
⊢ ∃ (A : ℝ) (B : ℝ), t ∈ Ioo A B ∧ t₀ ∈ Ioo A B

Tactic:
use (min (-|t|) (-|t₀|) - 1), (max |t| |t₀| + 1)

Premises used: abs, HSub.hSub, HAdd.hAdd, Max.max, OfNat.ofNat, Neg.neg, Min.min
-- 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
t₀ : ℝ
hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)
hf : ∀ (t : ℝ), HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ (t : ℝ), HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t : ℝ
⊢ t ∈ Ioo (min (-|t|) (-|t₀|) - 1) (max |t| |t₀| + 1) ∧ t₀ ∈ Ioo (min (-|t|) (-|t₀|) - 1) (max |t| |t₀| + 1)

Tactic:
grind
-- 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
t₀ : ℝ
hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)
hf : ∀ (t : ℝ), HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ (t : ℝ), HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t : ℝ
h : ∀ (A B : ℝ) (Ht : t ∈ Ioo A B) (Ht₀ : t₀ ∈ Ioo A B), f t = g t
⊢ f t = g t

Tactic:
obtain ⟨A, B, Ht, Ht₀⟩ : ∃ A B, t ∈ Set.Ioo A B ∧ t₀ ∈ Set.Ioo A B := by
    use (min (-|t|) (-|t₀|) - 1), (max |t| |t₀| + 1)
    grind
-- 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
t₀ : ℝ
hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)
hf : ∀ (t : ℝ), HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ (t : ℝ), HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t A B : ℝ
Ht : t ∈ Ioo A B
Ht₀ : t₀ ∈ Ioo A B
⊢ f t = g t

Tactic:
ODE_solution_unique_of_mem_Ioo
    (fun t _ => hv t) Ht₀ (fun t _ => hf t) (fun t _ => hg t) heq Ht

Premises used: ODE_solution_unique_of_mem_Ioo
-- 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
t₀ : ℝ
hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)
hf : ∀ (t : ℝ), HasDerivAt f (v t (f t)) t ∧ f t ∈ s t
hg : ∀ (t : ℝ), HasDerivAt g (v t (g t)) t ∧ g t ∈ s t
heq : f t₀ = g t₀
t A B : ℝ
Ht : t ∈ Ioo A B
Ht₀ : t₀ ∈ Ioo A B
⊢ f t = g t

Tactic:
exact ODE_solution_unique_of_mem_Ioo
    (fun t _ => hv t) Ht₀ (fun t _ => hf t) (fun t _ => hg t) heq Ht

Premises used: ODE_solution_unique_of_mem_Ioo
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
α : ℝ → E
t₀ : ℝ
x₀ : E
t : ℝ
⊢ picard f t₀ x₀ α t = x₀ + ∫ (τ : ℝ) in t₀..t, f τ (α τ)

Tactic:
rfl

Premises used: ODE.picard, rfl
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
α : ℝ → E
t₀ : ℝ
x₀ : E
⊢ picard f t₀ x₀ α t₀ = x₀

Tactic:
simp
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E → E
α : ℝ → E
s : Set ℝ
u : Set E
n : WithTop ℕ∞
hf : ContDiffOn ℝ n (uncurry f) (s ×ˢ u)
hα : ContDiffOn ℝ n α s
hmem : ∀ t ∈ s, α t ∈ u
⊢ ContDiffOn.{0, 0, u_1} ℝ (F := ℝ × E) n (fun (t : ℝ) ↦ (t, α t)) s

Tactic:
fun_prop