awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra
Goal:
R : Type u_1
inst : NormedRing R
inst_1 : CompleteSpace R
n_1 : ℕ∞ω
𝕜 : Type u_2
inst_2 : NontriviallyNormedField 𝕜
inst_3 : NormedAlgebra 𝕜 R
H : Type u_3
inst_4 : TopologicalSpace H
E : Type u_4
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_5
inst_7 : TopologicalSpace M
inst_8 : ChartedSpace H M
V : Type u_6
inst_9 : NormedAddCommGroup V
inst_10 : NormedSpace 𝕜 V
inst_11 : CompleteSpace V
n : ℕ∞ω
⊢ ContMDiffSMul (H := V →L[𝕜] V) 𝓘(𝕜, V →L[𝕜] V) 𝓘(𝕜, V) n (V →L[𝕜] V)ˣ V

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
h : IsMIntegralCurve γ v
s : Set ℝ
⊢ IsMIntegralCurveOn γ v s

Tactic:
fun t _ ↦ (h t).hasMFDerivWithinAt

Premises used: IsMIntegralCurveOn, HasMFDerivAt.hasMFDerivWithinAt
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
⊢ IsMIntegralCurve γ v ↔ IsMIntegralCurveOn γ v univ

Tactic:
⟨fun h ↦ h.isMIntegralCurveOn _, fun h t ↦ (h t (mem_univ _)).hasMFDerivAt Filter.univ_mem⟩

Premises used: Set.univ, IsMIntegralCurve.isMIntegralCurveOn, Iff.intro, Set.mem_univ, Filter.univ_mem, HasMFDerivWithinAt.hasMFDerivAt
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
mp : IsMIntegralCurveAt γ v t₀ → ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s
mpr : (∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s) → IsMIntegralCurveAt γ v t₀
⊢ IsMIntegralCurveAt γ v t₀ ↔ ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
h : IsMIntegralCurveAt γ v t₀
⊢ ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))

Tactic:
rw [IsMIntegralCurveAt, Filter.eventually_iff_exists_mem] at h

Premises used: IsMIntegralCurveAt, Filter.eventually_iff_exists_mem
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
h : ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))
mp :
  ∀ (s : Set ℝ) (hs : s ∈ 𝓝 t₀)
    (h : ∀ y ∈ s, HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))),
    ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s
⊢ ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s

Tactic:
obtain ⟨s, hs, h⟩ := h
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : ∀ y ∈ s, HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))
⊢ ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s

Tactic:
⟨s, hs, fun t ht ↦ (h t ht).hasMFDerivWithinAt⟩

Premises used: HasMFDerivAt.hasMFDerivWithinAt, And.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : ∀ y ∈ s, HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))
⊢ ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s

Tactic:
exact ⟨s, hs, fun t ht ↦ (h t ht).hasMFDerivWithinAt⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsMIntegralCurveOn γ v s
mpr : ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))
⊢ IsMIntegralCurveAt γ v t₀

Tactic:
rw [IsMIntegralCurveAt, Filter.eventually_iff_exists_mem]

Premises used: IsMIntegralCurveAt, Filter.eventually_iff_exists_mem
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsMIntegralCurveOn γ v s
mpr :
  ∀ (s' : Set ℝ) (h1 : s' ⊆ s) (h2 : IsOpen s') (h3 : t₀ ∈ s'),
    ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))
⊢ ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))

Tactic:
obtain ⟨s', h1, h2, h3⟩ := mem_nhds_iff.mp hs

Premises used: mem_nhds_iff, Iff.mp
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsMIntegralCurveOn γ v s
s' : Set ℝ
h1 : s' ⊆ s
h2 : IsOpen s'
h3 : t₀ ∈ s'
⊢ ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))

Tactic:
⟨s', h2.mem_nhds h3, ?_⟩

Premises used: And.intro, IsOpen.mem_nhds, Exists.intro
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsMIntegralCurveOn γ v s
s' : Set ℝ
h1 : s' ⊆ s
h2 : IsOpen s'
h3 : t₀ ∈ s'
mpr : ∀ y ∈ s', HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))
⊢ ∃ v_1 ∈ 𝓝 t₀, ∀ y ∈ v_1, HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))

Tactic:
refine ⟨s', h2.mem_nhds h3, ?_⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsMIntegralCurveOn γ v s
s' : Set ℝ
h1 : s' ⊆ s
h2 : IsOpen s'
h3 : t₀ ∈ s'
t : ℝ
ht : t ∈ s'
mpr : s ∈ 𝓝 t
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))

Tactic:
apply (h t (h1 ht)).hasMFDerivAt

Premises used: HasMFDerivWithinAt.hasMFDerivAt
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsMIntegralCurveOn γ v s
s' : Set ℝ
h1 : s' ⊆ s
h2 : IsOpen s'
h3 : t₀ ∈ s'
t : ℝ
ht : t ∈ s'
mpr : ∃ t_1 ⊆ s, IsOpen t_1 ∧ t ∈ t_1
⊢ s ∈ 𝓝 t

