awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst_6 : CompleteSpace E
hx : I.IsInteriorPoint x₀
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) x₀
hv :
  ContDiffWithinAt ℝ 1
    (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
      (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
      ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
f : ℝ → E
hf1 : f t₀ = (↑(extChartAt I x₀) : M → E) x₀
hf2 :
  ∀ᶠ (y : ℝ) in 𝓝 t₀,
    HasDerivAt f
      (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
          (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
          ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
      y
a : ℝ
ha : a > 0
hf2' :
  ∀ y ∈ Metric.ball t₀ a,
    HasDerivAt f
      (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
          (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
          ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
      y
hcont : ∀ A ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) 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
        (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
            (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
            ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
        y ∧
      f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y
t : ℝ
ht : t ∈ s
xₜ : M := (↑(extChartAt I x₀).symm : E → M) (f t)
h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ : (a : E) → E) (v xₜ)) t
hf3 : f t ∈ interior (extChartAt I x₀).target
hf3' : f t ∈ (extChartAt I x₀).target
hft1 : (↑(extChartAt I x₀).symm : E → M) (f t) ∈ (extChartAt I x₀).source
hft2 : xₜ ∈ (extChartAt I xₜ).source
h₁ : HasDerivAt (((↑(extChartAt I xₜ) : M → E) ∘ (↑(extChartAt I x₀).symm : E → M)) ∘ f) (v xₜ) t
⊢ HasDerivAt
    (((↑I : H → E) ∘
        (↑(chartAt H ((↑(OpenPartialHomeomorph.symm (chartAt H x₀)) : H → M) ((↑I.symm : E → H) (f t)))) : M → H)) ∘
      ((↑(OpenPartialHomeomorph.symm (chartAt H x₀)) : H → M) ∘ (↑I.symm : E → H)) ∘ f)
    (v ((↑(OpenPartialHomeomorph.symm (chartAt H x₀)) : H → M) ((↑I.symm : E → H) (f t)))) t

Tactic:
change HasDerivAt ((extChartAt I xₜ ∘ (extChartAt I x₀).symm) ∘ f) (v xₜ) t

Premises used: extChartAt, HasDerivAt, Function.comp, PartialEquiv.symm, PartialEquiv.toFun
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst_6 : CompleteSpace E
hx : I.IsInteriorPoint x₀
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) x₀
hv :
  ContDiffWithinAt ℝ 1
    (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
      (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
      ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
f : ℝ → E
hf1 : f t₀ = (↑(extChartAt I x₀) : M → E) x₀
hf2 :
  ∀ᶠ (y : ℝ) in 𝓝 t₀,
    HasDerivAt f
      (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
          (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
          ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
      y
a : ℝ
ha : a > 0
hf2' :
  ∀ y ∈ Metric.ball t₀ a,
    HasDerivAt f
      (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
          (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
          ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
      y
hcont : ∀ A ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) 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
        (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
            (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
            ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
        y ∧
      f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y
t : ℝ
ht : t ∈ s
xₜ : M := (↑(extChartAt I x₀).symm : E → M) (f t)
h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ : (a : E) → E) (v xₜ)) t
hf3 : f t ∈ interior (extChartAt I x₀).target
hf3' : f t ∈ (extChartAt I x₀).target
hft1 : (↑(extChartAt I x₀).symm : E → M) (f t) ∈ (extChartAt I x₀).source
hft2 : xₜ ∈ (extChartAt I xₜ).source
h₁ :
  HasDerivAt (((↑(extChartAt I xₜ) : M → E) ∘ (↑(extChartAt I x₀).symm : E → M)) ∘ f)
    ((tangentCoordChange I x₀ xₜ xₜ : (a : E) → E) ((tangentCoordChange I xₜ x₀ xₜ : (a : E) → E) (v xₜ) : E)) t
⊢ HasDerivAt (((↑(extChartAt I xₜ) : M → E) ∘ (↑(extChartAt I x₀).symm : E → M)) ∘ f) (v xₜ) t

Tactic:
rw [← tangentCoordChange_self (I := I) (x := xₜ) (z := xₜ) (v := v xₜ) hft2,
    ← tangentCoordChange_comp (x := x₀) ⟨⟨hft2, hft1⟩, hft2⟩]

Premises used: tangentCoordChange_comp, tangentCoordChange_self, And.intro
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst_6 : CompleteSpace E
hx : I.IsInteriorPoint x₀
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) x₀
hv :
  ContDiffWithinAt ℝ 1
    (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
      (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
      ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
f : ℝ → E
hf1 : f t₀ = (↑(extChartAt I x₀) : M → E) x₀
hf2 :
  ∀ᶠ (y : ℝ) in 𝓝 t₀,
    HasDerivAt f
      (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
          (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
          ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
      y
a : ℝ
ha : a > 0
hf2' :
  ∀ y ∈ Metric.ball t₀ a,
    HasDerivAt f
      (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
          (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
          ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
      y
hcont : ∀ A ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) 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
        (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
            (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
            ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
        y ∧
      f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y
t : ℝ
ht : t ∈ s
xₜ : M := (↑(extChartAt I x₀).symm : E → M) (f t)
h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ : (a : E) → E) (v xₜ)) t
hf3 : f t ∈ interior (extChartAt I x₀).target
hf3' : f t ∈ (extChartAt I x₀).target
hft1 : (↑(extChartAt I x₀).symm : E → M) (f t) ∈ (extChartAt I x₀).source
hft2 : xₜ ∈ (extChartAt I xₜ).source
apply :
  HasFDerivAt ((↑(extChartAt I xₜ) : M → E) ∘ (↑(extChartAt I x₀).symm : E → M)) (tangentCoordChange I x₀ xₜ xₜ) (f t)
⊢ HasDerivAt (((↑(extChartAt I xₜ) : M → E) ∘ (↑(extChartAt I x₀).symm : E → M)) ∘ f)
    ((tangentCoordChange I x₀ xₜ xₜ : (a : E) → E) ((tangentCoordChange I xₜ x₀ xₜ : (a : E) → E) (v xₜ) : E)) t

Tactic:
apply HasFDerivAt.comp_hasDerivAt _ _ h

Premises used: HasFDerivAt.comp_hasDerivAt
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst_6 : CompleteSpace E
hx : I.IsInteriorPoint x₀
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) x₀
hv :
  ContDiffWithinAt ℝ 1
    (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
      (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
      ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
f : ℝ → E
hf1 : f t₀ = (↑(extChartAt I x₀) : M → E) x₀
hf2 :
  ∀ᶠ (y : ℝ) in 𝓝 t₀,
    HasDerivAt f
      (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
          (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
          ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
      y
a : ℝ
ha : a > 0
hf2' :
  ∀ y ∈ Metric.ball t₀ a,
    HasDerivAt f
      (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
          (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
          ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
      y
hcont : ∀ A ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) 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
        (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
            (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
            ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
        y ∧
      f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y
t : ℝ
ht : t ∈ s
xₜ : M := (↑(extChartAt I x₀).symm : E → M) (f t)
h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ : (a : E) → E) (v xₜ)) t
hf3 : f t ∈ interior (extChartAt I x₀).target
hf3' : f t ∈ (extChartAt I x₀).target
hft1 : (↑(extChartAt I x₀).symm : E → M) (f t) ∈ (extChartAt I x₀).source
hft2 : xₜ ∈ (extChartAt I xₜ).source
apply :
  HasFDerivWithinAt ((↑(extChartAt I xₜ) : M → E) ∘ (↑(extChartAt I x₀).symm : E → M)) (tangentCoordChange I x₀ xₜ xₜ)
    (range (↑I : H → E)) (f t)
⊢ HasFDerivAt ((↑(extChartAt I xₜ) : M → E) ∘ (↑(extChartAt I x₀).symm : E → M)) (tangentCoordChange I x₀ xₜ xₜ) (f t)

Tactic:
apply HasFDerivWithinAt.hasFDerivAt (s := range I) _ <|
    mem_nhds_iff.mpr ⟨interior (extChartAt I x₀).target,
      subset_trans interior_subset (extChartAt_target_subset_range ..),
      isOpen_interior, hf3⟩

Premises used: Iff.mpr, extChartAt, interior_subset, mem_nhds_iff, PartialEquiv.target, isOpen_interior, subset_trans, extChartAt_target_subset_range, And.intro, interior, Exists.intro, HasFDerivWithinAt.hasFDerivAt
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst_6 : CompleteSpace E
hx : I.IsInteriorPoint x₀
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) x₀
hv :
  ContDiffWithinAt ℝ 1
    (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
      (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
      ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
f : ℝ → E
hf1 : f t₀ = (↑(extChartAt I x₀) : M → E) x₀
hf2 :
  ∀ᶠ (y : ℝ) in 𝓝 t₀,
    HasDerivAt f
      (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
          (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
          ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
      y
a : ℝ
ha : a > 0
hf2' :
  ∀ y ∈ Metric.ball t₀ a,
    HasDerivAt f
      (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
          (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
          ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
      y
hcont : ∀ A ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) 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
        (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
            (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
            ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
        y ∧
      f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y
t : ℝ
ht : t ∈ s
xₜ : M := (↑(extChartAt I x₀).symm : E → M) (f t)
h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ : (a : E) → E) (v xₜ)) t
hf3 : f t ∈ interior (extChartAt I x₀).target
hf3' : f t ∈ (extChartAt I x₀).target
hft1 : (↑(extChartAt I x₀).symm : E → M) (f t) ∈ (extChartAt I x₀).source
hft2 : xₜ ∈ (extChartAt I xₜ).source
rw :
  HasFDerivWithinAt ((↑(extChartAt I xₜ) : M → E) ∘ (↑(extChartAt I x₀).symm : E → M)) (tangentCoordChange I x₀ xₜ xₜ)
    (range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) ((↑(extChartAt I x₀).symm : E → M) (f t)))
⊢ HasFDerivWithinAt ((↑(extChartAt I xₜ) : M → E) ∘ (↑(extChartAt I x₀).symm : E → M)) (tangentCoordChange I x₀ xₜ xₜ)
    (range (↑I : H → E)) (f t)

Tactic:
rw [← (extChartAt I x₀).right_inv hf3']

Premises used: extChartAt, PartialEquiv.right_inv
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst_6 : CompleteSpace E
hx : I.IsInteriorPoint x₀
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) x₀
hv :
  ContDiffWithinAt ℝ 1
    (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
      (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
      ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
f : ℝ → E
hf1 : f t₀ = (↑(extChartAt I x₀) : M → E) x₀
hf2 :
  ∀ᶠ (y : ℝ) in 𝓝 t₀,
    HasDerivAt f
      (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
          (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
          ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
      y
a : ℝ
ha : a > 0
hf2' :
  ∀ y ∈ Metric.ball t₀ a,
    HasDerivAt f
      (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
          (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
          ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
      y
hcont : ∀ A ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) 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
        (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
            (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
            ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
        y ∧
      f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y
t : ℝ
ht : t ∈ s
xₜ : M := (↑(extChartAt I x₀).symm : E → M) (f t)
h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ : (a : E) → E) (v xₜ)) t
hf3 : f t ∈ interior (extChartAt I x₀).target
hf3' : f t ∈ (extChartAt I x₀).target
hft1 : (↑(extChartAt I x₀).symm : E → M) (f t) ∈ (extChartAt I x₀).source
hft2 : xₜ ∈ (extChartAt I xₜ).source
⊢ HasFDerivWithinAt ((↑(extChartAt I xₜ) : M → E) ∘ (↑(extChartAt I x₀).symm : E → M)) (tangentCoordChange I x₀ xₜ xₜ)
    (range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) ((↑(extChartAt I x₀).symm : E → M) (f t)))

Tactic:
hasFDerivWithinAt_tangentCoordChange ⟨hft1, hft2⟩

Premises used: hasFDerivWithinAt_tangentCoordChange, And.intro
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst_6 : CompleteSpace E
hx : I.IsInteriorPoint x₀
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) x₀
hv :
  ContDiffWithinAt ℝ 1
    (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
      (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
      ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)))
    (range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) x₀)
f : ℝ → E
hf1 : f t₀ = (↑(extChartAt I x₀) : M → E) x₀
hf2 :
  ∀ᶠ (y : ℝ) in 𝓝 t₀,
    HasDerivAt f
      (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
          (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
          ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
      y
a : ℝ
ha : a > 0
hf2' :
  ∀ y ∈ Metric.ball t₀ a,
    HasDerivAt f
      (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
          (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
          ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
      y
hcont : ∀ A ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) 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
        (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
            (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨x₀, v x₀⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
            ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I x₀).symm : E → M)) (f y)).2
        y ∧
      f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y
t : ℝ
ht : t ∈ s
xₜ : M := (↑(extChartAt I x₀).symm : E → M) (f t)
h : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ : (a : E) → E) (v xₜ)) t
hf3 : f t ∈ interior (extChartAt I x₀).target
hf3' : f t ∈ (extChartAt I x₀).target
hft1 : (↑(extChartAt I x₀).symm : E → M) (f t) ∈ (extChartAt I x₀).source
hft2 : xₜ ∈ (extChartAt I xₜ).source
⊢ HasFDerivWithinAt ((↑(extChartAt I xₜ) : M → E) ∘ (↑(extChartAt I x₀).symm : E → M)) (tangentCoordChange I x₀ xₜ xₜ)
    (range (↑I : H → E)) ((↑(extChartAt I x₀) : M → E) ((↑(extChartAt I x₀).symm : E → M) (f t)))

Tactic:
exact hasFDerivWithinAt_tangentCoordChange ⟨hft1, hft2⟩

Premises used: hasFDerivWithinAt_tangentCoordChange, And.intro
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst_6 : CompleteSpace E
inst_7 : BoundarylessManifold I M
hv :
  ContMDiffAt I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1
    (fun (x : M) ↦ ⟨x, v x⟩) x₀
⊢ ∃ (γ : ℝ → M), γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀

Tactic:
exists_isMIntegralCurveAt_of_contMDiffAt t₀ hv BoundarylessManifold.isInteriorPoint

Premises used: BoundarylessManifold.isInteriorPoint, exists_isMIntegralCurveAt_of_contMDiffAt
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hv :
  ContMDiffAt I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1
    (fun (x : M) ↦ ⟨x, v x⟩) (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
⊢ let v' : E → E := fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x));
  v' = fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))

Tactic:
set v' : E → E := fun x ↦
    tangentCoordChange I ((extChartAt I (γ t₀)).symm x) (γ t₀) ((extChartAt I (γ t₀)).symm x)
      (v ((extChartAt I (γ t₀)).symm x)) with hv'

Premises used: extChartAt, PartialEquiv.symm, tangentCoordChange, PartialEquiv.toFun, DFunLike.coe
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hv :
  ContMDiffAt I (I.prod 𝓘(ℝ, E)) (M' := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) 1
    (fun (x : M) ↦ ⟨x, v x⟩) (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
v' : E → E :=
  fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
hv' :
  v' = fun (x : E) ↦
    (tangentCoordChange I ((↑(extChartAt I (γ t₀)).symm : E → M) x) (γ t₀) ((↑(extChartAt I (γ t₀)).symm : E → M) x) :
        (a : E) → E)
      (v ((↑(extChartAt I (γ t₀)).symm : E → M) x) : TangentSpace I ((↑(extChartAt I (γ t₀)).symm : E → M) x))
⊢ ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) (γ t₀) ∧
    ContDiffWithinAt ℝ 1
      (comp (β := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I))
        (↑(extChartAt (I.prod 𝓘(ℝ, E)) ⟨γ t₀, v (γ t₀)⟩) : Bundle.TotalSpace E (TangentSpace I) → E × E)
        ((fun (x : M) ↦ ⟨x, v x⟩) ∘ (↑(extChartAt I (γ t₀)).symm : E → M)))
      (range (↑I : H → E)) ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))

Tactic:
rw [contMDiffAt_iff] at hv

Premises used: contMDiffAt_iff