awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
v' : E → E :=
  fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
hv' :
  v' = fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) (γ t₀)
hv :
  ContDiffWithinAt ℝ 1
    (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
      (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨γ t₀, v (γ t₀)⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
      ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I (γ t₀)).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
⊢ γ =ᶠ[𝓝 t₀] γ'
have obtain : ∀ (K : NNReal) (s : Set E) (hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))) (hlip : LipschitzOnWith K v' s),
  γ =ᶠ[𝓝 t₀] γ'
Tactic: obtain ⟨K, s, hs, hlip⟩ : ∃ K, ∃ s ∈ 𝓝 _, LipschitzOnWith K v' s :=
    (hv.contDiffAt (range_mem_nhds_isInteriorPoint hγt₀)).snd.exists_lipschitzOnWith
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
v' : E → E :=
  fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
hv' :
  v' = fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) (γ t₀)
hv :
  ContDiffWithinAt ℝ 1
    (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
      (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨γ t₀, v (γ t₀)⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
      ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I (γ t₀)).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
hlip : LipschitzOnWith K v' s
⊢ γ =ᶠ[𝓝 t₀] γ'
have hlip₁ : ∀ (t : ℝ), LipschitzOnWith.{u_1, u_1} (α := E) (β := E) K ((fun (x : ℝ) ↦ v') t) ((fun (x : ℝ) ↦ s) t)
Tactic: have hlip (t : ℝ) : LipschitzOnWith K ((fun _ ↦ v') t) ((fun _ ↦ s) t) := hlip
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
v' : E → E :=
  fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
hv' :
  v' = fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) (γ t₀)
hv :
  ContDiffWithinAt ℝ 1
    (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
      (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨γ t₀, v (γ t₀)⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
      ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I (γ t₀)).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
hlip_1 : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith.{u_1, u_1} (α := E) (β := E) K ((fun (x : ℝ) ↦ v') t) ((fun (x : ℝ) ↦ s) t)
⊢ γ =ᶠ[𝓝 t₀] γ'
have hsrc : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀), ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
Tactic: have hsrc {g} (hg : IsMIntegralCurveAt g v t₀) :
    ∀ᶠ t in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t := eventually_mem_nhds_iff.mpr <|
      continuousAt_def.mp hg.continuousAt _ <| extChartAt_source_mem_nhds (g t₀)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
v' : E → E :=
  fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
hv' :
  v' = fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) (γ t₀)
hv :
  ContDiffWithinAt ℝ 1
    (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
      (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨γ t₀, v (γ t₀)⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
      ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I (γ t₀)).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
hlip_1 : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith.{u_1, u_1} (α := E) (β := E) K ((fun (x : ℝ) ↦ v') t) ((fun (x : ℝ) ↦ s) t)
hsrc : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀), ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
⊢ γ =ᶠ[𝓝 t₀] γ'
have hmem : ∀ {g : ℝ → M} {t : ℝ} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t), g t ∈ (extChartAt I (g t₀)).source
Tactic: have hmem {g : ℝ → M} {t} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t) :
    g t ∈ (extChartAt I (g t₀)).source := mem_preimage.mp <| mem_of_mem_nhds ht
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
v' : E → E :=
  fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
hv' :
  v' = fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) (γ t₀)
hv :
  ContDiffWithinAt ℝ 1
    (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
      (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨γ t₀, v (γ t₀)⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
      ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I (γ t₀)).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
hlip_1 : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith.{u_1, u_1} (α := E) (β := E) K ((fun (x : ℝ) ↦ v') t) ((fun (x : ℝ) ↦ s) t)
hsrc : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀), ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
hmem : ∀ {g : ℝ → M} {t : ℝ} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t), g t ∈ (extChartAt I (g t₀)).source
g : ℝ → M
hg : IsMIntegralCurveAt g v t₀
h' : γ t₀ = g t₀
⊢ ∀ᶠ (t : ℝ) in 𝓝 t₀,
    HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g) ((fun (x : ℝ) ↦ v') t (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t))
        t ∧
      Membership.mem (γ := Set E) ((fun (x : ℝ) ↦ s) t) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)
have a : ∀ᶠ (x : ℝ) in 𝓝 t₀,
  HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g) ((fun (x : ℝ) ↦ v') x (((↑(extChartAt I (g t₀)) : M → E) ∘ g) x)) x
Tactic: apply Filter.Eventually.and
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
v' : E → E :=
  fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
hv' :
  v' = fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) (γ t₀)
hv :
  ContDiffWithinAt ℝ 1
    (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
      (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨γ t₀, v (γ t₀)⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
      ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I (γ t₀)).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
hlip_1 : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith.{u_1, u_1} (α := E) (β := E) K ((fun (x : ℝ) ↦ v') t) ((fun (x : ℝ) ↦ s) t)
hsrc : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀), ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
hmem : ∀ {g : ℝ → M} {t : ℝ} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t), g t ∈ (extChartAt I (g t₀)).source
g : ℝ → M
hg : IsMIntegralCurveAt g v t₀
h' : γ t₀ = g t₀
a :
  ∀ᶠ (x : ℝ) in 𝓝 t₀,
    HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g) ((fun (x : ℝ) ↦ v') x (((↑(extChartAt I (g t₀)) : M → E) ∘ g) x))
      x
⊢ ∀ᶠ (t : ℝ) in 𝓝 t₀,
    HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g) ((fun (x : ℝ) ↦ v') t (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t))
        t ∧
      Membership.mem (γ := Set E) ((fun (x : ℝ) ↦ s) t) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)
have a₁ : ∀ᶠ (x : ℝ) in 𝓝 t₀, Membership.mem (γ := Set E) ((fun (x : ℝ) ↦ s) x) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) x)
Tactic: apply Filter.Eventually.and
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
v' : E → E :=
  fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
hv' :
  v' = fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) (γ t₀)
hv :
  ContDiffWithinAt ℝ 1
    (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
      (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨γ t₀, v (γ t₀)⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
      ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I (γ t₀)).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
hlip_1 : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith.{u_1, u_1} (α := E) (β := E) K ((fun (x : ℝ) ↦ v') t) ((fun (x : ℝ) ↦ s) t)
hsrc : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀), ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
hmem : ∀ {g : ℝ → M} {t : ℝ} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t), g t ∈ (extChartAt I (g t₀)).source
g : ℝ → M
hg : IsMIntegralCurveAt g v t₀
h' : γ t₀ = g t₀
⊢ ∀ᶠ (x : ℝ) in 𝓝 t₀,
    HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g) ((fun (x : ℝ) ↦ v') x (((↑(extChartAt I (g t₀)) : M → E) ∘ g) x))
      x
have a : ∀ (x : ℝ),
  g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 x ∧
      HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g)
        ((tangentCoordChange I (g x) (g t₀) (g x) : (a : E) → E) (v (g x) : TangentSpace I (g x))) x →
    HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g) ((fun (x : ℝ) ↦ v') x (((↑(extChartAt I (g t₀)) : M → E) ∘ g) x))
      x
Tactic: apply (hsrc hg |>.and hg.eventually_hasDerivAt).mono
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
v' : E → E :=
  fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
hv' :
  v' = fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) (γ t₀)
hv :
  ContDiffWithinAt ℝ 1
    (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
      (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨γ t₀, v (γ t₀)⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
      ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I (γ t₀)).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
hlip_1 : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith.{u_1, u_1} (α := E) (β := E) K ((fun (x : ℝ) ↦ v') t) ((fun (x : ℝ) ↦ s) t)
hsrc : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀), ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
hmem : ∀ {g : ℝ → M} {t : ℝ} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t), g t ∈ (extChartAt I (g t₀)).source
g : ℝ → M
hg : IsMIntegralCurveAt g v t₀
h' : γ t₀ = g t₀
t : ℝ
ht1 : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
ht2 :
  HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g)
    ((tangentCoordChange I (g t) (g t₀) (g t) : (a : E) → E) (v (g t) : TangentSpace I (g t))) t
⊢ HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g) ((fun (x : ℝ) ↦ v') t (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)) t
have a : HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g)
  ((fun (x : ℝ) (x_1 : E) ↦
      ((tangentCoordChange I ((↑(extChartAt I (g t₀)).symm : E → M) x_1) (g t₀)
              ((↑(extChartAt I (g t₀)).symm : E → M) x_1) :
            (a : E) → E)
          (v ((↑(extChartAt I (g t₀)).symm : E → M) x_1) : TangentSpace I ((↑(extChartAt I (g t₀)).symm : E → M) x_1)) :
        E))
    t (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t))
  t
Tactic: rw [hv', h']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
v' : E → E :=
  fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
hv' :
  v' = fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) (γ t₀)
hv :
  ContDiffWithinAt ℝ 1
    (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
      (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨γ t₀, v (γ t₀)⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
      ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I (γ t₀)).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
hlip_1 : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith.{u_1, u_1} (α := E) (β := E) K ((fun (x : ℝ) ↦ v') t) ((fun (x : ℝ) ↦ s) t)
hsrc : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀), ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
hmem : ∀ {g : ℝ → M} {t : ℝ} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t), g t ∈ (extChartAt I (g t₀)).source
g : ℝ → M
hg : IsMIntegralCurveAt g v t₀
h' : γ t₀ = g t₀
t : ℝ
ht1 : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
ht2 :
  HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g)
    ((tangentCoordChange I (g t) (g t₀) (g t) : (a : E) → E) (v (g t) : TangentSpace I (g t))) t
⊢ Eq (α := E) ((tangentCoordChange I (g t) (g t₀) (g t) : (a : E) → E) (v (g t) : TangentSpace I (g t)) : E)
    ((fun (x : ℝ) (x_1 : E) ↦
          ((tangentCoordChange I ((↑(extChartAt I (g t₀)).symm : E → M) x_1) (g t₀)
                  ((↑(extChartAt I (g t₀)).symm : E → M) x_1) :
                (a : E) → E)
              (v ((↑(extChartAt I (g t₀)).symm : E → M) x_1) :
                TangentSpace I ((↑(extChartAt I (g t₀)).symm : E → M) x_1)) :
            E))
        t (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t) :
      E)
have a : g t = (↑(extChartAt I (g t₀)).symm : E → M) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)
Tactic: congr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
v' : E → E :=
  fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
hv' :
  v' = fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) (γ t₀)
hv :
  ContDiffWithinAt ℝ 1
    (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
      (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨γ t₀, v (γ t₀)⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
      ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I (γ t₀)).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
hlip_1 : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith.{u_1, u_1} (α := E) (β := E) K ((fun (x : ℝ) ↦ v') t) ((fun (x : ℝ) ↦ s) t)
hsrc : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀), ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
hmem : ∀ {g : ℝ → M} {t : ℝ} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t), g t ∈ (extChartAt I (g t₀)).source
g : ℝ → M
hg : IsMIntegralCurveAt g v t₀
h' : γ t₀ = g t₀
t : ℝ
ht1 : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
ht2 :
  HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g)
    ((tangentCoordChange I (g t) (g t₀) (g t) : (a : E) → E) (v (g t) : TangentSpace I (g t))) t
⊢ g t = (↑(extChartAt I (g t₀)).symm : E → M) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)
have a : g t = (↑(extChartAt I (g t₀)).symm : E → M) ((↑(extChartAt I (g t₀)) : M → E) (g t))
Tactic: rw [Function.comp_apply, PartialEquiv.left_inv _ (hmem ht1)]