awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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
⊢ ∃ (ε : ℝ) (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
have obtain : ∀ (a : ℝ) (ha : 0 < a) (has : ball x₀ a ⊆ s),
  ∃ (ε : ℝ) (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₀ sorry) x₀ a r L K
Tactic: obtain ⟨a, ha : 0 < a, has⟩ := Metric.mem_nhds_iff.mp hs
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
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
⊢ ∃ (ε : ℝ) (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
have hL : let L := (↑K : ℝ) * a + ‖f x₀‖ + 1;
L = (↑K : ℝ) * a + ‖f x₀‖ + 1
Tactic: set L := K * a + ‖f x₀‖ + 1 with hL
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
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
⊢ ∃ (ε : ℝ) (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
have hL0 : 0 < L
Tactic: have hL0 : 0 < L := by positivity
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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 - f x₀‖ + ‖f x₀‖ ≤ (↑K : ℝ) * ‖x - x₀‖ + ‖f x₀‖
have bc : ‖f x - f x₀‖ ≤ (↑K : ℝ) * ‖x - x₀‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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 - f x₀‖ ≤ (↑K : ℝ) * ‖x - x₀‖
have apply : x ∈ s
Tactic: apply hl.norm_sub_le _ (mem_of_mem_nhds hs)
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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 ∈ s
have apply : closedBall x₀ (a / 2) ⊆ ball x₀ a
Tactic: apply subset_trans _ has hx
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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)
⊢ (↑K : ℝ) * ‖x - x₀‖ + ‖f x₀‖ ≤ (↑K : ℝ) * a + ‖f x₀‖
have bc : ‖x - x₀‖ ≤ a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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 - x₀‖ ≤ a
have bc : x ∈ closedBall x₀ a
Tactic: rw [← mem_closedBall_iff_norm]
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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‖ ≤ (↑K : ℝ) * a + ‖f x₀‖ + 1
have x₁ : ‖f x - f x₀‖ + ‖f x₀‖ ≤ (↑K : ℝ) * ‖x - x₀‖ + ‖f x₀‖
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
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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₀‖
⊢ ‖f x‖ ≤ (↑K : ℝ) * a + ‖f x₀‖ + 1
have x₂ : (↑K : ℝ) * ‖x - x₀‖ + ‖f x₀‖ ≤ (↑K : ℝ) * a + ‖f x₀‖
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
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
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
⊢ ∃ (ε : ℝ) (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
have hb : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (hypothesis)
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 < ε) (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
have hε0 : 0 < ε
Tactic: have hε0 : 0 < ε := by positivity
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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
have refine : ∀ (t₀ : ℝ),
  IsPicardLindelof (fun (x : ℝ) ↦ f) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ sorry) x₀
    (NNReal.mk (a / 2) sorry) (NNReal.mk (a / 2) sorry / 2) (NNReal.mk L sorry) 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₀ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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₀ : ℝ
⊢ 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
have apply : (↑(NNReal.mk L sorry) : ℝ) *
    max (t₀ + ε - (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ sorry) : ℝ))
      ((↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ sorry) : ℝ) - (t₀ - ε)) ≤
  (↑(NNReal.mk (a / 2) sorry) : ℝ) - (↑(NNReal.mk (a / 2) sorry / 2) : ℝ)
Tactic: apply of_time_independent hb <|
    hl.mono <| subset_trans (closedBall_subset_ball (half_lt_self ha)) has
