-- 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
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 : f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 t₀
⊢ ∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v t₀

Tactic:
rw [← eventually_mem_nhds_iff] at hnhds

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
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'
⊢ ∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v 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 :
  ∀ᶠ (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
⊢ ∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v t₀

Tactic:
have hcont := (hf2' t₀ (Metric.mem_ball_self ha)).continuousAt

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
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 : ContinuousAt f t₀
⊢ ∃ γ, γ t₀ = x₀ ∧ IsIntegralCurveAt γ v t₀