awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
t₀ : ℝ
inst_5 : IsManifold I 1 M
hγ : IsMIntegralCurveOn γ v s
t : ℝ
ht : t ∈ s
hsrc : γ t ∈ (extChartAt I (γ t₀)).source
⊢ γ t ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (γ t₀))).source

Tactic:
replace hsrc := extChartAt_source I (γ t₀) ▸ hsrc
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
t₀ : ℝ
inst_5 : IsManifold I 1 M
hγ : IsMIntegralCurveOn γ v s
t : ℝ
ht : t ∈ s
hsrc : γ t ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (γ t₀))).source
rw :
  HasMFDerivWithinAt 𝓘(ℝ, ℝ) 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ) s t
    (ContinuousLinearMap.toSpanSingleton ℝ
      ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))))
⊢ HasDerivWithinAt ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ)
    ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) s t

Tactic:
rw [hasDerivWithinAt_iff_hasFDerivWithinAt, ← hasMFDerivWithinAt_iff_hasFDerivWithinAt]

Premises used: hasDerivWithinAt_iff_hasFDerivWithinAt, hasMFDerivWithinAt_iff_hasFDerivWithinAt
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
t₀ : ℝ
inst_5 : IsManifold I 1 M
hγ : IsMIntegralCurveOn γ v s
t : ℝ
ht : t ∈ s
hsrc : γ t ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (γ t₀))).source
apply :
  Eq (α := TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace 𝓘(ℝ, E) (((↑(extChartAt I (γ t₀)) : M → E) ∘ γ) t))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I (γ t)) (mfderiv% (↑(chartAt H (γ t₀)) : M → H) (γ t))
        (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t))) :
      TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
    (ContinuousLinearMap.toSpanSingleton ℝ
        ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) :
      ℝ →L[ℝ] E)
⊢ HasMFDerivWithinAt 𝓘(ℝ, ℝ) 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ) s t
    (ContinuousLinearMap.toSpanSingleton ℝ
      ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))))

Tactic:
apply (HasMFDerivWithinAt.comp t (hasMFDerivWithinAt_extChartAt (I := I) hsrc) (hγ _ ht)
    (Set.subset_preimage_image _ _)).congr_mfderiv

Premises used: hasMFDerivWithinAt_extChartAt, HasMFDerivWithinAt.congr_mfderiv, HasMFDerivWithinAt.comp, Set.subset_preimage_image
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
t₀ : ℝ
inst_5 : IsManifold I 1 M
hγ : IsMIntegralCurveOn γ v s
t : ℝ
ht : t ∈ s
hsrc : γ t ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (γ t₀))).source
rw :
  ∀ (x : TangentSpace 𝓘(ℝ, ℝ) t),
    Eq (α := TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
      (((ContinuousLinearMap.comp (M₂ := TangentSpace I (γ t)) (mfderiv% (↑(chartAt H (γ t₀)) : M → H) (γ t))
                (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t))) :
              TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t))) :
            (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
          x :
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
      ((ContinuousLinearMap.toSpanSingleton ℝ
              ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) :
            (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
          x :
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace 𝓘(ℝ, E) (((↑(extChartAt I (γ t₀)) : M → E) ∘ γ) t))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I (γ t)) (mfderiv% (↑(chartAt H (γ t₀)) : M → H) (γ t))
        (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t))) :
      TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
    (ContinuousLinearMap.toSpanSingleton ℝ
        ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) :
      ℝ →L[ℝ] E)

Tactic:
rw [ContinuousLinearMap.ext_iff]

