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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ 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₀)
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₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
hlip_1 : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith.{u_1, u_1} (α := E) (β := E) K ((fun (x : ℝ) ↦ v') t) ((fun (x : ℝ) ↦ s) t)
hsrc : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀), ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
hmem : ∀ {g : ℝ → M} {t : ℝ} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t), g t ∈ (extChartAt I (g t₀)).source
g : ℝ → M
hg : IsMIntegralCurveAt g v t₀
h' : γ t₀ = g t₀
t : ℝ
ht1 : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
ht2 :
  HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g)
    ((tangentCoordChange I (g t) (g t₀) (g t) : (a : E) → E) (v (g t) : TangentSpace I (g t))) t
a : g t = (↑(extChartAt I (g t₀)).symm : E → M) ((↑(extChartAt I (g t₀)) : M → E) (g t))
⊢ g t = (↑(extChartAt I (g t₀)).symm : E → M) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)
have a₁ : g t = g t
Tactic: rw [Function.comp_apply, PartialEquiv.left_inv _ (hmem ht1)]
-- 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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ 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₀)
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₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
hlip_1 : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith.{u_1, u_1} (α := E) (β := E) K ((fun (x : ℝ) ↦ v') t) ((fun (x : ℝ) ↦ s) t)
hsrc : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀), ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
hmem : ∀ {g : ℝ → M} {t : ℝ} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t), g t ∈ (extChartAt I (g t₀)).source
g : ℝ → M
hg : IsMIntegralCurveAt g v t₀
h' : γ t₀ = g t₀
⊢ ∀ᶠ (x : ℝ) in 𝓝 t₀, Membership.mem (γ := Set E) ((fun (x : ℝ) ↦ s) x) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) x)
have a : s ∈ 𝓝 (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t₀)
Tactic: apply ((continuousAt_extChartAt (g t₀)).comp hg.continuousAt).preimage_mem_nhds
-- 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₀)
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₀)
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₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
hlip_1 : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith.{u_1, u_1} (α := E) (β := E) K ((fun (x : ℝ) ↦ v') t) ((fun (x : ℝ) ↦ s) t)
hsrc : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀), ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
hmem : ∀ {g : ℝ → M} {t : ℝ} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t), g t ∈ (extChartAt I (g t₀)).source
⊢ γ =ᶠ[𝓝 t₀] γ'
have hdrv : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀) (h' : γ t₀ = g t₀),
  ∀ᶠ (t : ℝ) in 𝓝 t₀,
    HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g) ((fun (x : ℝ) ↦ v') t (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t))
        t ∧
      Membership.mem (γ := Set E) ((fun (x : ℝ) ↦ s) t) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)
Tactic: have hdrv {g} (hg : IsMIntegralCurveAt g v t₀) (h' : γ t₀ = g t₀) : ∀ᶠ t in 𝓝 t₀,
      HasDerivAt ((extChartAt I (g t₀)) ∘ g) ((fun _ ↦ v') t (((extChartAt I (g t₀)) ∘ g) t)) t ∧
      ((extChartAt I (g t₀)) ∘ g) t ∈ (fun _ ↦ s) t := by
    apply Filter.Eventually.and
    · apply (hsrc hg |>.and hg.eventually_hasDerivAt).mono
      rintro t ⟨ht1, ht2⟩
      rw [hv', h']
      apply ht2.congr_deriv
      congr <;>
      rw [Function.comp_apply, PartialEquiv.left_inv _ (hmem ht1)]
    · apply ((continuousAt_extChartAt (g t₀)).comp hg.continuousAt).preimage_mem_nhds
      rw [Function.comp_apply, ← h']
      exact hs
-- 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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ 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₀)
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₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
hlip_1 : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith.{u_1, u_1} (α := E) (β := E) K ((fun (x : ℝ) ↦ v') t) ((fun (x : ℝ) ↦ s) t)
hsrc : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀), ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
hmem : ∀ {g : ℝ → M} {t : ℝ} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t), g t ∈ (extChartAt I (g t₀)).source
hdrv :
  ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀) (h' : γ t₀ = g t₀),
    ∀ᶠ (t : ℝ) in 𝓝 t₀,
      HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g)
          ((fun (x : ℝ) ↦ v') t (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)) t ∧
        Membership.mem (γ := Set E) ((fun (x : ℝ) ↦ s) t) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)
g : ℝ → M
hg : IsMIntegralCurveAt g v t₀
⊢ g =ᶠ[𝓝 t₀] (↑(extChartAt I (g t₀)).symm : E → M) ∘ (↑(extChartAt I (g t₀)) : M → E) ∘ g
have apply : ∀ (x : ℝ),
  g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 x →
    g x = ((↑(extChartAt I (g t₀)).symm : E → M) ∘ (↑(extChartAt I (g t₀)) : M → E) ∘ g) x
Tactic: apply (hsrc hg).mono
-- 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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ 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₀)
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₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
hlip_1 : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith.{u_1, u_1} (α := E) (β := E) K ((fun (x : ℝ) ↦ v') t) ((fun (x : ℝ) ↦ s) t)
hsrc : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀), ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
hmem : ∀ {g : ℝ → M} {t : ℝ} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t), g t ∈ (extChartAt I (g t₀)).source
hdrv :
  ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀) (h' : γ t₀ = g t₀),
    ∀ᶠ (t : ℝ) in 𝓝 t₀,
      HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g)
          ((fun (x : ℝ) ↦ v') t (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)) t ∧
        Membership.mem (γ := Set E) ((fun (x : ℝ) ↦ s) t) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)
g : ℝ → M
hg : IsMIntegralCurveAt g v t₀
t : ℝ
ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
⊢ g t = ((↑(extChartAt I (g t₀)).symm : E → M) ∘ (↑(extChartAt I (g t₀)) : M → E) ∘ g) t
have rw : g t = (↑(extChartAt I (g t₀)).symm : E → M) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)
Tactic: rw [Function.comp_apply, Function.comp_apply, PartialEquiv.left_inv _ (hmem ht)]
-- 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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ 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₀)
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₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
hlip_1 : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith.{u_1, u_1} (α := E) (β := E) K ((fun (x : ℝ) ↦ v') t) ((fun (x : ℝ) ↦ s) t)
hsrc : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀), ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
hmem : ∀ {g : ℝ → M} {t : ℝ} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t), g t ∈ (extChartAt I (g t₀)).source
hdrv :
  ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀) (h' : γ t₀ = g t₀),
    ∀ᶠ (t : ℝ) in 𝓝 t₀,
      HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g)
          ((fun (x : ℝ) ↦ v') t (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)) t ∧
        Membership.mem (γ := Set E) ((fun (x : ℝ) ↦ s) t) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)
g : ℝ → M
hg : IsMIntegralCurveAt g v t₀
t : ℝ
ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
rw : g t = (↑(extChartAt I (g t₀)).symm : E → M) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)
⊢ g t = ((↑(extChartAt I (g t₀)).symm : E → M) ∘ (↑(extChartAt I (g t₀)) : M → E) ∘ g) t
have rw₁ : g t = (↑(extChartAt I (g t₀)).symm : E → M) ((↑(extChartAt I (g t₀)) : M → E) (g t))
Tactic: rw [Function.comp_apply, Function.comp_apply, PartialEquiv.left_inv _ (hmem ht)]
-- 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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ 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₀)
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₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
hlip_1 : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith.{u_1, u_1} (α := E) (β := E) K ((fun (x : ℝ) ↦ v') t) ((fun (x : ℝ) ↦ s) t)
hsrc : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀), ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
hmem : ∀ {g : ℝ → M} {t : ℝ} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t), g t ∈ (extChartAt I (g t₀)).source
hdrv :
  ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀) (h' : γ t₀ = g t₀),
    ∀ᶠ (t : ℝ) in 𝓝 t₀,
      HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g)
          ((fun (x : ℝ) ↦ v') t (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)) t ∧
        Membership.mem (γ := Set E) ((fun (x : ℝ) ↦ s) t) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)
g : ℝ → M
hg : IsMIntegralCurveAt g v t₀
t : ℝ
ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
rw : g t = (↑(extChartAt I (g t₀)).symm : E → M) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)
rw₁ : g t = (↑(extChartAt I (g t₀)).symm : E → M) ((↑(extChartAt I (g t₀)) : M → E) (g t))
⊢ g t = ((↑(extChartAt I (g t₀)).symm : E → M) ∘ (↑(extChartAt I (g t₀)) : M → E) ∘ g) t
have rw₂ : g t = g t
Tactic: rw [Function.comp_apply, Function.comp_apply, PartialEquiv.left_inv _ (hmem ht)]
-- 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₀)
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₀)
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₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
hlip_1 : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith.{u_1, u_1} (α := E) (β := E) K ((fun (x : ℝ) ↦ v') t) ((fun (x : ℝ) ↦ s) t)
hsrc : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀), ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
hmem : ∀ {g : ℝ → M} {t : ℝ} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t), g t ∈ (extChartAt I (g t₀)).source
hdrv :
  ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀) (h' : γ t₀ = g t₀),
    ∀ᶠ (t : ℝ) in 𝓝 t₀,
      HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g)
          ((fun (x : ℝ) ↦ v') t (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)) t ∧
        Membership.mem (γ := Set E) ((fun (x : ℝ) ↦ s) t) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)
⊢ γ =ᶠ[𝓝 t₀] γ'
have heq : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀),
  g =ᶠ[𝓝 t₀] (↑(extChartAt I (g t₀)).symm : E → M) ∘ (↑(extChartAt I (g t₀)) : M → E) ∘ g