Tactic:
rw [mem_nhds_iff]

Premises used: mem_nhds_iff
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsMIntegralCurveOn γ v s
s' : Set ℝ
h1 : s' ⊆ s
h2 : IsOpen s'
h3 : t₀ ∈ s'
t : ℝ
ht : t ∈ s'
⊢ ∃ t_1 ⊆ s, IsOpen t_1 ∧ t ∈ t_1

Tactic:
⟨s', h1, h2, ht⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsMIntegralCurveOn γ v s
s' : Set ℝ
h1 : s' ⊆ s
h2 : IsOpen s'
h3 : t₀ ∈ s'
t : ℝ
ht : t ∈ s'
⊢ ∃ t_1 ⊆ s, IsOpen t_1 ∧ t ∈ t_1

Tactic:
exact ⟨s', h1, h2, ht⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
rw : (∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s) ↔ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ IsMIntegralCurveAt γ v t₀ ↔ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)

Tactic:
rw [isMIntegralCurveAt_iff]

Premises used: isMIntegralCurveAt_iff
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
mp : (∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s) → ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
mpr : (∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)) → ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s
⊢ (∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s) ↔ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsMIntegralCurveOn γ v s
⊢ ∃ ε > 0, Metric.ball t₀ ε ⊆ s

Tactic:
rw [Metric.mem_nhds_iff] at hs

Premises used: Metric.mem_nhds_iff
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t₀
h : IsMIntegralCurveOn γ v s
hs₁ : ∃ ε > 0, Metric.ball t₀ ε ⊆ s
⊢ IsMIntegralCurveOn γ v s

Tactic:
rw [Metric.mem_nhds_iff] at hs

Premises used: Metric.mem_nhds_iff
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
hs : ∃ ε > 0, Metric.ball t₀ ε ⊆ s
h : IsMIntegralCurveOn γ v s
mp : ∀ (ε : ℝ) (hε : ε > 0) (hε' : Metric.ball t₀ ε ⊆ s), ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)

Tactic:
obtain ⟨ε, hε, hε'⟩ := hs
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
h : IsMIntegralCurveOn γ v s
ε : ℝ
hε : ε > 0
hε' : Metric.ball t₀ ε ⊆ s
⊢ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)

Tactic:
⟨ε, hε, fun t ht ↦ (h t (hε' ht)).mono hε'⟩

Premises used: And.intro, Exists.intro, HasMFDerivWithinAt.mono
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
s : Set ℝ
h : IsMIntegralCurveOn γ v s
ε : ℝ
hε : ε > 0
hε' : Metric.ball t₀ ε ⊆ s
⊢ ∃ ε > 0, IsMIntegralCurveOn γ v (Metric.ball t₀ ε)

Tactic:
refine ⟨ε, hε, fun t ht ↦ (h t (hε' ht)).mono hε'⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s

Tactic:
⟨Metric.ball t₀ ε, Metric.ball_mem_nhds _ hε, h⟩

Premises used: Metric.ball, Metric.ball_mem_nhds, And.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ ∃ s ∈ 𝓝 t₀, IsMIntegralCurveOn γ v s

Tactic:
exact ⟨Metric.ball t₀ ε, Metric.ball_mem_nhds _ hε, h⟩
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
h : IsMIntegralCurve γ v
t : ℝ
⊢ IsMIntegralCurveAt γ v t

Tactic:
isMIntegralCurveAt_iff.mpr ⟨univ, Filter.univ_mem, fun t _ ↦ (h t).hasMFDerivWithinAt⟩

Premises used: Iff.mpr, Set.univ, isMIntegralCurveAt_iff, HasMFDerivAt.hasMFDerivWithinAt, And.intro, Exists.intro, Filter.univ_mem
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
h : ∀ (t : ℝ), IsMIntegralCurveAt γ v t
t : ℝ
obtain :
  ∀ (s : Set ℝ) (hs : s ∈ 𝓝 t) (h : IsMIntegralCurveOn γ v s),
    HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))

Tactic:
obtain ⟨s, hs, h⟩ := isMIntegralCurveAt_iff.mp (h t)

Premises used: isMIntegralCurveAt_iff, Iff.mp
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
h_1 : ∀ (t : ℝ), IsMIntegralCurveAt γ v t
t : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t
h : IsMIntegralCurveOn γ v s
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))

Tactic:
h t (mem_of_mem_nhds hs) |>.hasMFDerivAt hs

Premises used: mem_of_mem_nhds, HasMFDerivWithinAt.hasMFDerivAt
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
h_1 : ∀ (t : ℝ), IsMIntegralCurveAt γ v t
t : ℝ
s : Set ℝ
hs : s ∈ 𝓝 t
h : IsMIntegralCurveOn γ v s
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))

Tactic:
exact h t (mem_of_mem_nhds hs) |>.hasMFDerivAt hs

Premises used: mem_of_mem_nhds, HasMFDerivWithinAt.hasMFDerivAt
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s s' : Set ℝ
h : IsMIntegralCurveOn γ v s
hs : s' ⊆ s
⊢ IsMIntegralCurveOn γ v s'

