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
⊢ ∃ (α : E → ℝ → E),
    ∀ x ∈ closedBall x₀ (↑r : ℝ),
      α x (↑t₀ : ℝ) = x ∧ ∀ t ∈ Icc tmin tmax, HasDerivWithinAt (α x) (f t (α x t)) (Icc tmin tmax) t

Tactic:
have ⟨α, hα⟩ := exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith hf
  ⟨α, hα.1⟩

Premises used: Exists, And.left, Exists.intro, IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_lipschitzOnWith, _private.0.IsPicardLindelof.exists_forall_mem_closedBall_eq_forall_mem_Icc_hasDerivWithinAt.match_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
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ : ℝ
have :
  ∀ (ε : ℝ) (hε : 0 < ε) (a r w w_1 : ℝ≥0) (hr : 0 < r)
    (hpl :
      ∀ (t₀ : ℝ),
        IsPicardLindelof (fun (x : ℝ) ↦ f) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r w
          w_1),
    ∃ r > 0,
      ∃ ε > 0, ∀ x ∈ closedBall x₀ r, ∃ (α : ℝ → E), α t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t
⊢ ∃ r > 0,
    ∃ ε > 0, ∀ x ∈ closedBall x₀ r, ∃ (α : ℝ → E), α t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t

Tactic:
have ⟨ε, hε, a, r, _, _, hr, hpl⟩ := IsPicardLindelof.of_contDiffAt_one hf
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ ε : ℝ
hε : 0 < ε
a r w w_1 : ℝ≥0
hr : 0 < r
hpl :
  ∀ (t₀ : ℝ),
    IsPicardLindelof (fun (x : ℝ) ↦ f) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r w w_1
⊢ ∃ r > 0,
    ∃ ε > 0, ∀ x ∈ closedBall x₀ r, ∃ (α : ℝ → E), α t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t

Tactic:
⟨r, hr, ε, hε, fun x hx ↦ ?_⟩

Premises used: And.intro, Exists.intro, 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
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ ε : ℝ
hε : 0 < ε
a r w w_1 : ℝ≥0
hr : 0 < r
hpl :
  ∀ (t₀ : ℝ),
    IsPicardLindelof (fun (x : ℝ) ↦ f) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r w w_1
refine :
  ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)),
    ∃ (α : ℝ → E), α t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t
⊢ ∃ r > 0,
    ∃ ε > 0, ∀ x ∈ closedBall x₀ r, ∃ (α : ℝ → E), α t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t

Tactic:
refine ⟨r, hr, ε, hε, fun x 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
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ ε : ℝ
hε : 0 < ε
a r w w_1 : ℝ≥0
hr : 0 < r
hpl :
  ∀ (t₀ : ℝ),
    IsPicardLindelof (fun (x : ℝ) ↦ f) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r w w_1
x : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
have :
  ∀ (α : ℝ → E) (hα1 : α (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) : ℝ) = x)
    (hα2 : ∀ t ∈ Icc (t₀ - ε) (t₀ + ε), HasDerivWithinAt α (f (α t)) (Icc (t₀ - ε) (t₀ + ε)) t),
    ∃ (α : ℝ → E), α t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t
⊢ ∃ (α : ℝ → E), α t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t

Tactic:
have ⟨α, hα1, hα2⟩ := (hpl t₀).exists_eq_forall_mem_Icc_hasDerivWithinAt 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
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ ε : ℝ
hε : 0 < ε
a r w w_1 : ℝ≥0
hr : 0 < r
hpl :
  ∀ (t₀ : ℝ),
    IsPicardLindelof (fun (x : ℝ) ↦ f) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r w w_1
x : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : ℝ → E
hα1 : α (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) : ℝ) = x
hα2 : ∀ t ∈ Icc (t₀ - ε) (t₀ + ε), HasDerivWithinAt α (f (α t)) (Icc (t₀ - ε) (t₀ + ε)) t
⊢ ∃ (α : ℝ → E), α t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t

