awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
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 : ℝ),
    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
⊢ ∀ᶠ (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 (hsrc hg |>.and hg.eventually_hasDerivAt).mono

Premises used: Filter.Eventually.and, Filter.Eventually.mono, IsMIntegralCurveAt.eventually_hasDerivAt
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
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
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
⊢ HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g) ((fun (x : ℝ) ↦ v') t (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)) t

Tactic:
rw [hv', h']
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
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
a a₁ a₂ : g t = (↑(extChartAt I (g t₀)).symm : E → M) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) 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)

Tactic:
congr
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
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
a : g t = (↑(extChartAt I (g t₀)).symm : E → M) ((↑(extChartAt I (g t₀)) : M → E) (g t))
a₁ a₂ : g t = g t
⊢ 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)]

Premises used: Function.comp_apply, PartialEquiv.left_inv
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
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 : s ∈ 𝓝 (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t₀)
⊢ ∀ᶠ (x : ℝ) in 𝓝 t₀, Membership.mem (γ := Set E) ((fun (x : ℝ) ↦ s) x) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) x)

Tactic:
apply ((continuousAt_extChartAt (g t₀)).comp hg.continuousAt).preimage_mem_nhds

Premises used: continuousAt_extChartAt, ContinuousAt.preimage_mem_nhds, IsMIntegralCurveAt.continuousAt, ContinuousAt.comp
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
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 : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
⊢ s ∈ 𝓝 (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t₀)

Tactic:
rw [Function.comp_apply, ← h']

Premises used: Function.comp_apply
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
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₀
⊢ s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))

Tactic:
hs
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
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₀
⊢ s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))

Tactic:
exact hs
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
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)

Tactic:
have hdrv {g} (hg : IsMIntegralCurveAt g v t₀) (h' : γ t₀ = g t₀) : ∀ᶠ t in 𝓝 t₀,
      HasDerivAt ((extChartAt I (g t₀)) ∘ g) ((fun _ ↦ v') t (((extChartAt I (g t₀)) ∘ g) t)) t ∧
      ((extChartAt I (g t₀)) ∘ g) t ∈ (fun _ ↦ s) t := by
    apply Filter.Eventually.and
    · apply (hsrc hg |>.and hg.eventually_hasDerivAt).mono
      rintro t ⟨ht1, ht2⟩
      rw [hv', h']
      apply ht2.congr_deriv
      congr <;>
      rw [Function.comp_apply, PartialEquiv.left_inv _ (hmem ht1)]
    · apply ((continuousAt_extChartAt (g t₀)).comp hg.continuousAt).preimage_mem_nhds
      rw [Function.comp_apply, ← h']
      exact hs