mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : 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 ↦
    (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x))
      (v (↑(extChartAt I (γ t₀)).symm x))
hv' :
  v' = fun x ↦
    (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x))
      (v (↑(extChartAt I (γ t₀)).symm x))
left✝ : ContinuousAt (fun x ↦ ⟨x, v x⟩) (γ t₀)
hv :
  ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent ⟨γ t₀, v (γ t₀)⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I (γ t₀)).symm)
    (range ↑I) (↑(extChartAt I (γ t₀)) (γ t₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 (↑(extChartAt I (γ t₀)) (γ t₀))
hlip✝ : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith K ((fun x ↦ v') t) ((fun x ↦ s) t)
hsrc : ∀ {g : ℝ → M}, IsMIntegralCurveAt g v t₀ → ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
hmem : ∀ {g : ℝ → M} {t : ℝ}, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t → g t ∈ (extChartAt I (g t₀)).source
hdrv :
  ∀ {g : ℝ → M},
    IsMIntegralCurveAt g v t₀ →
      γ t₀ = g t₀ →
        ∀ᶠ (t : ℝ) in 𝓝 t₀,
          HasDerivAt (↑(extChartAt I (g t₀)) ∘ g) ((fun x ↦ v') t ((↑(extChartAt I (g t₀)) ∘ g) t)) t ∧
            (↑(extChartAt I (g t₀)) ∘ g) t ∈ (fun x ↦ s) t
g : ℝ → M
hg : IsMIntegralCurveAt g v t₀
⊢ g =ᶠ[𝓝 t₀] ↑(extChartAt I (g t₀)).symm ∘ ↑(extChartAt I (g t₀)) ∘ g

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t + (asup - ε / 2) ∈ Ioo (-ε) ε}
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
hγ2 : IsMIntegralCurveOn γ2 v {t | t - (asup - ε / 2) ∈ Ioo (-ε) ε}
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
⊢ γ2 (asup - ε / 2) = γ (asup - ε / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹³ : TopologicalSpace H
E : Type u_3
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
H' : Type u_5
inst✝⁸ : TopologicalSpace H'
E' : Type u_6
inst✝⁷ : NormedAddCommGroup E'
inst✝⁶ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁵ : TopologicalSpace M'
inst✝⁴ : ChartedSpace H' M'
inst✝³ : IsManifold I 2 M
inst✝² : IsManifold I' 2 M'
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace E'
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffOn I I' 2 f s
hx₀ : x₀ ∈ s
ht : t ⊆ (extChartAt I' (f x₀)).source
hst : MapsTo f s t
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
A' : x₀ = ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)
h'f : MDiffAt[s] f x₀
this : (mfderiv[range ↑I] ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀)).inverse = mfderiv% ↑(extChartAt I x₀) x₀
V' : (x : E') → TangentSpace 𝓘(𝕜, E') x := mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) V (range ↑I')
hV' : V' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) V (range ↑I')
W' : (x : E') → TangentSpace 𝓘(𝕜, E') x := mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) W (range ↑I')
hW' : W' = mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) W (range ↑I')
F : E → E' := (↑(extChartAt I' (f x₀)) ∘ f) ∘ ↑(extChartAt I x₀).symm
hF : F = (↑(extChartAt I' (f x₀)) ∘ f) ∘ ↑(extChartAt I x₀).symm
hFx₀ : ↑(extChartAt I' (f x₀)) (f x₀) = F (↑(extChartAt I x₀) x₀)
P :
  ∀ (Y : (x : M') → TangentSpace I' x),
    mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x₀).symm) (mpullbackWithin I I' f Y s)
        (range ↑I) =ᶠ[𝓝[↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x₀) x₀]
      mpullbackWithin 𝓘(𝕜, E) 𝓘(𝕜, E') F (mpullbackWithin 𝓘(𝕜, E') I' (↑(extChartAt I' (f x₀)).symm) Y (range ↑I'))
        (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I)
⊢ (f ∘ ↑(extChartAt I x₀).symm) (↑(extChartAt I x₀) x₀) ∈ (chartAt H' (f x₀)).source

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
smooth_pM : ContMDiffAt (I.tangent.prod I'.tangent) I.tangent n Prod.fst (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p.1.proj ∈ (chartAt H a.proj).source ∧ p.2.proj ∈ (chartAt H' b.proj).source
φ : E → E := fun x ↦ ↑I (↑(chartAt H a.proj) (↑(chartAt H p.1.proj).symm (↑I.symm x)))
D0 : DifferentiableWithinAt 𝕜 φ (range ↑I) (↑I (↑(chartAt H p.1.proj) p.1.proj))
D :
  ∀ (w : TangentBundle I' M'),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.fst) (range (Prod.map ↑I ↑I'))
      (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' w.proj) w.proj))
φ' : E' → E' := fun x ↦ ↑I' (↑(chartAt H' b.proj) (↑(chartAt H' p.2.proj).symm (↑I'.symm x)))
⊢ DifferentiableWithinAt 𝕜 φ' (range ↑I') (↑I' (↑(chartAt H' p.2.proj) p.2.proj))

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
smooth_pM : ContMDiffAt (I.tangent.prod I'.tangent) I.tangent n Prod.fst (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p.1.proj ∈ (chartAt H a.proj).source ∧ p.2.proj ∈ (chartAt H' b.proj).source
φ : E → E := fun x ↦ ↑I (↑(chartAt H a.proj) (↑(chartAt H p.1.proj).symm (↑I.symm x)))
D0 : DifferentiableWithinAt 𝕜 φ (range ↑I) (↑I (↑(chartAt H p.1.proj) p.1.proj))
D :
  ∀ (w : TangentBundle I' M'),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.fst) (range (Prod.map ↑I ↑I'))
      (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' w.proj) w.proj))
φ' : E' → E' := fun x ↦ ↑I' (↑(chartAt H' b.proj) (↑(chartAt H' p.2.proj).symm (↑I'.symm x)))
D0' : DifferentiableWithinAt 𝕜 φ' (range ↑I') (↑I' (↑(chartAt H' p.2.proj) p.2.proj))
⊢ DifferentiableWithinAt 𝕜 φ' (range ↑I') (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj)).2

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
smooth_pM : ContMDiffAt (I.tangent.prod I'.tangent) I.tangent n Prod.fst (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p.1.proj ∈ (chartAt H a.proj).source ∧ p.2.proj ∈ (chartAt H' b.proj).source
φ : E → E := fun x ↦ ↑I (↑(chartAt H a.proj) (↑(chartAt H p.1.proj).symm (↑I.symm x)))
D0 : DifferentiableWithinAt 𝕜 φ (range ↑I) (↑I (↑(chartAt H p.1.proj) p.1.proj))
D :
  ∀ (w : TangentBundle I' M'),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.fst) (range (Prod.map ↑I ↑I'))
      (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' w.proj) w.proj))
φ' : E' → E' := fun x ↦ ↑I' (↑(chartAt H' b.proj) (↑(chartAt H' p.2.proj).symm (↑I'.symm x)))
D0' : DifferentiableWithinAt 𝕜 φ' (range ↑I') (↑I' (↑(chartAt H' p.2.proj) p.2.proj))
⊢ MapsTo Prod.snd (range (Prod.map ↑I ↑I')) (range ↑I')

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : 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 ↦
    (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x))
      (v (↑(extChartAt I (γ t₀)).symm x))
hv' :
  v' = fun x ↦
    (tangentCoordChange I (↑(extChartAt I (γ t₀)).symm x) (γ t₀) (↑(extChartAt I (γ t₀)).symm x))
      (v (↑(extChartAt I (γ t₀)).symm x))
left✝ : ContinuousAt (fun x ↦ ⟨x, v x⟩) (γ t₀)
hv :
  ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent ⟨γ t₀, v (γ t₀)⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I (γ t₀)).symm)
    (range ↑I) (↑(extChartAt I (γ t₀)) (γ t₀))
K : NNReal
s : Set E
hs : s ∈ 𝓝 (↑(extChartAt I (γ t₀)) (γ t₀))
hlip✝ : LipschitzOnWith K v' s
hlip : ∀ (t : ℝ), LipschitzOnWith K ((fun x ↦ v') t) ((fun x ↦ s) t)
hsrc : ∀ {g : ℝ → M}, IsMIntegralCurveAt g v t₀ → ∀ᶠ (t : ℝ) in 𝓝 t₀, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t
hmem : ∀ {g : ℝ → M} {t : ℝ}, g ⁻¹' (extChartAt I (g t₀)).source ∈ 𝓝 t → g t ∈ (extChartAt I (g t₀)).source
hdrv :
  ∀ {g : ℝ → M},
    IsMIntegralCurveAt g v t₀ →
      γ t₀ = g t₀ →
        ∀ᶠ (t : ℝ) in 𝓝 t₀,
          HasDerivAt (↑(extChartAt I (g t₀)) ∘ g) ((fun x ↦ v') t ((↑(extChartAt I (g t₀)) ∘ g) t)) t ∧
            (↑(extChartAt I (g t₀)) ∘ g) t ∈ (fun x ↦ s) t
heq : ∀ {g : ℝ → M}, IsMIntegralCurveAt g v t₀ → g =ᶠ[𝓝 t₀] ↑(extChartAt I (g t₀)).symm ∘ ↑(extChartAt I (g t₀)) ∘ g
⊢ (↑(extChartAt I (γ t₀)) ∘ γ) t₀ = (↑(extChartAt I (γ' t₀)) ∘ γ') t₀

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type u_2
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
hγt₀ : I.IsInteriorPoint (γ t₀)
hv : ContMDiffAt I I.tangent 1 (fun x ↦ ⟨x, v x⟩) (γ t₀)
hγ : IsMIntegralCurveAt γ v t₀
hγ' : IsMIntegralCurveAt γ' v t₀
h : γ t₀ = γ' t₀
⊢ γ =ᶠ[𝓝 t₀] γ'

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
⊢ -(asup + ε / 2) < 0

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
⊢ 0 < a

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range ↑I ×ˢ range ↑I') (↑I w, ↑I' w')
smooth_pM : ContMDiffAt (I.tangent.prod I'.tangent) I.tangent n Prod.fst (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p.1.proj ∈ (chartAt H a.proj).source ∧ p.2.proj ∈ (chartAt H' b.proj).source
φ : E → E := fun x ↦ ↑I (↑(chartAt H a.proj) (↑(chartAt H p.1.proj).symm (↑I.symm x)))
D0 : DifferentiableWithinAt 𝕜 φ (range ↑I) (↑I (↑(chartAt H p.1.proj) p.1.proj))
D :
  ∀ (w : TangentBundle I' M'),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.fst) (range (Prod.map ↑I ↑I'))
      (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' w.proj) w.proj))
⊢ DifferentiableWithinAt 𝕜 φ (range ↑I) (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj)).1

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
⊢ -a < 0

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
⊢ γ_ext 0 = x

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p.1.proj ∈ (chartAt H a.proj).source ∧ p.2.proj ∈ (chartAt H' b.proj).source
φ : E' → E' := fun x ↦ ↑I' (↑(chartAt H' b.proj) (↑(chartAt H' p.2.proj).symm (↑I'.symm x)))
⊢ DifferentiableWithinAt 𝕜 φ (range ↑I') (↑I' (↑(chartAt H' p.2.proj) p.2.proj))

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
v : (x : M) → TangentSpace I x
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
ε : ℝ
hε : 0 < ε
h : ∀ (x : M), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-ε) ε)
x : M
s : Set ℝ := {a | ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)}
hbdd : BddAbove s
asup : ℝ := sSup s
hasup : asup = sSup s
a : ℝ
hlt : asup - ε / 2 < a
γ : ℝ → M
h0 : γ 0 = x
hγ : IsMIntegralCurveOn γ v (Ioo (-a) a)
γ1_aux : ℝ → M
h1_aux : γ1_aux 0 = γ (-(asup - ε / 2))
γ1 : ℝ → M := γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
γ1_def : γ1 = γ1_aux ∘ fun x ↦ x + (asup - ε / 2)
heq1 : γ1 (-(asup - ε / 2)) = γ (-(asup - ε / 2))
γ2_aux : ℝ → M
h2_aux : γ2_aux 0 = γ (asup - ε / 2)
γ2 : ℝ → M := γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
γ2_def : γ2 = γ2_aux ∘ fun x ↦ x - (asup - ε / 2)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
hγ1 : IsMIntegralCurveOn γ1 v {t | t ∈ Ioo (-ε - (asup - ε / 2)) (ε - (asup - ε / 2))}
hγ2 : IsMIntegralCurveOn γ2 v {t | t ∈ Ioo (-ε + (asup - ε / 2)) (ε + (asup - ε / 2))}
hεle : ε ≤ asup
γ_ext : ℝ → M := (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
γ_ext_def : γ_ext = (Ioo (-(asup + ε / 2)) a).piecewise ((Ioo (-a) a).piecewise γ γ1) γ2
heq_ext : γ_ext 0 = x
⊢ -(asup + ε / 2) < asup - ε / 2

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I 1 M
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : T2Space M
a b : ℝ
ht₀ : t₀ ∈ Ioo a b
hγt : ∀ t ∈ Ioo a b, I.IsInteriorPoint (γ t)
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a b)
h : γ t₀ = γ' t₀
⊢ EqOn γ γ' (Ioo a b)

Tactic:
by

Goal state after: