-- 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
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I (↑(extChartAt I x₀).symm ∘ f) t
    (ContinuousLinearMap.smulRight 1 (v ((↑(extChartAt I x₀).symm ∘ f) t)))

Tactic:
have hf3 := mem_preimage.mp <| mem_of_mem_nhds (haux t ht).2

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 ((tangentCoordChange I xₜ x₀ xₜ) (v xₜ)) t
hf3 : f t ∈ interior (extChartAt I x₀).target
⊢ HasMFDerivAt (modelWithCornersSelf ℝ ℝ) I (↑(extChartAt I x₀).symm ∘ f) t
    (ContinuousLinearMap.smulRight 1 (v ((↑(extChartAt I x₀).symm ∘ f) 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₀ = x₀ ∧ IsIntegralCurveAt γ v t₀

Tactic:
refine ⟨(extChartAt I x₀).symm ∘ f,
  Eq.symm (by rw [Function.comp_apply, hf1, PartialEquiv.left_inv _ (mem_extChartAt_source ..)]),
  isIntegralCurveAt_iff.mpr ⟨s, hs, ?_⟩⟩

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
⊢ IsIntegralCurveOn (↑(extChartAt I x₀).symm ∘ f) v s