Tactic:
⟨α, hα1, 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
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ ε : ℝ
hε : 0 < ε
a r w w_1 : ℝ≥0
hr : 0 < r
hpl :
  ∀ (t₀ : ℝ),
    IsPicardLindelof (fun (x : ℝ) ↦ f) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r w w_1
x : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : ℝ → E
hα1 : α (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) : ℝ) = x
hα2 : ∀ t ∈ Icc (t₀ - ε) (t₀ + ε), HasDerivWithinAt α (f (α t)) (Icc (t₀ - ε) (t₀ + ε)) t
refine : ∀ (t : ℝ) (ht : t ∈ Ioo (t₀ - ε) (t₀ + ε)), HasDerivAt α (f (α t)) t
⊢ ∃ (α : ℝ → E), α t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t

Tactic:
refine ⟨α, hα1, 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
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ ε : ℝ
hε : 0 < ε
a r w w_1 : ℝ≥0
hr : 0 < r
hpl :
  ∀ (t₀ : ℝ),
    IsPicardLindelof (fun (x : ℝ) ↦ f) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r w w_1
x : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : ℝ → E
hα1 : α (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) : ℝ) = x
hα2 : ∀ t ∈ Icc (t₀ - ε) (t₀ + ε), HasDerivWithinAt α (f (α t)) (Icc (t₀ - ε) (t₀ + ε)) t
t : ℝ
ht : t ∈ Ioo (t₀ - ε) (t₀ + ε)
⊢ HasDerivAt α (f (α t)) t

Tactic:
hα2 t (Ioo_subset_Icc_self ht) |>.hasDerivAt (Icc_mem_nhds ht.1 ht.2)

Premises used: Set.Ioo_subset_Icc_self, And.right, And.left, HasDerivWithinAt.hasDerivAt, Icc_mem_nhds
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ ε : ℝ
hε : 0 < ε
a r w w_1 : ℝ≥0
hr : 0 < r
hpl :
  ∀ (t₀ : ℝ),
    IsPicardLindelof (fun (x : ℝ) ↦ f) (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) x₀ a r w w_1
x : E
hx : x ∈ closedBall x₀ (↑r : ℝ)
α : ℝ → E
hα1 : α (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ ⋯) : ℝ) = x
hα2 : ∀ t ∈ Icc (t₀ - ε) (t₀ + ε), HasDerivWithinAt α (f (α t)) (Icc (t₀ - ε) (t₀ + ε)) t
t : ℝ
ht : t ∈ Ioo (t₀ - ε) (t₀ + ε)
⊢ HasDerivAt α (f (α t)) t

Tactic:
exact hα2 t (Ioo_subset_Icc_self ht) |>.hasDerivAt (Icc_mem_nhds ht.1 ht.2)

Premises used: Set.Ioo_subset_Icc_self, And.right, And.left, HasDerivWithinAt.hasDerivAt, Icc_mem_nhds
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ : ℝ
⊢ ∃ (α : ℝ → E), α t₀ = x₀ ∧ ∃ ε > 0, ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t

Tactic:
have ⟨_, hr, ε, hε, H⟩ := exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt hf t₀
  have ⟨α, hα1, hα2⟩ := H x₀ (mem_closedBall_self (le_of_lt hr))
  ⟨α, hα1, ε, hε, hα2⟩

Premises used: _private.0.ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀.match_1, _private.0.ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀.match_2, le_of_lt, Exists, GT.gt, And, And.intro, ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt, Exists.intro, OfNat.ofNat, Eq, 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
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ : ℝ
obtain :
  ∀ (r : ℝ) (hr : r > 0) (ε : ℝ) (hε : ε > 0)
    (H : ∀ x ∈ closedBall x₀ r, ∃ (α : ℝ → E), α t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t),
    ∃ (α : E → ℝ → E), ∀ᶠ (xt : E × ℝ) in 𝓝 x₀ ×ˢ 𝓝 t₀, α xt.1 t₀ = xt.1 ∧ HasDerivAt (α xt.1) (f (α xt.1 xt.2)) xt.2
