awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
x : E
hx : x ∈ closedBall x₀ (a / 2)
x₁ : ‖f x - f x₀‖ + ‖f x₀‖ ≤ (↑K : ℝ) * ‖x - x₀‖ + ‖f x₀‖
x₂ : (↑K : ℝ) * ‖x - x₀‖ + ‖f x₀‖ ≤ (↑K : ℝ) * a + ‖f x₀‖
⊢ ‖f x‖ ≤ (↑K : ℝ) * a + ‖f x₀‖ + 1

Tactic:
calc
      ‖f x‖ ≤ ‖f x - f x₀‖ + ‖f x₀‖ := norm_le_norm_sub_add _ _
      _ ≤ K * ‖x - x₀‖ + ‖f x₀‖ := by
        gcongr
        apply hl.norm_sub_le _ (mem_of_mem_nhds hs)
        apply subset_trans _ has hx
        exact closedBall_subset_ball <| half_lt_self ha -- this is where we need `a / 2`
      _ ≤ K * a + ‖f x₀‖ := by
        gcongr
        rw [← mem_closedBall_iff_norm]
        exact closedBall_subset_closedBall (half_le_self (le_of_lt ha)) hx
      _ ≤ L := le_add_of_nonneg_right zero_le_one

Premises used: zero_le_one, norm_le_norm_sub_add, le_add_of_nonneg_right
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
⊢ ∀ (x : E) (hx : x ∈ closedBall x₀ (a / 2)), ‖f x‖ ≤ L

Tactic:
have hb (x : E) (hx : x ∈ closedBall x₀ (a / 2)) : ‖f x‖ ≤ L := by
    rw [hL]
    calc
      ‖f x‖ ≤ ‖f x - f x₀‖ + ‖f x₀‖ := norm_le_norm_sub_add _ _
      _ ≤ K * ‖x - x₀‖ + ‖f x₀‖ := by
        gcongr
        apply hl.norm_sub_le _ (mem_of_mem_nhds hs)
        apply subset_trans _ has hx
        exact closedBall_subset_ball <| half_lt_self ha -- this is where we need `a / 2`
      _ ≤ K * a + ‖f x₀‖ := by
        gcongr
        rw [← mem_closedBall_iff_norm]
        exact closedBall_subset_closedBall (half_le_self (le_of_lt ha)) hx
      _ ≤ L := le_add_of_nonneg_right zero_le_one
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
hb : ∀ (x : E) (hx : x ∈ closedBall x₀ (a / 2)), ‖f x‖ ≤ L
ε : ℝ := a / L / 2 / 2
⊢ 0 < ε

Tactic:
positivity
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
hb : ∀ (x : E) (hx : x ∈ closedBall x₀ (a / 2)), ‖f x‖ ≤ L
ε : ℝ := a / L / 2 / 2
⊢ 0 < ε

Tactic:
have hε0 : 0 < ε := by positivity
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
hb : ∀ (x : E) (hx : x ∈ closedBall x₀ (a / 2)), ‖f x‖ ≤ L
ε : ℝ := a / L / 2 / 2
hε0 : 0 < ε
⊢ ∃ (ε : ℝ) (hε : 0 < ε) (a : ℝ≥0) (r : ℝ≥0) (L : ℝ≥0) (K : ℝ≥0) (_ : 0 < r),
    ∀ (t₀ : ℝ),
      IsPicardLindelof (fun (x : ℝ) ↦ f) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r L K

Tactic:
⟨ε, hε0,
    .mk (a / 2) (half_pos ha).le, (.mk (a / 2) (half_pos ha).le) / 2,
    .mk L hL0.le, K, half_pos <| half_pos ha, fun t₀ ↦ ?_⟩