Tactic:
fun t ht ↦ (h t (hs ht)).mono hs

Premises used: IsMIntegralCurveOn, HasMFDerivWithinAt.mono
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
h : IsMIntegralCurveAt γ v t₀
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I γ t₀ (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t₀)))

Tactic:
have ⟨_, hs, h⟩ := isMIntegralCurveAt_iff.mp h
  h t₀ (mem_of_mem_nhds hs) |>.hasMFDerivAt hs

Premises used: Real, ContinuousLinearMap.smulRight, _private.0.IsMIntegralCurveAt.hasMFDerivAt.match_1, HasMFDerivAt, isMIntegralCurveAt_iff, mem_of_mem_nhds, Iff.mp, modelWithCornersSelf, OfNat.ofNat, HasMFDerivWithinAt.hasMFDerivAt
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
t₀ : ℝ
h : IsMIntegralCurveOn γ v s
hs : s ∈ 𝓝 t₀
⊢ IsMIntegralCurveAt γ v t₀

Tactic:
isMIntegralCurveAt_iff.mpr ⟨s, hs, h⟩

Premises used: Iff.mpr, isMIntegralCurveAt_iff, And.intro, Exists.intro
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
h : ∀ t ∈ s, IsMIntegralCurveAt γ v t
t : ℝ
ht : t ∈ s
h₁ : HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))
⊢ HasMFDerivWithinAt 𝓘(ℝ, ℝ) I γ s t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))

Tactic:
apply HasMFDerivAt.hasMFDerivWithinAt

Premises used: HasMFDerivAt.hasMFDerivWithinAt
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
h : ∀ t ∈ s, IsMIntegralCurveAt γ v t
t : ℝ
ht : t ∈ s
h₁ :
  ∀ (s' : Set ℝ) (hs' : s' ∈ 𝓝 t)
    (h : ∀ y ∈ s', HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))),
    HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))

Tactic:
obtain ⟨s', hs', h⟩ := Filter.eventually_iff_exists_mem.mp (h t ht)

Premises used: Iff.mp, Filter.eventually_iff_exists_mem
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
h_1 : ∀ t ∈ s, IsMIntegralCurveAt γ v t
t : ℝ
ht : t ∈ s
s' : Set ℝ
hs' : s' ∈ 𝓝 t
h : ∀ y ∈ s', HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))

Tactic:
h _ (mem_of_mem_nhds hs')

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
h_1 : ∀ t ∈ s, IsMIntegralCurveAt γ v t
t : ℝ
ht : t ∈ s
s' : Set ℝ
hs' : s' ∈ 𝓝 t
h : ∀ y ∈ s', HasMFDerivAt 𝓘(ℝ, ℝ) I γ y (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ y)))
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight (S := ℝ) 1 (v (γ t)))

Tactic:
exact h _ (mem_of_mem_nhds hs')

Premises used: mem_of_mem_nhds
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
hs : IsOpen s
⊢ IsMIntegralCurveOn γ v s ↔ ∀ t ∈ s, IsMIntegralCurveAt γ v t

Tactic:
⟨fun h _ ht ↦ h.isMIntegralCurveAt (hs.mem_nhds ht), IsMIntegralCurveAt.isMIntegralCurveOn⟩

Premises used: IsMIntegralCurveOn.isMIntegralCurveAt, IsOpen.mem_nhds, Iff.intro, IsMIntegralCurveAt.isMIntegralCurveOn
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
t₀ : ℝ
hγ : IsMIntegralCurveOn γ v s
ht : t₀ ∈ s
⊢ ContinuousWithinAt γ s t₀

Tactic:
(hγ t₀ ht).1

Premises used: And.left
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
hγ : IsMIntegralCurveOn γ v s
⊢ ContinuousOn γ s

Tactic:
fun t ht ↦ (hγ t ht).continuousWithinAt

Premises used: HasMFDerivWithinAt.continuousWithinAt, ContinuousOn
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγ : IsMIntegralCurveAt γ v t₀
⊢ ContinuousAt γ t₀

Tactic:
have ⟨_, hs, hγ⟩ := isMIntegralCurveAt_iff.mp hγ
  hγ.continuousWithinAt (mem_of_mem_nhds hs) |>.continuousAt hs

Premises used: ContinuousAt, _private.0.IsMIntegralCurveAt.hasMFDerivAt.match_1, isMIntegralCurveAt_iff, mem_of_mem_nhds, IsMIntegralCurveOn.continuousWithinAt, Iff.mp, ContinuousWithinAt.continuousAt
-- Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
hγ : IsMIntegralCurve γ v
⊢ Continuous[_, inst_3] γ

Tactic:
continuous_iff_continuousAt.mpr fun t ↦ (hγ.isMIntegralCurveAt t).continuousAt

Premises used: Iff.mpr, IsMIntegralCurveAt.continuousAt, continuous_iff_continuousAt, IsMIntegralCurve.isMIntegralCurveAt