⊢ ∃ (α : E → ℝ → E), ∀ᶠ (xt : E × ℝ) in 𝓝 x₀ ×ˢ 𝓝 t₀, α xt.1 t₀ = xt.1 ∧ HasDerivAt (α xt.1) (f (α xt.1 xt.2)) xt.2

Tactic:
obtain ⟨r, hr, ε, hε, H⟩ := exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt hf t₀

Premises used: ContDiffAt.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ r : ℝ
hr : r > 0
ε : ℝ
hε : ε > 0
H : ∀ x ∈ closedBall x₀ r, ∃ (α : ℝ → E), α t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t
choose :
  ∀ (α : (x : E) → x ∈ closedBall x₀ r → ℝ → E)
    (hα :
      ∀ (x : E) (a : x ∈ closedBall x₀ r),
        α x a t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt (α x a) (f (α x a t)) t),
    ∃ (α : E → ℝ → E), ∀ᶠ (xt : E × ℝ) in 𝓝 x₀ ×ˢ 𝓝 t₀, α xt.1 t₀ = xt.1 ∧ HasDerivAt (α xt.1) (f (α xt.1 xt.2)) xt.2
⊢ ∃ (α : E → ℝ → E), ∀ᶠ (xt : E × ℝ) in 𝓝 x₀ ×ˢ 𝓝 t₀, α xt.1 t₀ = xt.1 ∧ HasDerivAt (α xt.1) (f (α xt.1 xt.2)) xt.2

Tactic:
choose α hα using 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
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ r : ℝ
hr : r > 0
ε : ℝ
hε : ε > 0
α : (x : E) → x ∈ closedBall x₀ r → ℝ → E
hα : ∀ (x : E) (a : x ∈ closedBall x₀ r), α x a t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt (α x a) (f (α x a t)) t
⊢ ∃ (α : E → ℝ → E), ∀ᶠ (xt : E × ℝ) in 𝓝 x₀ ×ˢ 𝓝 t₀, α xt.1 t₀ = xt.1 ∧ HasDerivAt (α xt.1) (f (α xt.1 xt.2)) xt.2

Tactic:
⟨fun (x : E) ↦ if hx : x ∈ closedBall x₀ r then α x hx else 0, ?_⟩

Premises used: Membership.mem, dite, Exists.intro, Metric.closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ r : ℝ
hr : r > 0
ε : ℝ
hε : ε > 0
α : (x : E) → x ∈ closedBall x₀ r → ℝ → E
hα : ∀ (x : E) (a : x ∈ closedBall x₀ r), α x a t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt (α x a) (f (α x a t)) t
refine :
  ∀ᶠ (xt : E × ℝ) in 𝓝 x₀ ×ˢ 𝓝 t₀,
    (fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) xt.1 t₀ = xt.1 ∧
      HasDerivAt ((fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) xt.1)
        (f ((fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) xt.1 xt.2)) xt.2
⊢ ∃ (α : E → ℝ → E), ∀ᶠ (xt : E × ℝ) in 𝓝 x₀ ×ˢ 𝓝 t₀, α xt.1 t₀ = xt.1 ∧ HasDerivAt (α xt.1) (f (α xt.1 xt.2)) xt.2

Tactic:
refine ⟨fun (x : E) ↦ if hx : x ∈ closedBall x₀ r then α x hx else 0, ?_⟩
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ r : ℝ
hr : r > 0
ε : ℝ
hε : ε > 0
α : (x : E) → x ∈ closedBall x₀ r → ℝ → E
hα : ∀ (x : E) (a : x ∈ closedBall x₀ r), α x a t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt (α x a) (f (α x a t)) t
rw :
  ∃ v ∈ 𝓝 x₀ ×ˢ 𝓝 t₀,
    ∀ y ∈ v,
      (fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) y.1 t₀ = y.1 ∧
        HasDerivAt ((fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) y.1)
          (f ((fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) y.1 y.2)) y.2
