awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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
⊢ HasDerivWithinAt (writtenInExtChartAt 𝓘(ℝ, ℝ) I t ((↑(extChartAt I x₀).symm : E → M) ∘ f))
    (v (((↑(extChartAt I x₀).symm : E → M) ∘ f) t)) (range (↑𝓘(ℝ, ℝ) : ℝ → ℝ)) ((↑(extChartAt 𝓘(ℝ, ℝ) t) : ℝ → ℝ) t)
have h₁ : 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: simp only [mfld_simps, hasDerivWithinAt_univ]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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
⊢ 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
have h₁ : HasDerivAt (((↑(extChartAt I xₜ) : M → E) ∘ (↑(extChartAt I x₀).symm : E → M)) ∘ f) (v xₜ) t
Tactic: change HasDerivAt ((extChartAt I xₜ ∘ (extChartAt I x₀).symm) ∘ f) (v xₜ) t
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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
⊢ HasDerivAt (((↑(extChartAt I xₜ) : M → E) ∘ (↑(extChartAt I x₀).symm : E → M)) ∘ f) (v xₜ) t
have 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
Tactic: rw [← tangentCoordChange_self (I := I) (x := xₜ) (z := xₜ) (v := v xₜ) hft2,
    ← tangentCoordChange_comp (x := x₀) ⟨⟨hft2, hft1⟩, hft2⟩]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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
⊢ 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
have apply : HasFDerivAt ((↑(extChartAt I xₜ) : M → E) ∘ (↑(extChartAt I x₀).symm : E → M)) (tangentCoordChange I x₀ xₜ xₜ) (f t)
Tactic: apply HasFDerivAt.comp_hasDerivAt _ _ h
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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
⊢ HasFDerivAt ((↑(extChartAt I xₜ) : M → E) ∘ (↑(extChartAt I x₀).symm : E → M)) (tangentCoordChange I x₀ xₜ xₜ) (f t)
have apply : HasFDerivWithinAt ((↑(extChartAt I xₜ) : M → E) ∘ (↑(extChartAt I x₀).symm : E → M)) (tangentCoordChange I x₀ xₜ xₜ)
  (range (↑I : H → E)) (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⟩
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (goal)
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)) (f t)
have 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)))
Tactic: rw [← (extChartAt I x₀).right_inv hf3']
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (hypothesis)
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₀
⊢ γ =ᶠ[𝓝 t₀] γ'
have hv' : 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'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (hypothesis)
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))
⊢ γ =ᶠ[𝓝 t₀] γ'
have hv₁ : 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
Cleared hypotheses: hv, hγ, hγ', h, v', hv'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (hypothesis)
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 :
  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₀))
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))
⊢ γ =ᶠ[𝓝 t₀] γ'
have left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) (γ t₀)
Tactic: obtain ⟨_, hv⟩ := hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique (hypothesis)
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 :
  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₀))
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))
left : ContinuousAt (Y := Bundle.TotalSpace.{u_3, u_1, u_1} (B := M) E (TangentSpace I)) (fun (x : M) ↦ ⟨x, v x⟩) (γ t₀)
⊢ γ =ᶠ[𝓝 t₀] γ'
have hv₁ : 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: obtain ⟨_, hv⟩ := hv
Cleared hypotheses: hv