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
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 : ℝ))
⊢ ContinuousOn (uncurry α) (closedBall x₀ (↑r : ℝ) ×ˢ Icc tmin tmax)
have apply : ∀ a ∈ closedBall x₀ (↑r : ℝ), ContinuousOn.{0, u_1} (Y := E) (fun (y : ℝ) ↦ uncurry α (a, y)) (Icc tmin tmax)
Tactic: apply continuousOn_prod_of_continuousOn_lipschitzOnWith _ L' _ hα2
-- 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
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ : ℝ
⊢ ∃ r > 0,
    ∃ ε > 0, ∀ x ∈ closedBall x₀ r, ∃ (α : ℝ → E), α t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t
have 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₀ sorry) 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: have ⟨ε, hε, a, r, _, _, hr, hpl⟩ := IsPicardLindelof.of_contDiffAt_one 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
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
have refine : ∀ (x : E) (hx : x ∈ closedBall x₀ (↑r : ℝ)),
  ∃ (α : ℝ → E), α t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t
Tactic: refine ⟨r, hr, ε, hε, fun x 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
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), α t₀ = x ∧ ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε), HasDerivAt α (f (α t)) t
have have : ∀ (α : ℝ → E) (hα1 : α (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Icc (t₀ - ε) (t₀ + ε)) t₀ sorry) : ℝ) = 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: have ⟨α, hα1, hα2⟩ := (hpl t₀).exists_eq_forall_mem_Icc_hasDerivWithinAt 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
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
have refine : ∀ (t : ℝ) (ht : t ∈ Ioo (t₀ - ε) (t₀ + ε)), HasDerivAt α (f (α t)) t
Tactic: refine ⟨α, hα1, 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
x₀ : E
hf : ContDiffAt ℝ 1 f x₀
t₀ : ℝ
⊢ ∃ (α : E → ℝ → E), ∀ᶠ (xt : E × ℝ) in 𝓝 x₀ ×ˢ 𝓝 t₀, α xt.1 t₀ = xt.1 ∧ HasDerivAt (α xt.1) (f (α xt.1 xt.2)) xt.2
have 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
Tactic: obtain ⟨r, hr, ε, hε, H⟩ := exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt hf 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
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
⊢ ∃ (α : E → ℝ → E), ∀ᶠ (xt : E × ℝ) in 𝓝 x₀ ×ˢ 𝓝 t₀, α xt.1 t₀ = xt.1 ∧ HasDerivAt (α xt.1) (f (α xt.1 xt.2)) xt.2
have 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
Tactic: choose α hα using H
Cleared hypotheses: 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
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
have 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
Tactic: refine ⟨fun (x : E) ↦ if hx : x ∈ closedBall x₀ r then α x hx else 0, ?_⟩
-- 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
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
⊢ ∀ᶠ (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
have 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
Tactic: rw [Filter.eventually_iff_exists_mem]
-- 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
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
have refine_1 : closedBall x₀ r ×ˢ Ioo (t₀ - ε) (t₀ + ε) ∈ 𝓝 x₀ ×ˢ 𝓝 t₀
Tactic: refine ⟨closedBall x₀ r ×ˢ Ioo (t₀ - ε) (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
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₀
⊢ ∃ 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
have 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
Tactic: refine ⟨closedBall x₀ r ×ˢ Ioo (t₀ - ε) (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
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 ×ˢ Ioo (t₀ - ε) (t₀ + ε) ∈ 𝓝 x₀ ×ˢ 𝓝 t₀
have refine_1 : closedBall x₀ r ∈ 𝓝 x₀ ∧ Ioo (t₀ - ε) (t₀ + ε) ∈ 𝓝 t₀
Tactic: rw [Filter.prod_mem_prod_iff]
-- 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
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
⊢ t₀ - ε < t₀
have linarith : t₀ ≤ t₀ - ε → 0 - ε + (t₀ - (t₀ - ε)) = 0
Tactic: linarith
-- 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
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
⊢ t₀ < t₀ + ε
have linarith : t₀ + ε ≤ t₀ → 0 - ε + (t₀ + ε - t₀) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
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
⊢ HasDerivWithinAt (γ ∘ fun (x : ℝ) ↦ x + dt) ((v ∘ fun (x : ℝ) ↦ x + dt) t ((γ ∘ fun (x : ℝ) ↦ x + dt) t)) (-dt +ᵥ s) t
have rw : HasDerivWithinAt γ (v (t + dt) ((fun (x : ℝ) ↦ γ (x + dt)) t)) s (t + dt)
Tactic: rw [comp_apply, hasDerivWithinAt_iff_hasFDerivWithinAt, Function.comp_def,
    hasFDerivWithinAt_comp_add_right, ← hasDerivWithinAt_iff_hasFDerivWithinAt, vadd_neg_vadd]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
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
⊢ HasDerivWithinAt γ (v (t + dt) ((fun (x : ℝ) ↦ γ (x + dt)) t)) s (t + dt)
have apply : t + dt ∈ s
Tactic: apply hγ (t + dt)
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
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
⊢ t + dt ∈ s
have rwa : ∀ (ht : - -dt +ᵥ t ∈ s), t + dt ∈ s
Tactic: rwa [mem_vadd_set_iff_neg_vadd_mem, neg_neg, vadd_eq_add, add_comm] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
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
⊢ t + dt ∈ s
have rwa₁ : ∀ (ht : dt +ᵥ t ∈ s), t + dt ∈ s
Tactic: rwa [mem_vadd_set_iff_neg_vadd_mem, neg_neg, vadd_eq_add, add_comm] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
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
⊢ t + dt ∈ s
have rwa₂ : ∀ (ht : dt + t ∈ s), t + dt ∈ s
Tactic: rwa [mem_vadd_set_iff_neg_vadd_mem, neg_neg, vadd_eq_add, add_comm] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
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
⊢ t + dt ∈ s
have rwa₃ : ∀ (ht : t + dt ∈ s), t + dt ∈ s
Tactic: rwa [mem_vadd_set_iff_neg_vadd_mem, neg_neg, vadd_eq_add, add_comm] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
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
have refine : ∀ (hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (-dt +ᵥ s)), IsIntegralCurveOn γ v s
Tactic: refine ⟨fun hγ ↦ ?_, fun hγ ↦ hγ.comp_add _⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
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 γ v s
have h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt
Tactic: convert! hγ.comp_add (-dt)
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
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
⊢ IsIntegralCurveOn γ v s
have h₁ : v = comp (β := ℝ) (v ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt
Tactic: convert! hγ.comp_add (-dt)
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
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
⊢ IsIntegralCurveOn γ v s
have h₂ : s = - -dt +ᵥ -dt +ᵥ s
Tactic: convert! hγ.comp_add (-dt)
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
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)
⊢ γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt
have h : ∀ (t : ℝ), γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x + dt) (fun (x : ℝ) ↦ x + -dt) t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
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)
⊢ v = comp (β := ℝ) (v ∘ fun (x : ℝ) ↦ x + dt) fun (x : ℝ) ↦ x + -dt
have h : ∀ (t : ℝ) (x : E), v t x = comp (β := ℝ) (v ∘ fun (x : ℝ) ↦ x + dt) (fun (x : ℝ) ↦ x + -dt) t x
Tactic: ext t
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ dt : ℝ
⊢ IsIntegralCurveAt (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (t₀ - dt) ↔ IsIntegralCurveAt γ v t₀
have simp_rw : (∃ ε > 0, IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (Metric.ball (t₀ - dt) ε)) ↔
  ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)
Tactic: simp_rw [isIntegralCurveAt_iff_exists_pos]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ dt : ℝ
⊢ (∃ ε > 0, IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (Metric.ball (t₀ - dt) ε)) ↔
    ∃ ε > 0, IsIntegralCurveOn γ v (Metric.ball t₀ ε)
have a : ∀ (ε : ℝ),
  IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (Metric.ball (t₀ - dt) ε) ↔
    IsIntegralCurveOn γ v (Metric.ball t₀ ε)
Tactic: congrm ∃ ε > 0, ?_
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
t₀ dt ε : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) (Metric.ball (t₀ - dt) ε) ↔
    IsIntegralCurveOn γ v (Metric.ball t₀ ε)