⊢ ∀ᶠ (xt : E × ℝ) in 𝓝 x₀ ×ˢ 𝓝 t₀,
    (fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) xt.1 t₀ = xt.1 ∧
      HasDerivAt ((fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) xt.1)
        (f ((fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) xt.1 xt.2)) xt.2

Tactic:
rw [Filter.eventually_iff_exists_mem]

Premises used: Filter.eventually_iff_exists_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
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ r : ℝ
hr : r > 0
ε : ℝ
hε : ε > 0
α : (x : E) → x ∈ closedBall x₀ r → ℝ → E
hα : ∀ (x : E) (a : x ∈ closedBall x₀ r), α x a t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt (α x a) (f (α x a t)) t
⊢ ∃ v ∈ 𝓝 x₀ ×ˢ 𝓝 t₀,
    ∀ y ∈ v,
      (fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) y.1 t₀ = y.1 ∧
        HasDerivAt ((fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) y.1)
          (f ((fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) y.1 y.2)) y.2

Tactic:
⟨closedBall x₀ r ×ˢ Ioo (t₀ - ε) (t₀ + ε), ?_, ?_⟩

Premises used: SProd.sprod, HSub.hSub, HAdd.hAdd, And.intro, Exists.intro, Metric.closedBall, Set.Ioo
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ r : ℝ
hr : r > 0
ε : ℝ
hε : ε > 0
α : (x : E) → x ∈ closedBall x₀ r → ℝ → E
hα : ∀ (x : E) (a : x ∈ closedBall x₀ r), α x a t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt (α x a) (f (α x a t)) t
refine_1 : closedBall x₀ r ×ˢ Ioo (t₀ - ε) (t₀ + ε) ∈ 𝓝 x₀ ×ˢ 𝓝 t₀
refine_2 :
  ∀ y ∈ closedBall x₀ r ×ˢ Ioo (t₀ - ε) (t₀ + ε),
    (fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) y.1 t₀ = y.1 ∧
      HasDerivAt ((fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) y.1)
        (f ((fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) y.1 y.2)) y.2
⊢ ∃ v ∈ 𝓝 x₀ ×ˢ 𝓝 t₀,
    ∀ y ∈ v,
      (fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) y.1 t₀ = y.1 ∧
        HasDerivAt ((fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) y.1)
          (f ((fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) y.1 y.2)) y.2