Tactic: have heq {g} (hg : IsMIntegralCurveAt g v t₀) :
    g =ᶠ[𝓝 t₀] (extChartAt I (g t₀)).symm ∘ ↑(extChartAt I (g t₀)) ∘ g := by
    apply (hsrc hg).mono
    intro t ht
    rw [Function.comp_apply, Function.comp_apply, PartialEquiv.left_inv _ (hmem ht)]
-- 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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ 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₀)
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₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 ((↑(extChartAt I (γ t₀)) : M → E) (γ t₀))
hlip_1 : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith.{u_1, u_1} (α := E) (β := E) K ((fun (x : ℝ) ↦ v') t) ((fun (x : ℝ) ↦ s) t)
hsrc : ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀), ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
hmem : ∀ {g : ℝ → M} {t : ℝ} (ht : g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t), g t ∈ (extChartAt I (g t₀)).source
hdrv :
  ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀) (h' : γ t₀ = g t₀),
    ∀ᶠ (t : ℝ) in 𝓝 t₀,
      HasDerivAt ((↑(extChartAt I (g t₀)) : M → E) ∘ g)
          ((fun (x : ℝ) ↦ v') t (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)) t ∧
        Membership.mem (γ := Set E) ((fun (x : ℝ) ↦ s) t) (((↑(extChartAt I (g t₀)) : M → E) ∘ g) t)
heq :
  ∀ {g : ℝ → M} (hg : IsMIntegralCurveAt g v t₀),
    g =ᶠ[𝓝 t₀] (↑(extChartAt I (g t₀)).symm : E → M) ∘ (↑(extChartAt I (g t₀)) : M → E) ∘ g
⊢ γ =ᶠ[𝓝 t₀] γ'
have suffices : (↑(extChartAt I (γ t₀)) : M → E) ∘ γ =ᶠ[𝓝 t₀] (↑(extChartAt I (γ' t₀)) : M → E) ∘ γ'
Tactic: suffices (extChartAt I (γ t₀)) ∘ γ =ᶠ[𝓝 t₀] (extChartAt I (γ' t₀)) ∘ γ' from
    (heq hγ).trans <| (this.fun_comp (extChartAt I (γ t₀)).symm).trans (h ▸ (heq hγ').symm)