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₀)
⊢ ∃ (γ : ℝ → M), γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
have obtain : ∀ (f : ℝ → E) (hf1 : f t₀ = (↑(extChartAt I x₀) : M → E) x₀)
  (hf2 :
    ∃ ε > 0,
      ∀ t ∈ Ioo (t₀ - ε) (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 t)).2
          t),
  ∃ (γ : ℝ → M), γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
Tactic: obtain ⟨f, hf1, hf2⟩ := hv.contDiffAt (range_mem_nhds_isInteriorPoint hx)
    |>.snd.exists_forall_mem_closedBall_exists_eq_forall_mem_Ioo_hasDerivAt₀ t₀
-- 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
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 :
  ∃ ε > 0,
    ∀ t ∈ Ioo (t₀ - ε) (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 t)).2
        t
⊢ ∃ (γ : ℝ → M), γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
have 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
Tactic: simp_rw [← Real.ball_eq_Ioo, ← Metric.eventually_nhds_iff_ball] at hf2
Cleared hypotheses: hf2
-- 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
⊢ ∃ (γ : ℝ → M), γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
have have : ∀ (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),
  ∃ (γ : ℝ → M), γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
Tactic: have ⟨a, ha, hf2'⟩ := Metric.eventually_nhds_iff_ball.mp hf2
-- 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
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
⊢ ∃ (γ : ℝ → M), γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
have hcont : ContinuousAt f t₀
Tactic: have hcont := (hf2' t₀ (Metric.mem_ball_self ha)).continuousAt
-- 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
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 : ContinuousAt f t₀
⊢ ∃ (γ : ℝ → M), γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
have hcont₁ : ∀ A ∈ 𝓝 ((↑(extChartAt I x₀) : M → E) x₀), f ⁻¹' A ∈ 𝓝 t₀
Tactic: rw [continuousAt_def, hf1] at hcont
Cleared hypotheses: hcont
-- 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
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₀
⊢ ∃ (γ : ℝ → M), γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
have hnhds : f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 t₀
Tactic: have hnhds : f ⁻¹' (interior (extChartAt I x₀).target) ∈ 𝓝 t₀ :=
    hcont _ (isOpen_interior.mem_nhds ((I.isInteriorPoint_iff).mp hx))
-- 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
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 : f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 t₀
⊢ ∃ (γ : ℝ → M), γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
have hnhds₁ : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'
Tactic: rw [← eventually_mem_nhds_iff] at hnhds
Cleared hypotheses: hnhds
-- 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'
⊢ ∃ (γ : ℝ → M), γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
have obtain : ∀ (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),
  ∃ (γ : ℝ → M), γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
Tactic: obtain ⟨s, hs, haux⟩ := (hf2.and hnhds).exists_mem
-- 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
⊢ x₀ = ((↑(extChartAt I x₀).symm : E → M) ∘ f) t₀
have rw : x₀ = (↑(extChartAt I x₀).symm : E → M) (f t₀)
Tactic: rw [Function.comp_apply, hf1, PartialEquiv.left_inv _ (mem_extChartAt_source ..)]
-- 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
rw : x₀ = (↑(extChartAt I x₀).symm : E → M) (f t₀)
⊢ x₀ = ((↑(extChartAt I x₀).symm : E → M) ∘ f) t₀
have rw₁ : x₀ = (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)
Tactic: rw [Function.comp_apply, hf1, PartialEquiv.left_inv _ (mem_extChartAt_source ..)]
-- 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
rw : x₀ = (↑(extChartAt I x₀).symm : E → M) (f t₀)
rw₁ : x₀ = (↑(extChartAt I x₀).symm : E → M) ((↑(extChartAt I x₀) : M → E) x₀)
⊢ x₀ = ((↑(extChartAt I x₀).symm : E → M) ∘ f) t₀
have rw₂ : x₀ = x₀
Tactic: rw [Function.comp_apply, hf1, PartialEquiv.left_inv _ (mem_extChartAt_source ..)]
-- 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
⊢ ∃ (γ : ℝ → M), γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
have refine : IsMIntegralCurveOn ((↑(extChartAt I x₀).symm : E → M) ∘ f) v s
Tactic: refine ⟨(extChartAt I x₀).symm ∘ f,
    Eq.symm (by rw [Function.comp_apply, hf1, PartialEquiv.left_inv _ (mem_extChartAt_source ..)]),
    isMIntegralCurveAt_iff.mpr ⟨s, hs, ?_⟩⟩