awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → (hx : x ∈ closedBall x₀ (↑r : ℝ)) → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : (x : E) → (t : ℝ) → E := fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
hα' : α' = fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
x : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
t : ℝ
ht : t ∈ Icc tmin tmax
refine_2 :
  HasDerivWithinAt (if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0)
    (f t ((if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0) t)) (Icc tmin tmax) t
⊢ HasDerivWithinAt ((fun (x : E) ↦ (if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0 : (t : ℝ) → E)) x)
    (f t ((fun (x : E) ↦ (if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0 : (t : ℝ) → E)) x t))
    (Icc tmin tmax) t

Tactic:
beta_reduce
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → (hx : x ∈ closedBall x₀ (↑r : ℝ)) → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : (x : E) → (t : ℝ) → E := fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
hα' : α' = fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
x : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
t : ℝ
ht : t ∈ Icc tmin tmax
refine_2 : HasDerivWithinAt (α x hx).compProj (f t ((α x hx).toFun (projIcc tmin tmax ⋯ t))) (Icc tmin tmax) t
⊢ HasDerivWithinAt (if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0)
    (f t ((if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0) t)) (Icc tmin tmax) t

Tactic:
rw [dif_pos hx, FunSpace.compProj_apply]

Premises used: dif_pos, ODE.FunSpace.compProj_apply
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → (hx : x ∈ closedBall x₀ (↑r : ℝ)) → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : (x : E) → (t : ℝ) → E := fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
hα' : α' = fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
x : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
t : ℝ
ht : t ∈ Icc tmin tmax
apply : ∀ x_1 ∈ Icc tmin tmax, (α x hx).compProj x_1 = picard f (↑t₀ : ℝ) x (α x hx).compProj x_1
⊢ HasDerivWithinAt (α x hx).compProj (f t ((α x hx).toFun (projIcc tmin tmax ⋯ t))) (Icc tmin tmax) t

Tactic:
apply hasDerivWithinAt_picard_Icc t₀.2 hf.continuousOn_uncurry
      (α x hx |>.continuous_compProj.continuousOn)
      (fun _ ht' ↦ α x hx |>.compProj_mem_closedBall hf.mul_max_le)
      x ht |>.congr_of_mem _ ht

Premises used: HasDerivWithinAt.congr_of_mem, Continuous.continuousOn, IsPicardLindelof.continuousOn_uncurry, ODE.hasDerivWithinAt_picard_Icc, ODE.FunSpace.continuous_compProj, IsPicardLindelof.mul_max_le, ODE.FunSpace.compProj_mem_closedBall, Subtype.property
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → (hx : x ∈ closedBall x₀ (↑r : ℝ)) → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : (x : E) → (t : ℝ) → E := fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
hα' : α' = fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
x : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
t : ℝ
ht : t ∈ Icc tmin tmax
t' : ℝ
ht' : t' ∈ Icc tmin tmax
nth_rw : (FunSpace.next hf hx (α x hx)).compProj t' = picard f (↑t₀ : ℝ) x (α x hx).compProj t'
⊢ (α x hx).compProj t' = picard f (↑t₀ : ℝ) x (α x hx).compProj t'

Tactic:
nth_rw 1 [← hα]
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → (hx : x ∈ closedBall x₀ (↑r : ℝ)) → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : (x : E) → (t : ℝ) → E := fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
hα' : α' = fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
x : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
t : ℝ
ht : t ∈ Icc tmin tmax
t' : ℝ
ht' : t' ∈ Icc tmin tmax
rw :
  (FunSpace.next hf hx (α x hx)).toFun (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t' ht') =
    picard f (↑t₀ : ℝ) x (α x hx).compProj t'
rw₁ rw₂ :
  picard f (↑t₀ : ℝ) x (α x hx).compProj (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t' ht') : ℝ) =
    picard f (↑t₀ : ℝ) x (α x hx).compProj t'
⊢ (FunSpace.next hf hx (α x hx)).compProj t' = picard f (↑t₀ : ℝ) x (α x hx).compProj t'