Tactic:
refine ⟨closedBall x₀ r ×ˢ Ioo (t₀ - ε) (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
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ r : ℝ
hr : r > 0
ε : ℝ
hε : ε > 0
α : (x : E) → x ∈ closedBall x₀ r → ℝ → E
hα : ∀ (x : E) (a : x ∈ closedBall x₀ r), α x a t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt (α x a) (f (α x a t)) t
refine_1 : closedBall x₀ r ∈ 𝓝 x₀ ∧ Ioo (t₀ - ε) (t₀ + ε) ∈ 𝓝 t₀
⊢ closedBall x₀ r ×ˢ Ioo (t₀ - ε) (t₀ + ε) ∈ 𝓝 x₀ ×ˢ 𝓝 t₀

Tactic:
rw [Filter.prod_mem_prod_iff]

Premises used: Filter.prod_mem_prod_iff
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ r : ℝ
hr : r > 0
ε : ℝ
hε : ε > 0
α : (x : E) → x ∈ closedBall x₀ r → ℝ → E
hα : ∀ (x : E) (a : x ∈ closedBall x₀ r), α x a t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt (α x a) (f (α x a t)) t
linarith : t₀ ≤ t₀ - ε → 0 - ε + (t₀ - (t₀ - ε)) = 0
⊢ t₀ - ε < t₀

Tactic:
linarith
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ r : ℝ
hr : r > 0
ε : ℝ
hε : ε > 0
α : (x : E) → x ∈ closedBall x₀ r → ℝ → E
hα : ∀ (x : E) (a : x ∈ closedBall x₀ r), α x a t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt (α x a) (f (α x a t)) t
linarith : t₀ + ε ≤ t₀ → 0 - ε + (t₀ + ε - t₀) = 0
⊢ t₀ < t₀ + ε

Tactic:
linarith
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ r : ℝ
hr : r > 0
ε : ℝ
hε : ε > 0
α : (x : E) → x ∈ closedBall x₀ r → ℝ → E
hα : ∀ (x : E) (a : x ∈ closedBall x₀ r), α x a t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt (α x a) (f (α x a t)) t
⊢ closedBall x₀ r ∈ 𝓝 x₀ ∧ Ioo (t₀ - ε) (t₀ + ε) ∈ 𝓝 t₀

Tactic:
exact ⟨closedBall_mem_nhds x₀ hr, Ioo_mem_nhds (by linarith) (by linarith)⟩
-- Module: Mathlib.Analysis.ODE.PicardLindelof
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : E → E
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ r : ℝ
hr : r > 0
ε : ℝ
hε : ε > 0
α : (x : E) → x ∈ closedBall x₀ r → ℝ → E
hα : ∀ (x : E) (a : x ∈ closedBall x₀ r), α x a t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt (α x a) (f (α x a t)) t
⊢ ∀ y ∈ closedBall x₀ r ×ˢ Ioo (t₀ - ε) (t₀ + ε),
    (fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) y.1 t₀ = y.1 ∧
      HasDerivAt ((fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) y.1)
        (f ((fun (x : E) ↦ (if hx : x ∈ closedBall x₀ r then α x hx else 0 : ℝ → E)) y.1 y.2)) y.2

Tactic:
grind
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
dt t : ℝ
ht : t ∈ -dt +ᵥ s
rw : HasDerivWithinAt γ (v (t + dt) ((fun (x : ℝ) ↦ γ (x + dt)) t)) s (t + dt)
⊢ HasDerivWithinAt (γ ∘ fun (x : ℝ) ↦ x + dt) ((v ∘ fun (x : ℝ) ↦ x + dt) t ((γ ∘ fun (x : ℝ) ↦ x + dt) t)) (-dt +ᵥ s) t

Tactic:
rw [comp_apply, hasDerivWithinAt_iff_hasFDerivWithinAt, Function.comp_def,
    hasFDerivWithinAt_comp_add_right, ← hasDerivWithinAt_iff_hasFDerivWithinAt, vadd_neg_vadd]

Premises used: hasDerivWithinAt_iff_hasFDerivWithinAt, vadd_neg_vadd, Function.comp_def, hasFDerivWithinAt_comp_add_right, Function.comp_apply
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
dt t : ℝ
ht : t ∈ -dt +ᵥ s
apply : t + dt ∈ s
⊢ HasDerivWithinAt γ (v (t + dt) ((fun (x : ℝ) ↦ γ (x + dt)) t)) s (t + dt)

Tactic:
apply hγ (t + dt)

Premises used: HAdd.hAdd
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
dt t : ℝ
ht : t ∈ -dt +ᵥ s
rwa : ∀ (ht : - -dt +ᵥ t ∈ s), t + dt ∈ s
rwa₁ : ∀ (ht : dt +ᵥ t ∈ s), t + dt ∈ s
rwa₂ : ∀ (ht : dt + t ∈ s), t + dt ∈ s
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (ht : t + dt ∈ s), t + dt ∈ s
⊢ t + dt ∈ s

Tactic:
rwa [mem_vadd_set_iff_neg_vadd_mem, neg_neg, vadd_eq_add, add_comm] at ht

Premises used: neg_neg, add_comm, vadd_eq_add, Set.mem_vadd_set_iff_neg_vadd_mem
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
dt : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (-dt +ᵥ s) ↔ IsIntegralCurveOn γ v s

Tactic:
⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_add _⟩

Premises used: IsIntegralCurveOn.comp_add, Iff.intro
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
dt : ℝ
refine :
  ∀ (hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (-dt +ᵥ s)), IsIntegralCurveOn γ v s
⊢ IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (-dt +ᵥ s) ↔ IsIntegralCurveOn γ v s

Tactic:
refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_add _⟩
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
dt : ℝ
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (-dt +ᵥ s)
⊢ IsIntegralCurveOn (comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt)
    (comp (β := ℝ) (v ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt) (- -dt +ᵥ -dt +ᵥ s)

Tactic:
hγ.comp_add (-dt)

Premises used: IsIntegralCurveOn.comp_add, Neg.neg
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
dt : ℝ
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (-dt +ᵥ s)
h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt
h₁ : v = comp (β := ℝ) (v ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt
h₂ : s = - -dt +ᵥ -dt +ᵥ s
⊢ IsIntegralCurveOn γ v s

Tactic:
convert! hγ.comp_add (-dt)

Premises used: IsIntegralCurveOn.comp_add, Neg.neg
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
dt : ℝ
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (-dt +ᵥ s)
h : ∀ (t : ℝ), γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) (fun (x : ℝ) ↦ x + -dt) t
⊢ γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt

Tactic:
ext t
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
dt : ℝ
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (-dt +ᵥ s)
t : ℝ
⊢ γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) (fun (x : ℝ) ↦ x + -dt) t

Tactic:
simp only [comp_apply, neg_add_cancel_right]

Premises used: neg_add_cancel_right, Function.comp_apply
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
dt : ℝ
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (-dt +ᵥ s)
h : ∀ (t : ℝ) (x : E), v t x = comp (β := ℝ) (v ∘ fun (x : ℝ) ↦ x + dt) (fun (x : ℝ) ↦ x + -dt) t x
⊢ v = comp (β := ℝ) (v ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt

Tactic:
ext t
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
dt : ℝ
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (-dt +ᵥ s)
t : ℝ
x : E
⊢ v t x = comp (β := ℝ) (v ∘ fun (x : ℝ) ↦ x + dt) (fun (x : ℝ) ↦ x + -dt) t x

Tactic:
simp only [comp_apply, neg_add_cancel_right]

Premises used: neg_add_cancel_right, Function.comp_apply
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
dt : ℝ
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (-dt +ᵥ s)
⊢ s = - -dt +ᵥ -dt +ᵥ s

Tactic:
simp only [neg_neg, vadd_neg_vadd]

Premises used: neg_neg, vadd_neg_vadd
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
dt : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x - dt) (v ∘ fun (x : ℝ) ↦ x - dt) (dt +ᵥ s) ↔ IsIntegralCurveOn γ v s

Tactic:
simpa using isIntegralCurveOn_comp_add (dt := -dt)

Premises used: isIntegralCurveOn_comp_add
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
dt : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x - dt) (v ∘ fun (x : ℝ) ↦ x - dt) (dt +ᵥ s)

Tactic:
isIntegralCurveOn_comp_sub.mpr hγ

Premises used: Iff.mpr, isIntegralCurveOn_comp_sub
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ dt : ℝ
simp_rw :
  (∃ ε > 0, IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (Metric.ball (t₀ - dt) ε)) ↔
    ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (t₀ - dt) ↔ IsIntegralCurveAt γ v t₀

Tactic:
simp_rw [isIntegralCurveAt_iff_exists_pos]

Premises used: isIntegralCurveAt_iff_exists_pos
-- Module: Mathlib.Analysis.ODE.Transform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ dt : ℝ
a :
  ∀ (ε : ℝ),
    IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (Metric.ball (t₀ - dt) ε) ↔
      IsIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ (∃ ε > 0, IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (Metric.ball (t₀ - dt) ε)) ↔
    ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)

Tactic:
congrm ∃ ε > 0, ?_