Premises used: ContinuousLinearMap.ext_iff
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
t₀ : ℝ
inst_5 : IsManifold I 1 M
hγ : IsMIntegralCurveOn γ v s
t : ℝ
ht : t ∈ s
hsrc : γ t ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (γ t₀))).source
a : TangentSpace 𝓘(ℝ, ℝ) t
rw :
  Eq (α := TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
    ((ContinuousLinearMap.smulRight (S := ℝ) 1
            ((tangentCoordChange I (γ t) (γ t₀) (γ t) :
                (a : TangentSpace I (γ t)) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
              (v (γ t))) :
          (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
        ((1 : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, ℝ) t) a : TangentSpace 𝓘(ℝ, ℝ) t) :
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
    ((ContinuousLinearMap.toSpanSingleton ℝ
            ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) :
          (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
        ((1 : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, ℝ) t) a : TangentSpace 𝓘(ℝ, ℝ) t) :
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
⊢ Eq (α := TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
    (((ContinuousLinearMap.comp (M₂ := TangentSpace I (γ t)) (mfderiv% (↑(chartAt H (γ t₀)) : M → H) (γ t))
              (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t))) :
            TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t))) :
          (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
        a :
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
    ((ContinuousLinearMap.toSpanSingleton ℝ
            ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) :
          (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
        a :
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))

Tactic:
rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.smulRight_apply, map_smul,
    ← ContinuousLinearMap.one_apply (R₁ := ℝ) a, ← ContinuousLinearMap.smulRight_apply,
    mfderiv_chartAt_eq_tangentCoordChange hsrc]

Premises used: mfderiv_chartAt_eq_tangentCoordChange, ContinuousLinearMap.one_apply, ContinuousLinearMap.smulRight_apply, map_smul, ContinuousLinearMap.comp_apply
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
t₀ : ℝ
inst_5 : IsManifold I 1 M
hγ : IsMIntegralCurveOn γ v s
t : ℝ
ht : t ∈ s
hsrc : γ t ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (γ t₀))).source
a : TangentSpace 𝓘(ℝ, ℝ) t
⊢ Eq (α := TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
    ((ContinuousLinearMap.smulRight (S := ℝ) 1
            ((tangentCoordChange I (γ t) (γ t₀) (γ t) :
                (a : TangentSpace I (γ t)) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
              (v (γ t))) :
          (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
        ((1 : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, ℝ) t) a : TangentSpace 𝓘(ℝ, ℝ) t) :
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
    ((ContinuousLinearMap.toSpanSingleton ℝ
            ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) :
          (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
        ((1 : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, ℝ) t) a : TangentSpace 𝓘(ℝ, ℝ) t) :
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_5 : IsManifold I 1 M
hγ : IsMIntegralCurveAt γ v t₀
apply :
  ∀ (x : ℝ),
    γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 x ∧
        HasMFDerivAt 𝓘(ℝ, ℝ) I γ x (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ x))) →
      HasDerivAt ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ)
        ((tangentCoordChange I (γ x) (γ t₀) (γ x) : (a : E) → E) (v (γ x) : TangentSpace I (γ x))) x
⊢ ∀ᶠ (t : ℝ) in 𝓝 t₀,
    HasDerivAt ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ)
      ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) t

Tactic:
apply eventually_mem_nhds_iff.mpr
    (hγ.continuousAt.preimage_mem_nhds (extChartAt_source_mem_nhds (I := I) _)) |>.and hγ |>.mono

Premises used: Iff.mpr, ContinuousAt.preimage_mem_nhds, Filter.Eventually.and, eventually_mem_nhds_iff, IsMIntegralCurveAt.continuousAt, extChartAt_source_mem_nhds, Filter.Eventually.mono
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_5 : IsManifold I 1 M
hγ : IsMIntegralCurveAt γ v t₀
t : ℝ
ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t
ht2 : HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))
⊢ t ∈ γ ⁻¹' (extChartAt I (γ t₀)).source

Tactic:
have hsrc := mem_of_mem_nhds ht1
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_5 : IsManifold I 1 M
hγ : IsMIntegralCurveAt γ v t₀
t : ℝ
ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t
ht2 : HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))
hsrc : t ∈ γ ⁻¹' (extChartAt I (γ t₀)).source
⊢ γ t ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (γ t₀))).source

Tactic:
rw [mem_preimage, extChartAt_source I (γ t₀)] at hsrc

Premises used: extChartAt_source, Set.mem_preimage
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_5 : IsManifold I 1 M
hγ : IsMIntegralCurveAt γ v t₀
t : ℝ
ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t
ht2 : HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))
hsrc : γ t ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (γ t₀))).source
rw :
  HasMFDerivAt 𝓘(ℝ, ℝ) 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ) t
    (ContinuousLinearMap.toSpanSingleton ℝ
      ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))))
⊢ HasDerivAt ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ)
    ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) t

Tactic:
rw [hasDerivAt_iff_hasFDerivAt, ← hasMFDerivAt_iff_hasFDerivAt]

Premises used: hasDerivAt_iff_hasFDerivAt, hasMFDerivAt_iff_hasFDerivAt
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_5 : IsManifold I 1 M
hγ : IsMIntegralCurveAt γ v t₀
t : ℝ
ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t
ht2 : HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))
hsrc : γ t ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (γ t₀))).source
apply :
  Eq (α := TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace 𝓘(ℝ, E) (((↑(extChartAt I (γ t₀)) : M → E) ∘ γ) t))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I (γ t)) (mfderiv% (↑(chartAt H (γ t₀)) : M → H) (γ t))
        (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t))) :
      TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
    (ContinuousLinearMap.toSpanSingleton ℝ
        ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) :
      ℝ →L[ℝ] E)
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ) t
    (ContinuousLinearMap.toSpanSingleton ℝ
      ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))))

Tactic:
apply (HasMFDerivAt.comp t (hasMFDerivAt_extChartAt (I := I) hsrc) ht2).congr_mfderiv