Tactic:
rw [FunSpace.compProj_of_mem ht', FunSpace.next_apply]

Premises used: ODE.FunSpace.next_apply, ODE.FunSpace.compProj_of_mem
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → (hx : x ∈ closedBall x₀ (↑r : ℝ)) → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : (x : E) → (t : ℝ) → E := fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
hα' : α' = fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
refine_3 :
  ∀ (L' : ℝ≥0)
    (h :
      ∀ (x y : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)) (hy : y ∈ closedBall x₀ (↑r : ℝ)) (α β : FunSpace t₀ x₀ r L),
        IsFixedPt (FunSpace.next hf hx) α → IsFixedPt (FunSpace.next hf hy) β → dist α β ≤ (↑L' : ℝ) * dist x y),
    ∃ (L' : ℝ≥0), ∀ t ∈ Icc tmin tmax, LipschitzOnWith (β := E) L' (fun (x : E) ↦ α' x t) (closedBall x₀ (↑r : ℝ))
⊢ ∃ (L' : ℝ≥0), ∀ t ∈ Icc tmin tmax, LipschitzOnWith (β := E) L' (fun (x : E) ↦ α' x t) (closedBall x₀ (↑r : ℝ))

Tactic:
obtain ⟨L', h⟩ := FunSpace.exists_forall_closedBall_funSpace_dist_le_mul hf

Premises used: ODE.FunSpace.exists_forall_closedBall_funSpace_dist_le_mul
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → (hx : x ∈ closedBall x₀ (↑r : ℝ)) → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : (x : E) → (t : ℝ) → E := fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
hα' : α' = fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
L' : ℝ≥0
h :
  ∀ (x y : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)) (hy : y ∈ closedBall x₀ (↑r : ℝ)) (α β : FunSpace t₀ x₀ r L),
    IsFixedPt (FunSpace.next hf hx) α → IsFixedPt (FunSpace.next hf hy) β → dist α β ≤ (↑L' : ℝ) * dist x y
⊢ ∃ (L' : ℝ≥0), ∀ t ∈ Icc tmin tmax, LipschitzOnWith (β := E) L' (fun (x : E) ↦ α' x t) (closedBall x₀ (↑r : ℝ))

Tactic:
⟨L', fun t ht ↦ LipschitzOnWith.of_dist_le_mul fun x hx y hy ↦ ?_⟩

Premises used: LipschitzOnWith.of_dist_le_mul, Exists.intro
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → (hx : x ∈ closedBall x₀ (↑r : ℝ)) → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : (x : E) → (t : ℝ) → E := fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
hα' : α' = fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
L' : ℝ≥0
h :
  ∀ (x y : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)) (hy : y ∈ closedBall x₀ (↑r : ℝ)) (α β : FunSpace t₀ x₀ r L),
    IsFixedPt (FunSpace.next hf hx) α → IsFixedPt (FunSpace.next hf hy) β → dist α β ≤ (↑L' : ℝ) * dist x y
refine_3 :
  ∀ (t : ℝ) (ht : t ∈ Icc tmin tmax) (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)) (y : E)
    (hy : y ∈ closedBall x₀ (↑r : ℝ)), dist (α' x t) (α' y t) ≤ (↑L' : ℝ) * dist x y
⊢ ∃ (L' : ℝ≥0), ∀ t ∈ Icc tmin tmax, LipschitzOnWith (β := E) L' (fun (x : E) ↦ α' x t) (closedBall x₀ (↑r : ℝ))

Tactic:
refine ⟨L', fun t ht ↦ LipschitzOnWith.of_dist_le_mul fun x hx y hy ↦ ?_⟩
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → (hx : x ∈ closedBall x₀ (↑r : ℝ)) → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : (x : E) → (t : ℝ) → E := fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
hα' : α' = fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
L' : ℝ≥0
h :
  ∀ (x y : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)) (hy : y ∈ closedBall x₀ (↑r : ℝ)) (α β : FunSpace t₀ x₀ r L),
    IsFixedPt (FunSpace.next hf hx) α → IsFixedPt (FunSpace.next hf hy) β → dist α β ≤ (↑L' : ℝ) * dist x y
t : ℝ
ht : t ∈ Icc tmin tmax
x : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
y : E
hy : y ∈ closedBall x₀ (↑r : ℝ)
refine_3 :
  dist.{u_1} (α := E) ((if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0) t)
      ((if hx : y ∈ closedBall x₀ (↑r : ℝ) then (α y hx).compProj else 0) t) ≤
    (↑L' : ℝ) * dist x y
⊢ dist (α' x t) (α' y t) ≤ (↑L' : ℝ) * dist x y

Tactic:
simp_rw [hα']
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → (hx : x ∈ closedBall x₀ (↑r : ℝ)) → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : (x : E) → (t : ℝ) → E := fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
hα' : α' = fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
L' : ℝ≥0
h :
  ∀ (x y : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)) (hy : y ∈ closedBall x₀ (↑r : ℝ)) (α β : FunSpace t₀ x₀ r L),
    IsFixedPt (FunSpace.next hf hx) α → IsFixedPt (FunSpace.next hf hy) β → dist α β ≤ (↑L' : ℝ) * dist x y
t : ℝ
ht : t ∈ Icc tmin tmax
x : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
y : E
hy : y ∈ closedBall x₀ (↑r : ℝ)
refine_3 :
  dist (α := E)
      ((((FunSpace.toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) (α x hx) :
              C((↑(Icc tmin tmax) : Type), E)) :
            (a : (↑(Icc tmin tmax) : Type)) → E)
          (projIcc tmin tmax ⋯ t) :
        E)
      ((((FunSpace.toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) (α y hy) :
              C((↑(Icc tmin tmax) : Type), E)) :
            (a : (↑(Icc tmin tmax) : Type)) → E)
          (projIcc tmin tmax ⋯ t) :
        E) ≤
    (↑L' : ℝ) * dist x y
⊢ dist.{u_1} (α := E) ((if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0) t)
      ((if hx : y ∈ closedBall x₀ (↑r : ℝ) then (α y hx).compProj else 0) t) ≤
    (↑L' : ℝ) * dist x y

Tactic:
rw [dif_pos hx, dif_pos hy, FunSpace.compProj_apply, FunSpace.compProj_apply,
      ← FunSpace.toContinuousMap_apply_eq_apply, ← FunSpace.toContinuousMap_apply_eq_apply]

Premises used: dif_pos, ODE.FunSpace.toContinuousMap_apply_eq_apply, ODE.FunSpace.compProj_apply
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → (hx : x ∈ closedBall x₀ (↑r : ℝ)) → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : (x : E) → (t : ℝ) → E := fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
hα' : α' = fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
L' : ℝ≥0
h :
  ∀ (x y : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)) (hy : y ∈ closedBall x₀ (↑r : ℝ)) (α β : FunSpace t₀ x₀ r L),
    IsFixedPt (FunSpace.next hf hx) α → IsFixedPt (FunSpace.next hf hy) β → dist α β ≤ (↑L' : ℝ) * dist x y
t : ℝ
ht : t ∈ Icc tmin tmax
x : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
y : E
hy : y ∈ closedBall x₀ (↑r : ℝ)
⊢ Nonempty (↑(Icc tmin tmax) : Type)

Tactic:
have : Nonempty (Icc tmin tmax) := ⟨t₀⟩
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → (hx : x ∈ closedBall x₀ (↑r : ℝ)) → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : (x : E) → (t : ℝ) → E := fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
hα' : α' = fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
L' : ℝ≥0
h :
  ∀ (x y : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)) (hy : y ∈ closedBall x₀ (↑r : ℝ)) (α β : FunSpace t₀ x₀ r L),
    IsFixedPt (FunSpace.next hf hx) α → IsFixedPt (FunSpace.next hf hy) β → dist α β ≤ (↑L' : ℝ) * dist x y
t : ℝ
ht : t ∈ Icc tmin tmax
x : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
y : E
hy : y ∈ closedBall x₀ (↑r : ℝ)
this : Nonempty (↑(Icc tmin tmax) : Type)
refine_3 :
  dist (α := C((↑(Icc tmin tmax) : Type), E))
      ((FunSpace.toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) (α x hx) :
        C((↑(Icc tmin tmax) : Type), E))
      ((FunSpace.toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) (α y hy) :
        C((↑(Icc tmin tmax) : Type), E)) ≤
    (↑L' : ℝ) * dist x y
⊢ dist (α := E)
      ((((FunSpace.toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) (α x hx) :
              C((↑(Icc tmin tmax) : Type), E)) :
            (a : (↑(Icc tmin tmax) : Type)) → E)
          (projIcc tmin tmax ⋯ t) :
        E)
      ((((FunSpace.toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) (α y hy) :
              C((↑(Icc tmin tmax) : Type), E)) :
            (a : (↑(Icc tmin tmax) : Type)) → E)
          (projIcc tmin tmax ⋯ t) :
        E) ≤
    (↑L' : ℝ) * dist x y

Tactic:
apply ContinuousMap.dist_le_iff_of_nonempty.mp

Premises used: Iff.mp, ContinuousMap.dist_le_iff_of_nonempty
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → (hx : x ∈ closedBall x₀ (↑r : ℝ)) → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : (x : E) → (t : ℝ) → E := fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
hα' : α' = fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
L' : ℝ≥0
h :
  ∀ (x y : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)) (hy : y ∈ closedBall x₀ (↑r : ℝ)) (α β : FunSpace t₀ x₀ r L),
    IsFixedPt (FunSpace.next hf hx) α → IsFixedPt (FunSpace.next hf hy) β → dist α β ≤ (↑L' : ℝ) * dist x y
t : ℝ
ht : t ∈ Icc tmin tmax
x : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
y : E
hy : y ∈ closedBall x₀ (↑r : ℝ)
this : Nonempty (↑(Icc tmin tmax) : Type)
⊢ dist (α := C((↑(Icc tmin tmax) : Type), E))
      ((FunSpace.toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) (α x hx) :
        C((↑(Icc tmin tmax) : Type), E))
      ((FunSpace.toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) (α y hy) :
        C((↑(Icc tmin tmax) : Type), E)) ≤
    (↑L' : ℝ) * dist x y

Tactic:
h x y hx hy (α x hx) (α y hy) (hα x hx) (hα y hy)

Premises used: setOf
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : (x : E) → (hx : x ∈ closedBall x₀ (↑r : ℝ)) → FunSpace t₀ x₀ r L
hα : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), IsFixedPt (FunSpace.next hf hx) (α x hx)
α' : (x : E) → (t : ℝ) → E := fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
hα' : α' = fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
L' : ℝ≥0
h :
  ∀ (x y : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)) (hy : y ∈ closedBall x₀ (↑r : ℝ)) (α β : FunSpace t₀ x₀ r L),
    IsFixedPt (FunSpace.next hf hx) α → IsFixedPt (FunSpace.next hf hy) β → dist α β ≤ (↑L' : ℝ) * dist x y
t : ℝ
ht : t ∈ Icc tmin tmax
x : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
y : E
hy : y ∈ closedBall x₀ (↑r : ℝ)
this : Nonempty (↑(Icc tmin tmax) : Type)
⊢ dist (α := C((↑(Icc tmin tmax) : Type), E))
      ((FunSpace.toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) (α x hx) :
        C((↑(Icc tmin tmax) : Type), E))
      ((FunSpace.toContinuousMap : (a : FunSpace t₀ x₀ r L) → C((↑(Icc tmin tmax) : Type), E)) (α y hy) :
        C((↑(Icc tmin tmax) : Type), E)) ≤
    (↑L' : ℝ) * dist x y

Tactic:
exact h x y hx hy (α x hx) (α y hy) (hα x hx) (hα y hy)
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
obtain :
  ∀ (α : E → ℝ → E)
    (hα1 :
      ∀ x ∈ closedBall x₀ (↑r : ℝ),
        α x (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Icc tmin tmax) t)
    (L' : ℝ≥0) (hα2 : ∀ t ∈ Icc tmin tmax, LipschitzOnWith (β := E) L' (fun (x : E) ↦ α x t) (closedBall x₀ (↑r : ℝ))),
    ∃ (α : E × ℝ → E),
      (∀ x ∈ closedBall x₀ (↑r : ℝ),
          α (x, (↑t₀ : ℝ)) = x ∧
            ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (fun (x_1 : ℝ) ↦ α (x, x_1)) (f t (α (x, t))) (Icc tmin tmax) t) ∧
        ContinuousOn α (closedBall x₀ (↑r : ℝ) ×ˢ Icc tmin tmax)
⊢ ∃ (α : E × ℝ → E),
    (∀ x ∈ closedBall x₀ (↑r : ℝ),
        α (x, (↑t₀ : ℝ)) = x ∧
          ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (fun (x_1 : ℝ) ↦ α (x, x_1)) (f t (α (x, t))) (Icc tmin tmax) t) ∧
      ContinuousOn α (closedBall x₀ (↑r : ℝ) ×ˢ Icc tmin tmax)

Tactic:
obtain ⟨α, hα1, L', hα2⟩ := hf.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith

Premises used: IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : E → ℝ → E
hα1 :
  ∀ x ∈ closedBall x₀ (↑r : ℝ),
    α x (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Icc tmin tmax) t
L' : ℝ≥0
hα2 : ∀ t ∈ Icc tmin tmax, LipschitzOnWith (β := E) L' (fun (x : E) ↦ α x t) (closedBall x₀ (↑r : ℝ))
⊢ ∃ (α : E × ℝ → E),
    (∀ x ∈ closedBall x₀ (↑r : ℝ),
        α (x, (↑t₀ : ℝ)) = x ∧
          ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (fun (x_1 : ℝ) ↦ α (x, x_1)) (f t (α (x, t))) (Icc tmin tmax) t) ∧
      ContinuousOn α (closedBall x₀ (↑r : ℝ) ×ˢ Icc tmin tmax)

Tactic:
⟨uncurry α, hα1, ?_⟩

Premises used: And.intro, Exists.intro, Function.uncurry
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : E → ℝ → E
hα1 :
  ∀ x ∈ closedBall x₀ (↑r : ℝ),
    α x (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Icc tmin tmax) t
L' : ℝ≥0
hα2 : ∀ t ∈ Icc tmin tmax, LipschitzOnWith (β := E) L' (fun (x : E) ↦ α x t) (closedBall x₀ (↑r : ℝ))
refine : ContinuousOn (uncurry α) (closedBall x₀ (↑r : ℝ) ×ˢ Icc tmin tmax)
⊢ ∃ (α : E × ℝ → E),
    (∀ x ∈ closedBall x₀ (↑r : ℝ),
        α (x, (↑t₀ : ℝ)) = x ∧
          ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (fun (x_1 : ℝ) ↦ α (x, x_1)) (f t (α (x, t))) (Icc tmin tmax) t) ∧
      ContinuousOn α (closedBall x₀ (↑r : ℝ) ×ˢ Icc tmin tmax)

Tactic:
refine ⟨uncurry α, hα1, ?_⟩
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : E → ℝ → E
hα1 :
  ∀ x ∈ closedBall x₀ (↑r : ℝ),
    α x (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Icc tmin tmax) t
L' : ℝ≥0
hα2 : ∀ t ∈ Icc tmin tmax, LipschitzOnWith (β := E) L' (fun (x : E) ↦ α x t) (closedBall x₀ (↑r : ℝ))
apply : ∀ a ∈ closedBall x₀ (↑r : ℝ), ContinuousOn.{0, u_1} (Y := E) (fun (y : ℝ) ↦ uncurry α (a, y)) (Icc tmin tmax)
⊢ ContinuousOn (uncurry α) (closedBall x₀ (↑r : ℝ) ×ˢ Icc tmin tmax)

Tactic:
apply continuousOn_prod_of_continuousOn_lipschitzOnWith _ L' _ hα2

Premises used: continuousOn_prod_of_continuousOn_lipschitzOnWith
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : E → ℝ → E
hα1 :
  ∀ x ∈ closedBall x₀ (↑r : ℝ),
    α x (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Icc tmin tmax) t
L' : ℝ≥0
hα2 : ∀ t ∈ Icc tmin tmax, LipschitzOnWith (β := E) L' (fun (x : E) ↦ α x t) (closedBall x₀ (↑r : ℝ))
⊢ ∀ a ∈ closedBall x₀ (↑r : ℝ), ContinuousOn.{0, u_1} (Y := E) (fun (y : ℝ) ↦ uncurry α (a, y)) (Icc tmin tmax)

Tactic:
fun x hx ↦ HasDerivWithinAt.continuousOn (hα1 x hx).2

Premises used: And.right, HasDerivWithinAt.continuousOn
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ℝ → E → E
tmin tmax : ℝ
t₀ : (↑(Icc tmin tmax) : Type)
x₀ : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
α : E → ℝ → E
hα1 :
  ∀ x ∈ closedBall x₀ (↑r : ℝ),
    α x (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Icc tmin tmax) t
L' : ℝ≥0
hα2 : ∀ t ∈ Icc tmin tmax, LipschitzOnWith (β := E) L' (fun (x : E) ↦ α x t) (closedBall x₀ (↑r : ℝ))
⊢ ∀ a ∈ closedBall x₀ (↑r : ℝ), ContinuousOn.{0, u_1} (Y := E) (fun (y : ℝ) ↦ uncurry α (a, y)) (Icc tmin tmax)

Tactic:
exact fun x hx ↦ HasDerivWithinAt.continuousOn (hα1 x hx).2

Premises used: And.right, HasDerivWithinAt.continuousOn