awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ∀ᶠ (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)
⊢ HasMFDerivWithinAt 𝓘(ℝ, ℝ) I ((↑(extChartAt I x₀).symm : E → M) ∘ f) s t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (((↑(extChartAt I x₀).symm : E → M) ∘ f) t)))
have h : HasDerivAt f
  ((fderivWithin ℝ ((↑(extChartAt I x₀) : M → E) ∘ (↑(extChartAt I xₜ).symm : E → M)) (range (↑I : H → E))
        ((↑(extChartAt I xₜ) : M → E) xₜ) :
      (a : E) → E)
    (v xₜ))
  t
Tactic: have h : HasDerivAt f (x := t) <| fderivWithin ℝ (extChartAt I x₀ ∘ (extChartAt I xₜ).symm)
    (range I) (extChartAt I xₜ xₜ) (v xₜ) := (haux t ht).1
-- 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 : ∀ᶠ (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
    ((fderivWithin ℝ ((↑(extChartAt I x₀) : M → E) ∘ (↑(extChartAt I xₜ).symm : E → M)) (range (↑I : H → E))
          ((↑(extChartAt I xₜ) : M → E) xₜ) :
        (a : E) → E)
      (v xₜ))
    t
⊢ HasMFDerivWithinAt 𝓘(ℝ, ℝ) I ((↑(extChartAt I x₀).symm : E → M) ∘ f) s t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (((↑(extChartAt I x₀).symm : E → M) ∘ f) t)))
have h₁ : HasDerivAt f ((tangentCoordChange I xₜ x₀ xₜ : (a : E) → E) (v xₜ)) t
Tactic: rw [← tangentCoordChange_def] at h
Cleared hypotheses: 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
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
⊢ HasMFDerivWithinAt 𝓘(ℝ, ℝ) I ((↑(extChartAt I x₀).symm : E → M) ∘ f) s t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (((↑(extChartAt I x₀).symm : E → M) ∘ f) t)))
have hf3 : f t ∈ interior (extChartAt I x₀).target
Tactic: have hf3 := mem_preimage.mp <| mem_of_mem_nhds (haux t ht).2
-- 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 : ∀ᶠ (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
⊢ HasMFDerivWithinAt 𝓘(ℝ, ℝ) I ((↑(extChartAt I x₀).symm : E → M) ∘ f) s t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (((↑(extChartAt I x₀).symm : E → M) ∘ f) t)))
have hf3' : f t ∈ (extChartAt I x₀).target
Tactic: have hf3' := mem_of_mem_of_subset hf3 interior_subset
-- 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 : ∀ᶠ (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
⊢ HasMFDerivWithinAt 𝓘(ℝ, ℝ) I ((↑(extChartAt I x₀).symm : E → M) ∘ f) s t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (((↑(extChartAt I x₀).symm : E → M) ∘ f) t)))
have hft1 : (↑(extChartAt I x₀).symm : E → M) (f t) ∈ (extChartAt I x₀).source
Tactic: have hft1 := mem_preimage.mp <|
    mem_of_mem_of_subset hf3' (extChartAt I x₀).target_subset_preimage_source
-- 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 : ∀ᶠ (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
⊢ HasMFDerivWithinAt 𝓘(ℝ, ℝ) I ((↑(extChartAt I x₀).symm : E → M) ∘ f) s t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (((↑(extChartAt I x₀).symm : E → M) ∘ f) t)))
have hft2 : xₜ ∈ (extChartAt I xₜ).source
Tactic: have hft2 := mem_extChartAt_source (I := I) xₜ
-- 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
⊢ HasMFDerivWithinAt 𝓘(ℝ, ℝ) I ((↑(extChartAt I x₀).symm : E → M) ∘ f) s t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (((↑(extChartAt I x₀).symm : E → M) ∘ f) t)))
have h₁ : HasMFDerivAt 𝓘(ℝ, ℝ) I ((↑(extChartAt I x₀).symm : E → M) ∘ f) t
  (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (((↑(extChartAt I x₀).symm : E → M) ∘ f) t)))
Tactic: apply HasMFDerivAt.hasMFDerivWithinAt
-- 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
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I ((↑(extChartAt I x₀).symm : E → M) ∘ f) t
    (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (((↑(extChartAt I x₀).symm : E → M) ∘ f) t)))
have h₁ : HasDerivWithinAt (writtenInExtChartAt 𝓘(ℝ, ℝ) I t ((↑(extChartAt I x₀).symm : E → M) ∘ f))
  (v (((↑(extChartAt I x₀).symm : E → M) ∘ f) t)) (range (↑𝓘(ℝ, ℝ) : ℝ → ℝ)) ((↑(extChartAt 𝓘(ℝ, ℝ) t) : ℝ → ℝ) t)
Tactic: refine ⟨(continuousAt_extChartAt_symm'' hf3').comp h.continuousAt,
    HasDerivWithinAt.hasFDerivWithinAt ?_⟩