have h : Metric.ball (t₀ - dt) ε = -dt +ᵥ Metric.ball t₀ ε
Tactic: convert! isIntegralCurveOn_comp_add
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
hγ : IsIntegralCurve γ v
dt : ℝ
⊢ IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt)
have rw : ∀ (hγ : IsIntegralCurveOn γ v univ) (dt : ℝ),
  IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) univ
Tactic: rw [← isIntegralCurveOn_univ] at *
Cleared hypotheses: hγ, dt
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
dt : ℝ
⊢ IsIntegralCurve (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) ↔ IsIntegralCurve γ v
have simp_rw : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) univ ↔ IsIntegralCurveOn γ v univ
Tactic: simp_rw [← isIntegralCurveOn_univ]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
dt : ℝ
⊢ IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x + dt) (v ∘ fun (x : ℝ) ↦ x + dt) univ ↔ IsIntegralCurveOn γ v univ
have h : univ = HVAdd.hVAdd (β := Set ℝ) (-dt) univ
Tactic: convert! isIntegralCurveOn_comp_add
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
hγ : IsIntegralCurveOn γ v s
a t : ℝ
ht : Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t
⊢ HasDerivWithinAt (γ ∘ fun (x : ℝ) ↦ x * a)
    (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) t ((γ ∘ fun (x : ℝ) ↦ x * a) t)) {t : ℝ | t * a ∈ s} t