Premises used: HasMFDerivAt.congr_mfderiv, hasMFDerivAt_extChartAt, HasMFDerivAt.comp
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_5 : IsManifold I 1 M
hγ : IsMIntegralCurveAt γ v t₀
t : ℝ
ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t
ht2 : HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))
hsrc : γ t ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (γ t₀))).source
rw :
  ∀ (x : TangentSpace 𝓘(ℝ, ℝ) t),
    Eq (α := TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
      (((ContinuousLinearMap.comp (M₂ := TangentSpace I (γ t)) (mfderiv% (↑(chartAt H (γ t₀)) : M → H) (γ t))
                (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t))) :
              TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t))) :
            (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
          x :
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
      ((ContinuousLinearMap.toSpanSingleton ℝ
              ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) :
            (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
          x :
        TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace 𝓘(ℝ, E) (((↑(extChartAt I (γ t₀)) : M → E) ∘ γ) t))
    (ContinuousLinearMap.comp (M₂ := TangentSpace I (γ t)) (mfderiv% (↑(chartAt H (γ t₀)) : M → H) (γ t))
        (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t))) :
      TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
    (ContinuousLinearMap.toSpanSingleton ℝ
        ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) :
      ℝ →L[ℝ] E)

Tactic:
rw [ContinuousLinearMap.ext_iff]

Premises used: ContinuousLinearMap.ext_iff
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_5 : IsManifold I 1 M
hγ : IsMIntegralCurveAt γ v t₀
t : ℝ
ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t
ht2 : HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))
hsrc : γ t ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (γ t₀))).source
a : TangentSpace 𝓘(ℝ, ℝ) t
rw :
  Eq (α := TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
    ((ContinuousLinearMap.smulRight (S := ℝ) 1
            ((tangentCoordChange I (γ t) (γ t₀) (γ t) :
                (a : TangentSpace I (γ t)) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
              (v (γ t))) :
          (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
        ((1 : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, ℝ) t) a : TangentSpace 𝓘(ℝ, ℝ) t) :
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
    ((ContinuousLinearMap.toSpanSingleton ℝ
            ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) :
          (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
        ((1 : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, ℝ) t) a : TangentSpace 𝓘(ℝ, ℝ) t) :
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
⊢ Eq (α := TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
    (((ContinuousLinearMap.comp (M₂ := TangentSpace I (γ t)) (mfderiv% (↑(chartAt H (γ t₀)) : M → H) (γ t))
              (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t))) :
            TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t))) :
          (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
        a :
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
    ((ContinuousLinearMap.toSpanSingleton ℝ
            ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) :
          (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
        a :
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))

Tactic:
rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.smulRight_apply, map_smul,
    ← ContinuousLinearMap.one_apply (R₁ := ℝ) a, ← ContinuousLinearMap.smulRight_apply,
    mfderiv_chartAt_eq_tangentCoordChange hsrc]

Premises used: mfderiv_chartAt_eq_tangentCoordChange, ContinuousLinearMap.one_apply, ContinuousLinearMap.smulRight_apply, map_smul, ContinuousLinearMap.comp_apply
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_5 : IsManifold I 1 M
hγ : IsMIntegralCurveAt γ v t₀
t : ℝ
ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t
ht2 : HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))
hsrc : γ t ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (γ t₀))).source
a : TangentSpace 𝓘(ℝ, ℝ) t
⊢ Eq (α := TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
    ((ContinuousLinearMap.smulRight (S := ℝ) 1
            ((tangentCoordChange I (γ t) (γ t₀) (γ t) :
                (a : TangentSpace I (γ t)) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
              (v (γ t))) :
          (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
        ((1 : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, ℝ) t) a : TangentSpace 𝓘(ℝ, ℝ) t) :
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
    ((ContinuousLinearMap.toSpanSingleton ℝ
            ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) :
          (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))
        ((1 : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace 𝓘(ℝ, ℝ) t) a : TangentSpace 𝓘(ℝ, ℝ) t) :
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) (γ t)))

Tactic:
rfl
-- 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
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst_6 : CompleteSpace E
hv :
  ContMDiffAt I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1
    (fun (x : M) ↦ ⟨x, v x⟩) x₀
hx : I.IsInteriorPoint x₀
⊢ ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) x₀ ∧
    ContDiffWithinAt ℝ 1
      (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
        (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
        ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)))
      (range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)

Tactic:
rw [contMDiffAt_iff] at hv

Premises used: contMDiffAt_iff
-- 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
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst_6 : CompleteSpace E
hv :
  ContMDiffAt I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1
    (fun (x : M) ↦ ⟨x, v x⟩) x₀
hx : I.IsInteriorPoint x₀
hv₁ :
  ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) x₀ ∧
    ContDiffWithinAt ℝ 1
      (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
        (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
        ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)))
      (range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
⊢ I.IsInteriorPoint x₀

Tactic:
rw [contMDiffAt_iff] at hv

Premises used: contMDiffAt_iff
-- 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
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst_6 : CompleteSpace E
hv :
  ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) x₀ ∧
    ContDiffWithinAt ℝ 1
      (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
        (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
        ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)))
      (range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
hx : I.IsInteriorPoint x₀
⊢ ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) x₀

Tactic:
obtain ⟨_, hv⟩ := hv