-- Mathlib/Analysis/ODE/Gronwall.lean
theorem ODE_solution_unique_of_mem_Icc
    (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₀) :
    EqOn f g (Icc a b)

Proof state:
case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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₀
⊢ EqOn f g (Icc t₀ b)

Tactic:
have hss : Ico t₀ b ⊆ Ioo a b := Ico_subset_Ioo_left ht.1

Result:
case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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)

Proof state:
case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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₀
⊢ EqOn f g (Icc a t₀ ∪ Icc t₀ b)

Tactic:
apply EqOn.union

Result:
case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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₀
⊢ EqOn f g (Icc a t₀)

case h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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₀
⊢ EqOn f g (Icc t₀ b)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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₀
⊢ EqOn f g (Icc a b)

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

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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₀
⊢ EqOn f g (Icc a t₀ ∪ Icc t₀ b)

Proof state:
case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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₀
⊢ EqOn f g (Icc a t₀)

Tactic:
have hss : Ioc a t₀ ⊆ Ioo a b := Ioc_subset_Ioo_right ht.2

Result:
case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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₀)

Proof state:
case h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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

Result:
no goals