-- Lean 4 proof step from Mathlib.Analysis.ODE.PicardLindelof (goal)
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₀ : ℝ
⊢ (↑(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) : ℝ)
have simp : 1 ≤ HSub.hSub (α := ℝ) 2 1
Tactic: simp [ε, field]
-- 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₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
⊢ ∃ (α : ℝ → E), α (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, α t = picard f (↑t₀ : ℝ) x α t
have 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
Tactic: obtain ⟨α, hα⟩ := FunSpace.exists_isFixedPt_next hf hx
-- 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₀ 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) α
⊢ ∃ (α : ℝ → E), α (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, α t = picard f (↑t₀ : ℝ) x α t
have refine : ∀ (t : ℝ) (ht : t ∈ Icc tmin tmax),
  (FunSpace.next hf hx α).compProj t = picard f (↑t₀ : ℝ) x (FunSpace.next hf hx α).compProj t
Tactic: refine ⟨(FunSpace.next hf hx α).compProj, by simp, 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₀ 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
⊢ (FunSpace.next hf hx α).compProj t = picard f (↑t₀ : ℝ) x (FunSpace.next hf hx α).compProj t
have rw : (FunSpace.next hf hx α).toFun (projIcc tmin tmax sorry t) = picard f (↑t₀ : ℝ) x (FunSpace.next hf hx α).compProj t
Tactic: rw [FunSpace.compProj_apply, FunSpace.next_apply, hα, projIcc_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₀ 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
⊢ (FunSpace.next hf hx α).compProj t = picard f (↑t₀ : ℝ) x (FunSpace.next hf hx α).compProj t
have rw₁ : picard f (↑t₀ : ℝ) x α.compProj (↑(projIcc tmin tmax sorry t) : ℝ) = picard f (↑t₀ : ℝ) x (FunSpace.next hf hx α).compProj t
Tactic: rw [FunSpace.compProj_apply, FunSpace.next_apply, hα, projIcc_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₀ 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
⊢ (FunSpace.next hf hx α).compProj t = picard f (↑t₀ : ℝ) x (FunSpace.next hf hx α).compProj t
have rw₂ : picard f (↑t₀ : ℝ) x α.compProj (↑(projIcc tmin tmax sorry t) : ℝ) = picard f (↑t₀ : ℝ) x α.compProj t
Tactic: rw [FunSpace.compProj_apply, FunSpace.next_apply, hα, projIcc_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₀ 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
⊢ (FunSpace.next hf hx α).compProj t = picard f (↑t₀ : ℝ) x (FunSpace.next hf hx α).compProj t
have rw₃ : picard f (↑t₀ : ℝ) x α.compProj (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t ht) : ℝ) =
  picard f (↑t₀ : ℝ) x α.compProj t
Tactic: rw [FunSpace.compProj_apply, FunSpace.next_apply, hα, projIcc_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₀ x : E
a r L K : ℝ≥0
hf : IsPicardLindelof f t₀ x₀ a r L K
hx : x ∈ closedBall x₀ (↑r : ℝ)
⊢ ∃ (α : ℝ → E), α (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
have 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
Tactic: obtain ⟨α, hα⟩ := FunSpace.exists_isFixedPt_next hf hx
-- 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₀ 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) α
⊢ α.compProj (↑t₀ : ℝ) = x
have rw : α.toFun t₀ = x
Tactic: rw [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₀ 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
⊢ α.compProj (↑t₀ : ℝ) = x
have rw₁ : (FunSpace.next hf hx α).toFun t₀ = x
Tactic: rw [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₀ 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
⊢ α.compProj (↑t₀ : ℝ) = x
have rw₂ : x = x
Tactic: rw [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₀ 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) α
⊢ ∃ (α : ℝ → E), α (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt α (f t (α t)) (Icc tmin tmax) t
have refine : ∀ (t : ℝ) (ht : t ∈ Icc tmin tmax), HasDerivWithinAt α.compProj (f t (α.compProj t)) (Icc tmin tmax) t
Tactic: refine ⟨α.compProj, by rw [FunSpace.compProj_val, ← hα, FunSpace.next_apply₀], 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₀ 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
⊢ HasDerivWithinAt α.compProj (f t (α.compProj t)) (Icc tmin tmax) t
have apply : ∀ x_1 ∈ Icc tmin tmax, α.compProj x_1 = picard f (↑t₀ : ℝ) x α.compProj x_1
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
-- 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₀ 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
⊢ α.compProj t' = picard f (↑t₀ : ℝ) x α.compProj t'
have nth_rw : (FunSpace.next hf hx α).compProj t' = picard f (↑t₀ : ℝ) x α.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₀ 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
⊢ (FunSpace.next hf hx α).compProj t' = picard f (↑t₀ : ℝ) x α.compProj t'
have rw : (FunSpace.next hf hx α).toFun (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t' ht') =
  picard f (↑t₀ : ℝ) x α.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₀ 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'
⊢ (FunSpace.next hf hx α).compProj t' = picard f (↑t₀ : ℝ) x α.compProj t'
have rw₁ : picard f (↑t₀ : ℝ) x α.compProj (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc tmin tmax) t' ht') : ℝ) =
  picard f (↑t₀ : ℝ) x α.compProj t'
Tactic: rw [FunSpace.compProj_of_mem ht', FunSpace.next_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
⊢ ∃ (α : 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 this : ∀ (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
-- 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
this : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)), ∃ (α : FunSpace t₀ x₀ r L), IsFixedPt (FunSpace.next hf 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 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 : ℝ))
Tactic: choose α hα using this
Cleared hypotheses: this