-- 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:
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 ((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
⊢ HasDerivAt ((↑(extChartAt I xₜ) ∘ ↑(extChartAt I x₀).symm) ∘ f)
    ((tangentCoordChange I x₀ xₜ xₜ) ((tangentCoordChange I xₜ x₀ xₜ) (v xₜ))) t

Tactic:
apply HasFDerivAt.comp_hasDerivAt _ _ h

Result:
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
⊢ HasFDerivAt (↑(extChartAt I xₜ) ∘ ↑(extChartAt I x₀).symm) (tangentCoordChange I x₀ xₜ xₜ) (f t)

Proof state:
case 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 :
  ∃ ε > 0,
    ∀ t ∈ Ioo (t₀ - ε) (t₀ + ε),
      HasDerivAt f
        ((↑(extChartAt I.tangent { proj := x₀, snd := v x₀ }) ∘
              (fun x => { proj := x, snd := v x }) ∘ ↑(extChartAt I x₀).symm)
            (f t)).2
        t
⊢ ∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v t₀

Tactic:
simp_rw [← Real.ball_eq_Ioo, ← Metric.eventually_nhds_iff_ball] at hf2

Result:
case 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
⊢ ∃ γ, γ 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
hv : ContMDiffAt I I.tangent 1 (fun x => { proj := x, snd := v x }) x₀
hx : I.IsInteriorPoint x₀
⊢ ∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v t₀

Tactic:
rw [contMDiffAt_iff] at hv

Result:
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
hv :
  ContinuousAt (fun x => { proj := x, snd := v x }) x₀ ∧
    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₀)
hx : I.IsInteriorPoint x₀
⊢ ∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v t₀