-- 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
⊢ HasDerivWithinAt (writtenInExtChartAt (modelWithCornersSelf ℝ ℝ) I t (↑(extChartAt I x₀).symm ∘ f))
    (v ((↑(extChartAt I x₀).symm ∘ f) t)) (range ↑(modelWithCornersSelf ℝ ℝ))
    (↑(extChartAt (modelWithCornersSelf ℝ ℝ) t) t)

Tactic:
simp only [mfld_simps, hasDerivWithinAt_univ]

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
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 ((↑I ∘ ↑(chartAt H (↑(chartAt H x₀).symm (↑I.symm (f t))))) ∘ (↑(chartAt H x₀).symm ∘ ↑I.symm) ∘ f)
    (v (↑(chartAt H x₀).symm (↑I.symm (f t)))) 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 :
  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₀

Tactic:
obtain ⟨_, hv⟩ := hv

Result:
case 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₀)
⊢ ∃ γ, γ 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
⊢ x₀ = (↑(extChartAt I x₀).symm ∘ f) t₀

Tactic:
rw [Function.comp_apply, hf1, PartialEquiv.left_inv _ (mem_extChartAt_source ..)]

Result:
no goals