Premises used: half_pos, HDiv.hDiv, NNReal.mk, LT.lt.le, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
hb : ∀ (x : E) (hx : x ∈ closedBall x₀ (a / 2)), ‖f x‖ ≤ L
ε : ℝ := a / L / 2 / 2
hε0 : 0 < ε
refine :
  ∀ (t₀ : ℝ),
    IsPicardLindelof (fun (x : ℝ) ↦ f) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀
      (NNReal.mk (a / 2) ⋯) (NNReal.mk (a / 2) ⋯ / 2) (NNReal.mk L ⋯) K
⊢ ∃ (ε : ℝ) (hε : 0 < ε) (a : ℝ≥0) (r : ℝ≥0) (L : ℝ≥0) (K : ℝ≥0) (_ : 0 < r),
    ∀ (t₀ : ℝ),
      IsPicardLindelof (fun (x : ℝ) ↦ f) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r L K

Tactic:
refine ⟨ε, hε0,
    .mk (a / 2) (half_pos ha).le, (.mk (a / 2) (half_pos ha).le) / 2,
    .mk L hL0.le, K, half_pos <| half_pos ha, fun t₀ ↦ ?_⟩
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
hb : ∀ (x : E) (hx : x ∈ closedBall x₀ (a / 2)), ‖f x‖ ≤ L
ε : ℝ := a / L / 2 / 2
hε0 : 0 < ε
t₀ : ℝ
apply :
  (↑(NNReal.mk L ⋯) : ℝ) *
      max (t₀ + ε - (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) : ℝ))
        ((↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) : ℝ) - (t₀ - ε)) ≤
    (↑(NNReal.mk (a / 2) ⋯) : ℝ) - (↑(NNReal.mk (a / 2) ⋯ / 2) : ℝ)
⊢ IsPicardLindelof (fun (x : ℝ) ↦ f) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀
    (NNReal.mk (a / 2) ⋯) (NNReal.mk (a / 2) ⋯ / 2) (NNReal.mk L ⋯) K

Tactic:
apply of_time_independent hb <|
    hl.mono <| subset_trans (closedBall_subset_ball (half_lt_self ha)) has

Premises used: half_lt_self, LipschitzOnWith.mono, subset_trans, Metric.closedBall_subset_ball, IsPicardLindelof.of_time_independent
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
hb : ∀ (x : E) (hx : x ∈ closedBall x₀ (a / 2)), ‖f x‖ ≤ L
ε : ℝ := a / L / 2 / 2
hε0 : 0 < ε
t₀ : ℝ
simp : 1 ≤ HSub.hSub (α := ℝ) 2 1
⊢ (↑(NNReal.mk L ⋯) : ℝ) *
      max (t₀ + ε - (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) : ℝ))
        ((↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) : ℝ) - (t₀ - ε)) ≤
    (↑(NNReal.mk (a / 2) ⋯) : ℝ) - (↑(NNReal.mk (a / 2) ⋯ / 2) : ℝ)

Tactic:
simp [ε, field]
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
K : ℝ≥0
s : Set E
hs : s ∈ 𝓝 x₀
hl : LipschitzOnWith K f s
a : ℝ
ha : 0 < a
has : ball x₀ a ⊆ s
L : ℝ := (↑K : ℝ) * a + ‖f x₀‖ + 1
hL : L = (↑K : ℝ) * a + ‖f x₀‖ + 1
hL0 : 0 < L
hb : ∀ (x : E) (hx : x ∈ closedBall x₀ (a / 2)), ‖f x‖ ≤ L
ε : ℝ := a / L / 2 / 2
hε0 : 0 < ε
t₀ : ℝ
⊢ 1 ≤ HSub.hSub (α := ℝ) 2 1

