awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
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)
⊢ ∃ (α : E → ℝ → E),
    (∀ x ∈ closedBall x₀ (↑r : ℝ),
        α x (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Icc tmin tmax) t) ∧
      ∃ (L' : ℝ≥0), ∀ t ∈ Icc tmin tmax, LipschitzOnWith (β := E) L' (fun (x : E) ↦ α x t) (closedBall x₀ (↑r : ℝ))
have hα' : let α' : (x : E) → (t : ℝ) → E := fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0;
α' = fun (x : E) ↦ if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0
Tactic: set α' := fun (x : E) ↦ if hx : x ∈ closedBall x₀ r then
    α x hx |>.compProj else 0 with hα'
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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
⊢ ∃ (α : E → ℝ → E),
    (∀ x ∈ closedBall x₀ (↑r : ℝ),
        α x (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Icc tmin tmax) t) ∧
      ∃ (L' : ℝ≥0), ∀ t ∈ Icc tmin tmax, LipschitzOnWith (β := E) L' (fun (x : E) ↦ α x t) (closedBall x₀ (↑r : ℝ))
have refine_1 : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), α' x (↑t₀ : ℝ) = x
Tactic: refine ⟨α', fun x hx ↦ ⟨?_, fun t ht ↦ ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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_1 : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), α' x (↑t₀ : ℝ) = x
⊢ ∃ (α : E → ℝ → E),
    (∀ x ∈ closedBall x₀ (↑r : ℝ),
        α x (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Icc tmin tmax) t) ∧
      ∃ (L' : ℝ≥0), ∀ t ∈ Icc tmin tmax, LipschitzOnWith (β := E) L' (fun (x : E) ↦ α x t) (closedBall x₀ (↑r : ℝ))
have refine_2 : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)) (t : ℝ) (ht : t ∈ Icc tmin tmax),
  HasDerivWithinAt (α' x) (f t (α' x t)) (Icc tmin tmax) t
Tactic: refine ⟨α', fun x hx ↦ ⟨?_, fun t ht ↦ ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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_1 : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), α' x (↑t₀ : ℝ) = x
refine_2 :
  ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)) (t : ℝ) (ht : t ∈ Icc tmin tmax),
    HasDerivWithinAt (α' x) (f t (α' x t)) (Icc tmin tmax) t
⊢ ∃ (α : E → ℝ → E),
    (∀ x ∈ closedBall x₀ (↑r : ℝ),
        α x (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Icc tmin tmax) t) ∧
      ∃ (L' : ℝ≥0), ∀ t ∈ Icc tmin tmax, LipschitzOnWith (β := E) L' (fun (x : E) ↦ α x t) (closedBall x₀ (↑r : ℝ))
have refine_3 : ∃ (L' : ℝ≥0), ∀ t ∈ Icc tmin tmax, LipschitzOnWith (β := E) L' (fun (x : E) ↦ α' x t) (closedBall x₀ (↑r : ℝ))
Tactic: refine ⟨α', fun x hx ↦ ⟨?_, fun t ht ↦ ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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 : ℝ)
⊢ (if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0) (↑t₀ : ℝ) = x
have refine_1 : (α x hx).compProj (↑t₀ : ℝ) = x
Tactic: rw [dif_pos hx, FunSpace.compProj_val, ← hα, FunSpace.next_apply₀]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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 : ℝ)
refine_1 : (α x hx).compProj (↑t₀ : ℝ) = x
⊢ (if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0) (↑t₀ : ℝ) = x
have refine_1₁ : (α x hx).toFun t₀ = x
Tactic: rw [dif_pos hx, FunSpace.compProj_val, ← hα, FunSpace.next_apply₀]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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 : ℝ)
refine_1 : (α x hx).compProj (↑t₀ : ℝ) = x
refine_1₁ : (α x hx).toFun t₀ = x
⊢ (if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0) (↑t₀ : ℝ) = x
have refine_1₂ : (FunSpace.next hf hx (α x hx)).toFun t₀ = x
Tactic: rw [dif_pos hx, FunSpace.compProj_val, ← hα, FunSpace.next_apply₀]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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 : ℝ)
refine_1 : (α x hx).compProj (↑t₀ : ℝ) = x
refine_1₁ : (α x hx).toFun t₀ = x
refine_1₂ : (FunSpace.next hf hx (α x hx)).toFun t₀ = x
⊢ (if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0) (↑t₀ : ℝ) = x
have refine_1₃ : x = x
Tactic: rw [dif_pos hx, FunSpace.compProj_val, ← hα, FunSpace.next_apply₀]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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
⊢ 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
have refine_2 : HasDerivWithinAt (α x hx).compProj (f t ((α x hx).toFun (projIcc tmin tmax sorry t))) (Icc tmin tmax) t
Tactic: rw [dif_pos hx, FunSpace.compProj_apply]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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
⊢ HasDerivWithinAt (α x hx).compProj (f t ((α x hx).toFun (projIcc tmin tmax ⋯ t))) (Icc tmin tmax) t
have apply : ∀ x_1 ∈ Icc tmin tmax, (α x hx).compProj x_1 = picard f (↑t₀ : ℝ) x (α x hx).compProj x_1
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
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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
⊢ (α x hx).compProj t' = picard f (↑t₀ : ℝ) x (α x hx).compProj t'
have nth_rw : (FunSpace.next hf hx (α x hx)).compProj t' = picard f (↑t₀ : ℝ) x (α x hx).compProj t'
Tactic: nth_rw 1 [← hα]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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
⊢ (FunSpace.next hf hx (α x hx)).compProj t' = picard f (↑t₀ : ℝ) x (α x hx).compProj t'
have 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'
Tactic: rw [FunSpace.compProj_of_mem ht', FunSpace.next_apply]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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'
⊢ (FunSpace.next hf hx (α x hx)).compProj t' = picard f (↑t₀ : ℝ) x (α x hx).compProj t'
have 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'
Tactic: rw [FunSpace.compProj_of_mem ht', FunSpace.next_apply]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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), ∀ t ∈ Icc tmin tmax, LipschitzOnWith (β := E) L' (fun (x : E) ↦ α' x t) (closedBall x₀ (↑r : ℝ))
have 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 : ℝ))
Tactic: obtain ⟨L', h⟩ := FunSpace.exists_forall_closedBall_funSpace_dist_le_mul hf
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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 : ℝ))
have 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
Tactic: refine ⟨L', fun t ht ↦ LipschitzOnWith.of_dist_le_mul fun x hx y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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 : ℝ)
⊢ 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
have 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 sorry 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 sorry t) :
      E) ≤
  (↑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]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
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 : ℝ)
⊢ 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
have this : Nonempty (↑(Icc tmin tmax) : Type)
Tactic: have : Nonempty (Icc tmin tmax) := ⟨t₀⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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 (α := 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
have 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
Tactic: apply ContinuousMap.dist_le_iff_of_nonempty.mp
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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),
    (∀ 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)
have 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)
Tactic: obtain ⟨α, hα1, L', hα2⟩ := hf.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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)
have refine : ContinuousOn (uncurry α) (closedBall x₀ (↑r : ℝ) ×ˢ Icc tmin tmax)
Tactic: refine ⟨uncurry α, hα1, ?_⟩