-- Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean
theorem exists_isIntegralCurveAt_of_contMDiffAt [CompleteSpace E]
    (hv : ContMDiffAt I I.tangent 1 (fun x ↦ (⟨x, v x⟩ : TangentBundle I M)) x₀)
    (hx : I.IsInteriorPoint x₀) :
    ∃ γ : ℝ → M, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v t₀

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I 1 M
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst✝ : CompleteSpace E
hx : I.IsInteriorPoint x₀
left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) x₀
hv :
  ContDiffWithinAt ℝ 1
    (↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘
      (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm)
    (range ↑I) (↑(extChartAt I x₀) x₀)
f : ℝ → E
hf1 : f t₀ = ↑(extChartAt I x₀) x₀
hf2 :
  ∀ᶠ (y : ℝ) in 𝓝 t₀,
    HasDerivAt f
      ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘
            (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm)
          (f y)).2
      y
a : ℝ
ha : a > 0
hf2' :
  ∀ y ∈ Metric.ball t₀ a,
    HasDerivAt f
      ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘
            (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm)
          (f y)).2
      y
hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀
hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'
s : Set ℝ
hs : s ∈ 𝓝 t₀
haux :
  ∀ y ∈ s,
    HasDerivAt f
        ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘
              (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm)
            (f y)).2
        y ∧
      f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y
t : ℝ
ht : t ∈ s
xₜ : M := ↑(extChartAt I x₀).symm (f t)
h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ) (v xₜ)) t
hf3 : f t ∈ interior (extChartAt I x₀).target
hf3' : f t ∈ (extChartAt I x₀).target
hft1 : ↑(extChartAt I x₀).symm (f t) ∈ (extChartAt I x₀).source
hft2 : xₜ ∈ (extChartAt I xₜ).source
⊢ HasFDerivWithinAt (↑(extChartAt I xₜ) ∘ ↑(extChartAt I x₀).symm) (tangentCoordChange I x₀ xₜ xₜ) (range ↑I)
    (↑(extChartAt I x₀) (↑(extChartAt I x₀).symm (f t)))

Tactic:
exact hasFDerivWithinAt_tangentCoordChange ⟨hft1, hft2⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I 1 M
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst✝ : CompleteSpace E
hx : I.IsInteriorPoint x₀
left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) x₀
hv :
  ContDiffWithinAt ℝ 1
    (↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘
      (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm)
    (range ↑I) (↑(extChartAt I x₀) x₀)
f : ℝ → E
hf1 : f t₀ = ↑(extChartAt I x₀) x₀
hf2 :
  ∀ᶠ (y : ℝ) in 𝓝 t₀,
    HasDerivAt f
      ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘
            (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm)
          (f y)).2
      y
a : ℝ
ha : a > 0
hf2' :
  ∀ y ∈ Metric.ball t₀ a,
    HasDerivAt f
      ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘
            (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm)
          (f y)).2
      y
hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀
hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'
s : Set ℝ
hs : s ∈ 𝓝 t₀
haux :
  ∀ y ∈ s,
    HasDerivAt f
        ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘
              (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm)
            (f y)).2
        y ∧
      f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y
t : ℝ
ht : t ∈ s
xₜ : M := ↑(extChartAt I x₀).symm (f t)
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I (↑(extChartAt I x₀).symm ∘ f) t
    (ContinuousLinearMap.smulRight 1 (v ((↑(extChartAt I x₀).symm ∘ f) t)))

Tactic:
have h : HasDerivAt f (x := t) <| fderivWithin ℝ (extChartAt I x₀ ∘ (extChartAt I xₜ).symm)
  (range I) (extChartAt I xₜ xₜ) (v xₜ) := (haux t ht).1

Result:
case intro.intro.intro.intro.intro
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I 1 M
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst✝ : CompleteSpace E
hx : I.IsInteriorPoint x₀
left✝ : ContinuousAt (fun x => { proj := x, snd := v x }) x₀
hv :
  ContDiffWithinAt ℝ 1
    (↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘
      (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm)
    (range ↑I) (↑(extChartAt I x₀) x₀)
f : ℝ → E
hf1 : f t₀ = ↑(extChartAt I x₀) x₀
hf2 :
  ∀ᶠ (y : ℝ) in 𝓝 t₀,
    HasDerivAt f
      ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘
            (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm)
          (f y)).2
      y
a : ℝ
ha : a > 0
hf2' :
  ∀ y ∈ Metric.ball t₀ a,
    HasDerivAt f
      ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘
            (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm)
          (f y)).2
      y
hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀
hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'
s : Set ℝ
hs : s ∈ 𝓝 t₀
haux :
  ∀ y ∈ s,
    HasDerivAt f
        ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘
              (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm)
            (f y)).2
        y ∧
      f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y
t : ℝ
ht : t ∈ s
xₜ : M := ↑(extChartAt I x₀).symm (f t)
h :
  HasDerivAt f
    ((fderivWithin ℝ (↑(extChartAt I x₀) ∘ ↑(extChartAt I xₜ).symm) (range ↑I) (↑(extChartAt I xₜ) xₜ)) (v xₜ)) t
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I (↑(extChartAt I x₀).symm ∘ f) t
    (ContinuousLinearMap.smulRight 1 (v ((↑(extChartAt I x₀).symm ∘ f) t)))