have simp : HasDerivWithinAt (γ ∘ fun (x : ℝ) ↦ x * a) (a • v (t * a) (γ (t * a))) {t : ℝ | t * a ∈ s} t
Tactic: simp only [comp_apply, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
⊢ a⁻¹ • s = {t : ℝ | t * a ∈ s}
have h : ∀ (t : ℝ), t ∈ a⁻¹ • s ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
t : ℝ
⊢ t ∈ a⁻¹ • s ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t
have h : t * a ∈ s ↔ Membership.mem (γ := Set ℝ) {t : ℝ | t * a ∈ s} t
Tactic: rw [mem_inv_smul_set_iff₀ ha, smul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
⊢ IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (a⁻¹ • s) ↔
    IsIntegralCurveOn γ v s
have heq : a⁻¹ • s = {t : ℝ | t * a ∈ s}
Tactic: have heq : a⁻¹ • s = { t | t * a ∈ s } := by
    ext t
    rw [mem_inv_smul_set_iff₀ ha, smul_eq_mul, mul_comm]
    rfl
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t : ℝ | t * a ∈ s}
⊢ IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (a⁻¹ • s) ↔
    IsIntegralCurveOn γ v s
have refine : ∀
  (hγ :
    IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (a⁻¹ • s)),
  IsIntegralCurveOn γ v s
Tactic: refine ⟨fun hγ ↦ ?_, heq ▸ fun hγ ↦ hγ.comp_mul a⟩
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t : ℝ | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (a⁻¹ • s)
⊢ IsIntegralCurveOn γ v s
have h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
Tactic: convert! hγ.comp_mul a⁻¹
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t : ℝ | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (a⁻¹ • s)
h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
⊢ IsIntegralCurveOn γ v s
have h₁ : v = HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)
Tactic: convert! hγ.comp_mul a⁻¹
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t : ℝ | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (a⁻¹ • s)
h : γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
h₁ :
  v =
    HSMul.hSMul (β := ℝ → E → E) a⁻¹ (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a) ∘ fun (x : ℝ) ↦ x * a⁻¹)
⊢ IsIntegralCurveOn γ v s
have h₂ : s = {t : ℝ | t * a⁻¹ ∈ a⁻¹ • s}
Tactic: convert! hγ.comp_mul a⁻¹
-- Lean 4 proof step from Mathlib.Analysis.ODE.Transform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
γ : ℝ → E
v : ℝ → E → E
s : Set ℝ
a : ℝ
ha : a ≠ 0
heq : a⁻¹ • s = {t : ℝ | t * a ∈ s}
hγ : IsIntegralCurveOn (γ ∘ fun (x : ℝ) ↦ x * a) (HSMul.hSMul (β := ℝ → E → E) a (v ∘ fun (x : ℝ) ↦ x * a)) (a⁻¹ • s)
⊢ γ = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) fun (x : ℝ) ↦ x * a⁻¹
have h : ∀ (t : ℝ), γ t = comp (β := ℝ) (γ ∘ fun (x : ℝ) ↦ x * a) (fun (x : ℝ) ↦ x * a⁻¹) t
Tactic: ext t