Tactic:
norm_num
-- 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₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
obtain :
  ∀ (α : FunSpace t₀ x₀ r L) (hα : IsFixedPt (FunSpace.next hf hx) α),
    ∃ (α : ℝ → E), α (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, α t = picard f (↑t₀ : ℝ) x α t
⊢ ∃ (α : ℝ → E), α (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, α t = picard f (↑t₀ : ℝ) x α t

Tactic:
obtain ⟨α, hα⟩ := FunSpace.exists_isFixedPt_next hf hx

Premises used: ODE.FunSpace.exists_isFixedPt_next
-- 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₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
hα : IsFixedPt (FunSpace.next hf hx) α
⊢ (FunSpace.next hf hx α).compProj (↑t₀ : ℝ) = x

Tactic:
simp
-- 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₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
hα : IsFixedPt (FunSpace.next hf hx) α
refine :
  ∀ (t : ℝ) (ht : t ∈ Icc tmin tmax),
    (FunSpace.next hf hx α).compProj t = picard f (↑t₀ : ℝ) x (FunSpace.next hf hx α).compProj t
⊢ ∃ (α : ℝ → E), α (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, α t = picard f (↑t₀ : ℝ) x α t

Tactic:
refine ⟨(FunSpace.next hf hx α).compProj, by simp, fun t ht ↦ ?_⟩
-- 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₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
hα : IsFixedPt (FunSpace.next hf hx) α
t : ℝ
ht : t ∈ Icc tmin tmax
rw : (FunSpace.next hf hx α).toFun (projIcc tmin tmax ⋯ t) = picard f (↑t₀ : ℝ) x (FunSpace.next hf hx α).compProj t
rw₁ :
  picard f (↑t₀ : ℝ) x α.compProj (↑(projIcc tmin tmax ⋯ t) : ℝ) =
    picard f (↑t₀ : ℝ) x (FunSpace.next hf hx α).compProj t
rw₂ : picard f (↑t₀ : ℝ) x α.compProj (↑(projIcc tmin tmax ⋯ t) : ℝ) = picard f (↑t₀ : ℝ) x α.compProj t
rw₃ rw₄ :
  picard f (↑t₀ : ℝ) x α.compProj (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t ht) : ℝ) =
    picard f (↑t₀ : ℝ) x α.compProj t
⊢ (FunSpace.next hf hx α).compProj t = picard f (↑t₀ : ℝ) x (FunSpace.next hf hx α).compProj t

Tactic:
rw [FunSpace.compProj_apply, FunSpace.next_apply, hα, projIcc_of_mem _ ht]

Premises used: ODE.FunSpace.next_apply, Set.projIcc_of_mem, 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₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
obtain :
  ∀ (α : FunSpace t₀ x₀ r L) (hα : IsFixedPt (FunSpace.next hf hx) α),
    ∃ (α : ℝ → E), α (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
⊢ ∃ (α : ℝ → E), α (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t

Tactic:
obtain ⟨α, hα⟩ := FunSpace.exists_isFixedPt_next hf hx

Premises used: ODE.FunSpace.exists_isFixedPt_next
-- 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₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
hα : IsFixedPt (FunSpace.next hf hx) α
rw : α.toFun t₀ = x
rw₁ : (FunSpace.next hf hx α).toFun t₀ = x
rw₂ rw₃ : x = x
⊢ α.compProj (↑t₀ : ℝ) = x

Tactic:
rw [FunSpace.compProj_val, ← hα, FunSpace.next_apply₀]

Premises used: ODE.FunSpace.next_apply₀, ODE.FunSpace.compProj_val
-- 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₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
hα : IsFixedPt (FunSpace.next hf hx) α
refine : ∀ (t : ℝ) (ht : t ∈ Icc tmin tmax), HasDerivWithinAt α.compProj (f t (α.compProj t)) (Icc tmin tmax) t
⊢ ∃ (α : ℝ → E), α (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t

Tactic:
refine ⟨α.compProj, by rw [FunSpace.compProj_val, ← hα, FunSpace.next_apply₀], fun t ht ↦ ?_⟩
-- 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₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
hα : IsFixedPt (FunSpace.next hf hx) α
t : ℝ
ht : t ∈ Icc tmin tmax
apply : ∀ x_1 ∈ Icc tmin tmax, α.compProj x_1 = picard f (↑t₀ : ℝ) x α.compProj x_1
⊢ HasDerivWithinAt α.compProj (f t (α.compProj t)) (Icc tmin tmax) t

Tactic:
apply hasDerivWithinAt_picard_Icc t₀.2 hf.continuousOn_uncurry
    α.continuous_compProj.continuousOn (fun _ ht' ↦ α.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₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
hα : IsFixedPt (FunSpace.next hf hx) α
t : ℝ
ht : t ∈ Icc tmin tmax
t' : ℝ
ht' : t' ∈ Icc tmin tmax
nth_rw : (FunSpace.next hf hx α).compProj t' = picard f (↑t₀ : ℝ) x α.compProj t'
⊢ α.compProj t' = picard f (↑t₀ : ℝ) x α.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₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : FunSpace t₀ x₀ r L
hα : IsFixedPt (FunSpace.next hf hx) α
t : ℝ
ht : t ∈ Icc tmin tmax
t' : ℝ
ht' : t' ∈ Icc tmin tmax
rw :
  (FunSpace.next hf hx α).toFun (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t' ht') =
    picard f (↑t₀ : ℝ) x α.compProj t'
rw₁ rw₂ :
  picard f (↑t₀ : ℝ) x α.compProj (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t' ht') : ℝ) =
    picard f (↑t₀ : ℝ) x α.compProj t'
⊢ (FunSpace.next hf hx α).compProj t' = picard f (↑t₀ : ℝ) x α.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 L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a 0 L K
⊢ ∃ (α : ℝ → E), α (↑t₀ : ℝ) = x₀ ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t

Tactic:
exists_eq_forall_mem_Icc_hasDerivWithinAt hf (mem_closedBall_self le_rfl)

Premises used: le_rfl, IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt, Metric.mem_closedBall_self
-- 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), IsFixedPt (FunSpace.next hf hx) α

Tactic:
have (x) (hx : x ∈ closedBall x₀ r) := FunSpace.exists_isFixedPt_next hf hx
-- 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
this : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ∃ (α : FunSpace t₀ x₀ r L), IsFixedPt (FunSpace.next hf hx) α
choose :
  ∀ (α : (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 : ℝ))
⊢ ∃ (α : 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 : ℝ))

Tactic:
choose α hα using this
-- 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)
⊢ 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α'

Premises used: Membership.mem, dite, ODE.FunSpace.compProj, Metric.closedBall, OfNat.ofNat, NNReal.toReal
-- 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
⊢ ∃ (α : 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 : ℝ))

Tactic:
⟨α', fun x hx ↦ ⟨?_, fun t ht ↦ ?_⟩, ?_⟩

Premises used: And.intro, 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
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
refine_3 :
  ∃ (L' : ℝ≥0), ∀ 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 (α 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 : ℝ))

Tactic:
refine ⟨α', fun x hx ↦ ⟨?_, fun t ht ↦ ?_⟩, ?_⟩
-- 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 : ℝ)
refine_1 :
  (fun (x : E) ↦ (if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0 : (t : ℝ) → E)) x (↑t₀ : ℝ) = x
⊢ α' x (↑t₀ : ℝ) = x

Tactic:
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
x : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
refine_1 : (if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0) (↑t₀ : ℝ) = x
⊢ (fun (x : E) ↦ (if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0 : (t : ℝ) → E)) x (↑t₀ : ℝ) = x

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 : ℝ)
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
refine_1₃ refine_1₄ : x = x
⊢ (if hx : x ∈ closedBall x₀ (↑r : ℝ) then (α x hx).compProj else 0) (↑t₀ : ℝ) = x

Tactic:
rw [dif_pos hx, FunSpace.compProj_val, ← hα, FunSpace.next_apply₀]

Premises used: dif_pos, ODE.FunSpace.next_apply₀, ODE.FunSpace.compProj_val
-- 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 ((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
⊢ HasDerivWithinAt (α' x) (f t (α' x t)) (Icc tmin tmax) t

Tactic:
rw [hα']