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
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
⊢ ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ) t₀ = ((↑(extChartAt I (γ' t₀)) : M → E) ∘ γ') t₀
have rw : (↑(extChartAt I (γ t₀)) : M → E) (γ t₀) = ((↑(extChartAt I (γ' t₀)) : M → E) ∘ γ') t₀
Tactic: rw [Function.comp_apply, Function.comp_apply, 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
γ γ' : ℝ → 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
rw : (↑(extChartAt I (γ t₀)) : M → E) (γ t₀) = ((↑(extChartAt I (γ' t₀)) : M → E) ∘ γ') t₀
⊢ ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ) t₀ = ((↑(extChartAt I (γ' t₀)) : M → E) ∘ γ') t₀
have rw₁ : (↑(extChartAt I (γ t₀)) : M → E) (γ t₀) = (↑(extChartAt I (γ' t₀)) : M → E) (γ' t₀)
Tactic: rw [Function.comp_apply, Function.comp_apply, 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
γ γ' : ℝ → 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
rw : (↑(extChartAt I (γ t₀)) : M → E) (γ t₀) = ((↑(extChartAt I (γ' t₀)) : M → E) ∘ γ') t₀
rw₁ : (↑(extChartAt I (γ t₀)) : M → E) (γ t₀) = (↑(extChartAt I (γ' t₀)) : M → E) (γ' t₀)
⊢ ((↑(extChartAt I (γ t₀)) : M → E) ∘ γ) t₀ = ((↑(extChartAt I (γ' t₀)) : M → E) ∘ γ') t₀
have rw₂ : (↑(extChartAt I (γ' t₀)) : M → E) (γ' t₀) = (↑(extChartAt I (γ' t₀)) : M → E) (γ' t₀)
Tactic: rw [Function.comp_apply, Function.comp_apply, h]
-- 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₀ : ℝ
inst_6 : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv :
  ContMDiff 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⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
⊢ EqOn γ γ' (Ioo a b)
have hs : let s := {t : ℝ | γ t = γ' t} ∩ Ioo a b;
s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
Tactic: set s := {t | γ t = γ' t} ∩ Ioo a b with 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₀ : ℝ
inst_6 : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv :
  ContMDiff 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⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t : ℝ | γ t = γ' t} ∩ Ioo a b
hs : s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
⊢ EqOn γ γ' (Ioo a b)
have suffices : Ioo a b ⊆ s
Tactic: suffices hsub : Ioo a b ⊆ s from fun t ht ↦ mem_setOf.mp ((subset_def ▸ hsub) t ht).1
-- 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₀ : ℝ
inst_6 : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv :
  ContMDiff 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⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t : ℝ | γ t = γ' t} ∩ Ioo a b
hs : s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
⊢ Ioo a b ⊆ s
have apply : closure s ∩ Ioo a b ⊆ s
Tactic: apply isPreconnected_Ioo.subset_of_closure_inter_subset (s := Ioo a b) (u := s) _
    ⟨t₀, ⟨ht₀, ⟨h, 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₀ : ℝ
inst_6 : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv :
  ContMDiff 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⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t : ℝ | γ t = γ' t} ∩ Ioo a b
hs : s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
apply : closure s ∩ Ioo a b ⊆ s
⊢ Ioo a b ⊆ s
have apply₁ : IsOpen s
Tactic: apply isPreconnected_Ioo.subset_of_closure_inter_subset (s := Ioo a b) (u := s) _
    ⟨t₀, ⟨ht₀, ⟨h, 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₀ : ℝ
inst_6 : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv :
  ContMDiff 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⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t : ℝ | γ t = γ' t} ∩ Ioo a b
hs : s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
⊢ closure s ∩ Ioo a b ⊆ s
have rw : Subset (α := Set { x : ℝ // x ∈ Ioo a b })
  (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioo a b) ⁻¹'
    closure
      (image (α := { x : ℝ // x ∈ Ioo a b }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioo a b))
        {a_1 : { x : ℝ // x ∈ Ioo a b } | γ (↑a_1 : ℝ) = γ' (↑a_1 : ℝ)}))
  {a_1 : { x : ℝ // x ∈ Ioo a b } | γ (↑a_1 : ℝ) = γ' (↑a_1 : ℝ)}
Tactic: rw [hs, inter_comm, ← Subtype.image_preimage_val, inter_comm, ← Subtype.image_preimage_val,
      image_subset_image_iff Subtype.val_injective, preimage_setOf_eq]
-- 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₀ : ℝ
inst_6 : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv :
  ContMDiff 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⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t : ℝ | γ t = γ' t} ∩ Ioo a b
hs : s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
t : { x : ℝ // x ∈ Ioo a b }
ht :
  Membership.mem (γ := Set { x : ℝ // x ∈ Ioo a b })
    (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioo a b) ⁻¹'
      closure
        (image (α := { x : ℝ // x ∈ Ioo a b }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ Ioo a b))
          {a_1 : { x : ℝ // x ∈ Ioo a b } | γ (↑a_1 : ℝ) = γ' (↑a_1 : ℝ)}))
    t
⊢ Membership.mem (γ := Set { x : ℝ // x ∈ Ioo a b }) {a_1 : { x : ℝ // x ∈ Ioo a b } | γ (↑a_1 : ℝ) = γ' (↑a_1 : ℝ)} t
have ht₁ : Membership.mem (γ := Set { a_1 : ℝ // a_1 ∈ Ioo a b })
  (closure {a_1 : { x : ℝ // x ∈ Ioo a b } | γ (↑a_1 : ℝ) = γ' (↑a_1 : ℝ)}) t
Tactic: rw [mem_preimage, ← closure_subtype] at ht
Cleared hypotheses: 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₀ : ℝ
inst_6 : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv :
  ContMDiff 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⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t : ℝ | γ t = γ' t} ∩ Ioo a b
hs : s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
t : { x : ℝ // x ∈ Ioo a b }
ht :
  Membership.mem (γ := Set { a_1 : ℝ // a_1 ∈ Ioo a b })
    (closure {a_1 : { x : ℝ // x ∈ Ioo a b } | γ (↑a_1 : ℝ) = γ' (↑a_1 : ℝ)}) t
⊢ Membership.mem (γ := Set { x : ℝ // x ∈ Ioo a b }) {a_1 : { x : ℝ // x ∈ Ioo a b } | γ (↑a_1 : ℝ) = γ' (↑a_1 : ℝ)} t
have revert : ∀ ⦃t : { x : ℝ // x ∈ Ioo a b }⦄
  (ht :
    Membership.mem (γ := Set { a_1 : ℝ // a_1 ∈ Ioo a b })
      (closure {a_1 : { x : ℝ // x ∈ Ioo a b } | γ (↑a_1 : ℝ) = γ' (↑a_1 : ℝ)}) t),
  Membership.mem (γ := Set { x : ℝ // x ∈ Ioo a b }) {a_1 : { x : ℝ // x ∈ Ioo a b } | γ (↑a_1 : ℝ) = γ' (↑a_1 : ℝ)} t
Tactic: revert ht t
Cleared hypotheses: t, 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₀ : ℝ
inst_6 : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv :
  ContMDiff 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⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t : ℝ | γ t = γ' t} ∩ Ioo a b
hs : s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
⊢ ∀ ⦃t : { x : ℝ // x ∈ Ioo a b }⦄
    (ht :
      Membership.mem (γ := Set { a_1 : ℝ // a_1 ∈ Ioo a b })
        (closure {a_1 : { x : ℝ // x ∈ Ioo a b } | γ (↑a_1 : ℝ) = γ' (↑a_1 : ℝ)}) t),
    Membership.mem (γ := Set { x : ℝ // x ∈ Ioo a b }) {a_1 : { x : ℝ // x ∈ Ioo a b } | γ (↑a_1 : ℝ) = γ' (↑a_1 : ℝ)} t
have apply : Continuous[_, inst_3] fun (y : { x : ℝ // x ∈ Ioo a b }) ↦ γ (↑y : ℝ)
Tactic: apply IsClosed.closure_subset (isClosed_eq _ _)
-- 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₀ : ℝ
inst_6 : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv :
  ContMDiff 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⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t : ℝ | γ t = γ' t} ∩ Ioo a b
hs : s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
apply : Continuous[_, inst_3] fun (y : { x : ℝ // x ∈ Ioo a b }) ↦ γ (↑y : ℝ)
⊢ ∀ ⦃t : { x : ℝ // x ∈ Ioo a b }⦄
    (ht :
      Membership.mem (γ := Set { a_1 : ℝ // a_1 ∈ Ioo a b })
        (closure {a_1 : { x : ℝ // x ∈ Ioo a b } | γ (↑a_1 : ℝ) = γ' (↑a_1 : ℝ)}) t),
    Membership.mem (γ := Set { x : ℝ // x ∈ Ioo a b }) {a_1 : { x : ℝ // x ∈ Ioo a b } | γ (↑a_1 : ℝ) = γ' (↑a_1 : ℝ)} t
have apply₁ : Continuous[_, inst_3] fun (y : { x : ℝ // x ∈ Ioo a b }) ↦ γ' (↑y : ℝ)
Tactic: apply IsClosed.closure_subset (isClosed_eq _ _)
-- 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₀ : ℝ
inst_6 : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv :
  ContMDiff 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⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t : ℝ | γ t = γ' t} ∩ Ioo a b
hs : s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
⊢ Continuous[_, inst_3] fun (y : { x : ℝ // x ∈ Ioo a b }) ↦ γ (↑y : ℝ)
have rw : ∀ (x : { x : ℝ // x ∈ Ioo a b }), ContinuousAt.{0, u_3} (Y := M) (fun (y : { x : ℝ // x ∈ Ioo a b }) ↦ γ (↑y : ℝ)) x
Tactic: rw [continuous_iff_continuousAt]
-- 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₀ : ℝ
inst_6 : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv :
  ContMDiff 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⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t : ℝ | γ t = γ' t} ∩ Ioo a b
hs : s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
val : ℝ
ht : val ∈ Ioo a b
⊢ ContinuousAt.{0, u_3} (Y := M) (fun (y : { x : ℝ // x ∈ Ioo a b }) ↦ γ (↑y : ℝ))
    (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Ioo a b) val ht)
have apply : ContinuousAt γ (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Ioo a b) val ht) : ℝ)
Tactic: apply ContinuousAt.comp _ continuousAt_subtype_val
-- 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₀ : ℝ
inst_6 : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv :
  ContMDiff 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⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t : ℝ | γ t = γ' t} ∩ Ioo a b
hs : s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
val : ℝ
ht : val ∈ Ioo a b
⊢ ContinuousAt γ (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Ioo a b) val ht) : ℝ)
have rw : ContinuousAt γ val
Tactic: rw [Subtype.coe_mk]
-- 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₀ : ℝ
inst_6 : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv :
  ContMDiff 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⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t : ℝ | γ t = γ' t} ∩ Ioo a b
hs : s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
⊢ Continuous[_, inst_3] fun (y : { x : ℝ // x ∈ Ioo a b }) ↦ γ' (↑y : ℝ)
have rw : ∀ (x : { x : ℝ // x ∈ Ioo a b }), ContinuousAt.{0, u_3} (Y := M) (fun (y : { x : ℝ // x ∈ Ioo a b }) ↦ γ' (↑y : ℝ)) x
Tactic: rw [continuous_iff_continuousAt]
-- 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₀ : ℝ
inst_6 : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv :
  ContMDiff 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⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
s : Set ℝ := {t : ℝ | γ t = γ' t} ∩ Ioo a b
hs : s = {t : ℝ | γ t = γ' t} ∩ Ioo a b
val : ℝ
ht : val ∈ Ioo a b
⊢ ContinuousAt.{0, u_3} (Y := M) (fun (y : { x : ℝ // x ∈ Ioo a b }) ↦ γ' (↑y : ℝ))
    (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Ioo a b) val ht)
have apply : ContinuousAt γ' (↑(Subtype.mk (p := fun (x : ℝ) ↦ x ∈ Ioo a b) val ht) : ℝ)
Tactic: apply ContinuousAt.comp _ continuousAt_subtype_val