awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
h : ∀ (t : ℝ), IsMIntegralCurveAt γ v t
t : ℝ
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))
have obtain : ∀ (s : Set ℝ) (hs : s ∈ 𝓝 t) (h : IsMIntegralCurveOn γ v s),
  HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))
Tactic: obtain ⟨s, hs, h⟩ := isMIntegralCurveAt_iff.mp (h t)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
h : ∀ t ∈ s, IsMIntegralCurveAt γ v t
t : ℝ
ht : t ∈ s
⊢ HasMFDerivWithinAt 𝓘(ℝ, ℝ) I γ s t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))
have h₁ : HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))
Tactic: apply HasMFDerivAt.hasMFDerivWithinAt
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
h : ∀ t ∈ s, IsMIntegralCurveAt γ v t
t : ℝ
ht : t ∈ s
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))
have h₁ : ∀ (s' : Set ℝ) (hs' : s' ∈ 𝓝 t)
  (h : ∀ y ∈ s', HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))),
  HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))
Tactic: obtain ⟨s', hs', h⟩ := Filter.eventually_iff_exists_mem.mp (h t ht)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (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
γ : ℝ → 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
⊢ HasDerivWithinAt ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ)
    ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) s t
have hsrc₁ : γ t ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (γ t₀))).source
Tactic: replace hsrc := extChartAt_source I (γ t₀) ▸ hsrc
Cleared hypotheses: hsrc
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (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
γ : ℝ → 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
⊢ HasDerivWithinAt ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ)
    ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) s t
have 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))))
Tactic: rw [hasDerivWithinAt_iff_hasFDerivWithinAt, ← hasMFDerivWithinAt_iff_hasFDerivWithinAt]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (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
γ : ℝ → 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
⊢ HasMFDerivWithinAt 𝓘(ℝ, ℝ) 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ) s t
    (ContinuousLinearMap.toSpanSingleton ℝ
      ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))))
have 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)
Tactic: apply (HasMFDerivWithinAt.comp t (hasMFDerivWithinAt_extChartAt (I := I) hsrc) (hγ _ ht)
    (Set.subset_preimage_image _ _)).congr_mfderiv
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (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
γ : ℝ → 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
⊢ 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)
have 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)))
Tactic: rw [ContinuousLinearMap.ext_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (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
γ : ℝ → 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.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)))
have 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)))
Tactic: rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.smulRight_apply, map_smul,
    ← ContinuousLinearMap.one_apply (R₁ := ℝ) a, ← ContinuousLinearMap.smulRight_apply,
    mfderiv_chartAt_eq_tangentCoordChange hsrc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst_5 : IsManifold I 1 M
hγ : IsMIntegralCurveAt γ v t₀
⊢ ∀ᶠ (t : ℝ) in 𝓝 t₀,
    HasDerivAt ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ)
      ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) t
have 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
Tactic: apply eventually_mem_nhds_iff.mpr
    (hγ.continuousAt.preimage_mem_nhds (extChartAt_source_mem_nhds (I := I) _)) |>.and hγ |>.mono
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (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
γ : ℝ → 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)))
⊢ HasDerivAt ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ)
    ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) t
have hsrc : t ∈ γ ⁻¹' (extChartAt I (γ t₀)).source
Tactic: have hsrc := mem_of_mem_nhds ht1
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (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
γ : ℝ → 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
⊢ HasDerivAt ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ)
    ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) t
have hsrc₁ : γ t ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H (γ t₀))).source
Tactic: rw [mem_preimage, extChartAt_source I (γ t₀)] at hsrc
Cleared hypotheses: hsrc
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (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
γ : ℝ → 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
⊢ HasDerivAt ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ)
    ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))) t
have rw : HasMFDerivAt 𝓘(ℝ, ℝ) 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ) t
  (ContinuousLinearMap.toSpanSingleton ℝ
    ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))))
Tactic: rw [hasDerivAt_iff_hasFDerivAt, ← hasMFDerivAt_iff_hasFDerivAt]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (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
γ : ℝ → 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
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) 𝓘(ℝ, E) ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ) t
    (ContinuousLinearMap.toSpanSingleton ℝ
      ((tangentCoordChange I (γ t) (γ t₀) (γ t) : (a : E) → E) (v (γ t) : TangentSpace I (γ t))))
have 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)
Tactic: apply (HasMFDerivAt.comp t (hasMFDerivAt_extChartAt (I := I) hsrc) ht2).congr_mfderiv
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (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
γ : ℝ → 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
⊢ 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)
have 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)))
Tactic: rw [ContinuousLinearMap.ext_iff]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.Basic (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
γ : ℝ → 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.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)))
have 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)))
Tactic: rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.smulRight_apply, map_smul,
    ← ContinuousLinearMap.one_apply (R₁ := ℝ) a, ← ContinuousLinearMap.smulRight_apply,
    mfderiv_chartAt_eq_tangentCoordChange hsrc]
-- 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
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₀
⊢ ∃ (γ : ℝ → M), γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
have 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₀)
Tactic: rw [contMDiffAt_iff] at hv
Cleared hypotheses: hv, hx
-- 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
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₀
⊢ ∃ (γ : ℝ → M), γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
have left : 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
Cleared hypotheses: hv
-- 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
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₀
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) x₀
⊢ ∃ (γ : ℝ → M), γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
have hv₁ : 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: obtain ⟨_, hv⟩ := hv
Cleared hypotheses: hv