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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m 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'
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
t : Set N
u : Set M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g t x₀
hx₀ : x₀ ∈ t
hu : MapsTo g t u
hmn : m + 1 ≤ n
h'u : UniqueMDiff[u]
t' : Set N := t ∩ g ⁻¹' (extChartAt I (g x₀)).source
ht't : t' ⊆ t
hx₀gx₀ : (x₀, g x₀) ∈ t ×ˢ u
h4f✝ : ContinuousWithinAt (fun x ↦ f x (g x)) t x₀
h4f : (fun x ↦ f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source ∈ 𝓝[t] x₀
h3f : ∀ᶠ (x' : N × M) in 𝓝[t ×ˢ u] (x₀, g x₀), ContMDiffWithinAt (J.prod I) I' 1 (uncurry f) (t ×ˢ u) x'
h2f : ∀ᶠ (x₂ : N) in 𝓝[t] x₀, ContMDiffWithinAt I I' 1 (f x₂) u (g x₂)
h2g : g ⁻¹' (extChartAt I (g x₀)).source ∈ 𝓝[t] x₀
this✝ :
  ContDiffWithinAt 𝕜 m
    (fun x ↦
      fderivWithin 𝕜 (↑(extChartAt I' (f x₀ (g x₀))) ∘ f (↑(extChartAt J x₀).symm x) ∘ ↑(extChartAt I (g x₀)).symm)
        ((extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u)
        (↑(extChartAt I (g x₀)) (g (↑(extChartAt J x₀).symm x))))
    (↑(extChartAt J x₀).symm ⁻¹' t' ∩ range ↑J) (↑(extChartAt J x₀) x₀)
this :
  ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (fun x ↦
      fderivWithin 𝕜 (↑(extChartAt I' (f x₀ (g x₀))) ∘ f x ∘ ↑(extChartAt I (g x₀)).symm)
        ((extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u) (↑(extChartAt I (g x₀)) (g x)))
    t' x₀
x : N
hx : ContMDiffWithinAt I I' 1 (f x) u (g x)
h'x : x ∈ (fun x ↦ f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source
h2 : x ∈ g ⁻¹' (extChartAt I (g x₀)).source
hxt : x ∈ t
h1 : g x ∈ u
h3 : UniqueMDiffAt[(extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u] (↑(extChartAt I (g x₀)) (g x))
A :
  mfderiv[range ↑I] ↑(extChartAt I (g x₀)).symm (↑(extChartAt I (g x₀)) (g x)) =
    mfderiv[(extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u] ↑(extChartAt I (g x₀)).symm
      (↑(extChartAt I (g x₀)) (g x))
⊢ mfderiv[(extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u]
        (↑(extChartAt I' (f x₀ (g x₀))) ∘ f x ∘ ↑(extChartAt I (g x₀)).symm)
      (↑(extChartAt I (g x₀)) (g x)) =
    fderivWithin 𝕜 (↑(extChartAt I' (f x₀ (g x₀))) ∘ f x ∘ ↑(extChartAt I (g x₀)).symm)
      ((extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u) (↑(extChartAt I (g x₀)) (g x))

Tactic:
exact mfderivWithin_eq_fderivWithin

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
⊢ IsImmersionAtOfComplement Unit (𝓡∂ 1) 𝓘(ℝ, ℝ) n (fun z ↦ ↑z) z

Tactic:
let φ₀ := ContinuousLinearEquiv.prodUnique ℝ (EuclideanSpace ℝ (Fin 1)) Unit

Goal state after:
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) :=
  ContinuousLinearEquiv.prodUnique ℝ (EuclideanSpace ℝ (Fin 1)) Unit
⊢ IsImmersionAtOfComplement Unit (𝓡∂ 1) 𝓘(ℝ, ℝ) n (fun z ↦ ↑z) z
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: case hφ
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) := ⋯
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := ⋯
hz : ↑z < y
⊢ ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, ℝ) n (↑(Homeomorph.addLeft (-x)).toOpenPartialHomeomorph)
    (Homeomorph.addLeft (-x)).toOpenPartialHomeomorph.source

Tactic:
have : ContDiff ℝ n (fun y ↦ -x + y) := by fun_prop
        simpa [contMDiffOn_iff_contDiffOn, contDiffOn_univ]

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Icc

Goal state before:
pp: case neg
x y : ℝ
h : Fact (x < y)
n : WithTop ℕ∞
z : ↑(Icc x y)
φ₀ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] EuclideanSpace ℝ (Fin 1) :=
  ContinuousLinearEquiv.prodUnique ℝ (EuclideanSpace ℝ (Fin 1)) Unit
φ : (EuclideanSpace ℝ (Fin 1) × Unit) ≃L[ℝ] ℝ := φ₀.trans (PiLp.equivOfUnique 2 ℝ fun x ↦ ℝ)
hz : ¬↑z < y
⊢ IsImmersionAtOfComplement Unit (𝓡∂ 1) 𝓘(ℝ, ℝ) n (fun z ↦ ↑z) z

Tactic:
· -- At the right boundary point, the correct codomain chart is mapping `a` to `y - a`.
    apply IsImmersionAtOfComplement.mk_of_continuousAt (by fun_prop) φ
      (chartAt (EuclideanHalfSpace 1) z)
      (Homeomorph.pointReflection (y / 2)).toOpenPartialHomeomorph (mem_chart_source _ z)
      (by simp [Homeomorph.pointReflection]) (chart_mem_maximalAtlas _) ?_; swap
    · apply OpenPartialHomeomorph.mem_maximalAtlas_of_contMDiffOn
      · have : ContDiff ℝ n ((fun v ↦ v + y / 2) ∘ fun x ↦ y / 2 - x) := by fun_prop
        simpa [contMDiffOn_iff_contDiffOn, contDiffOn_univ]
      · have : ContDiff ℝ n ((fun v ↦ -v + y / 2) ∘ fun p' ↦ p' - y / 2) := by fun_prop
        simpa [contMDiffOn_iff_contDiffOn, contDiffOn_univ]
    intro z' hz'
    obtain ⟨⟨u, rfl⟩, hu⟩ :
        (∃ y, ⇑(𝓡∂ 1) y = z') ∧ ⇑(𝓡∂ 1).symm z' ∈ (IccRightChart x y).target := by
      simpa [hz] using! hz'
    replace hu : ofLp u.val 0 ≤ y - x := by
      apply le_of_lt
      simpa [modelWithCornersEuclideanHalfSpace_symm_apply, max_eq_left u.property] using! hu
    simp [hz, φ, φ₀, modelWithCornersEuclideanHalfSpace_symm_apply, u.property,
      IccRightChart_symm_apply_of_le hu, Equiv.pointReflection_apply]
    linarith

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

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
t₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsMIntegralCurveOn γ v s
t : ℝ
ht : t ∈ s
hsrc : γ t ∈ (chartAt H (γ t₀)).source
a : TangentSpace 𝓘(ℝ, ℝ) t
⊢ (ContinuousLinearMap.smulRight 1 ((mfderiv% ↑(chartAt H (γ t₀)) (γ t)) (v (γ t)))) (1 a) =
    (ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) (1 a)

Tactic:
mfderiv_chartAt_eq_tangentCoordChange hsrc

Goal state after:
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
t₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsMIntegralCurveOn γ v s
t : ℝ
ht : t ∈ s
hsrc : γ t ∈ (chartAt H (γ t₀)).source
a : TangentSpace 𝓘(ℝ, ℝ) t
⊢ (ContinuousLinearMap.smulRight 1 ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) (1 a) =
    (ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) (1 a)
Module: Mathlib.Geometry.Manifold.IntegralCurve.Basic

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsMIntegralCurveAt γ v t₀
t : ℝ
ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t
ht2 : HasMFDerivAt% γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))
hsrc : γ t ∈ (chartAt H (γ t₀)).source
a : TangentSpace 𝓘(ℝ, ℝ) t
⊢ (ContinuousLinearMap.smulRight 1 ((mfderiv% ↑(chartAt H (γ t₀)) (γ t)) (v (γ t)))) (1 a) =
    (ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) (1 a)

Tactic:
mfderiv_chartAt_eq_tangentCoordChange hsrc

Goal state after:
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ : ℝ
inst✝ : IsManifold I 1 M
hγ : IsMIntegralCurveAt γ v t₀
t : ℝ
ht1 : γ ⁻¹' (extChartAt I (γ t₀)).source ∈ 𝓝 t
ht2 : HasMFDerivAt% γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))
hsrc : γ t ∈ (chartAt H (γ t₀)).source
a : TangentSpace 𝓘(ℝ, ℝ) t
⊢ (ContinuousLinearMap.smulRight 1 ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) (1 a) =
    (ContinuousLinearMap.toSpanSingleton ℝ ((tangentCoordChange I (γ t) (γ t₀) (γ t)) (v (γ t)))) (1 a)
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
hv' : v ∈ sphere 0 1
⊢ Set.range ↑(stereographic hv).symm = {⟨v, hv'⟩}ᶜ

Tactic:
refine le_antisymm ?_ (stereographic hv).symm.target_subset_range

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
hv : ‖v‖ = 1
hv' : v ∈ sphere 0 1
⊢ Set.range ↑(stereographic hv).symm ⊆ {⟨v, hv'⟩}ᶜ
Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform

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
v : (x : M) → TangentSpace I x
x : M
h : v x = 0
t : ℝ
⊢ HasMFDerivAt% (fun x_1 ↦ x) t (smulRight 1 0)

Tactic:
smulRight_one_eq_toSpanSingleton,

Goal state after:
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
v : (x : M) → TangentSpace I x
x : M
h : v x = 0
t : ℝ
⊢ HasMFDerivAt% (fun x_1 ↦ x) t (toSpanSingleton ℝ 0)
Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform

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
v : (x : M) → TangentSpace I x
x : M
h : v x = 0
⊢ IsMIntegralCurve (fun x_1 ↦ x) v

Tactic:
intro t
  rw [h, smulRight_one_eq_toSpanSingleton, toSpanSingleton_zero]
  exact hasMFDerivAt_const ..

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
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
t : ℝ
ht : t ∈ Ioo (-(|t| + 1)) (|t| + 1)
⊢ HasMFDerivAt% (fun t ↦ γ (|t| + 1) t) t (ContinuousLinearMap.smulRight 1 (v ((fun t ↦ γ (|t| + 1) t) t)))

Tactic:
apply HasMFDerivAt.congr_of_eventuallyEq (f := γ (|t| + 1))

Goal state after:
case h
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
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
t : ℝ
ht : t ∈ Ioo (-(|t| + 1)) (|t| + 1)
⊢ HasMFDerivAt% (γ (|t| + 1)) t (ContinuousLinearMap.smulRight 1 (v ((fun t ↦ γ (|t| + 1) t) t)))

case h₁
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
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
x : M
γ : ℝ → ℝ → M
hγx : ∀ (a : ℝ), γ a 0 = x
hγ : ∀ a > 0, IsMIntegralCurveOn (γ a) v (Ioo (-a) a)
t : ℝ
ht : t ∈ Ioo (-(|t| + 1)) (|t| + 1)
⊢ (fun t ↦ γ (|t| + 1) t) =ᶠ[𝓝 t] γ (|t| + 1)
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

Goal state before:
pp: case neg
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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a b ∪ Ioo a' b'
hmem : t ∉ Ioo a b
ht' : t ∈ Ioo a b ∪ Ioo a' b'
⊢ HasMFDerivAt[Ioo a b ∪ Ioo a' b'] ((Ioo a b).piecewise γ γ') t
    (ContinuousLinearMap.smulRight 1 (v ((Ioo a b).piecewise γ γ' t)))

Tactic:
mem_union,

Goal state after:
case neg
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
γ γ' : ℝ → M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
a b a' b' : ℝ
hγ : IsMIntegralCurveOn γ v (Ioo a b)
hγ' : IsMIntegralCurveOn γ' v (Ioo a' b')
t₀ : ℝ
ht₀ : t₀ ∈ Ioo a b ∩ Ioo a' b'
h : γ t₀ = γ' t₀
t : ℝ
ht : t ∈ Ioo a b ∨ t ∈ Ioo a' b'
hmem : t ∉ Ioo a b
ht' : t ∈ Ioo a b ∪ Ioo a' b'
⊢ HasMFDerivAt[Ioo a b ∪ Ioo a' b'] ((Ioo a b).piecewise γ γ') t
    (ContinuousLinearMap.smulRight 1 (v ((Ioo a b).piecewise γ γ' t)))
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)
⊢ False

Tactic:
have heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2) := by simp [γ2_def, h2_aux]

Goal state after:
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)
heq2 : γ2 (asup - ε / 2) = γ (asup - ε / 2)
⊢ False
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₀
s : Set ℝ := ⋯
hs : s = {t | γ t = γ' t} ∩ Ioo a b
val✝ : ℝ
ht : val✝ ∈ Ioo a b
⊢ ContinuousAt γ ↑⟨val✝, ht⟩

Tactic:
rw [Subtype.coe_mk]

Goal state after:
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₀
s : Set ℝ := {t | γ t = γ' t} ∩ Ioo a b
hs : s = {t | γ t = γ' t} ∩ Ioo a b
val✝ : ℝ
ht : val✝ ∈ Ioo a b
⊢ ContinuousAt γ val✝
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₀
s : Set ℝ := ⋯
hs : s = {t | γ t = γ' t} ∩ Ioo a b
val✝ : ℝ
ht : val✝ ∈ Ioo a b
⊢ ContinuousAt γ' ↑⟨val✝, ht⟩

Tactic:
rw [Subtype.coe_mk]

Goal state after:
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₀
s : Set ℝ := {t | γ t = γ' t} ∩ Ioo a b
hs : s = {t | γ t = γ' t} ∩ Ioo a b
val✝ : ℝ
ht : val✝ ∈ Ioo a b
⊢ ContinuousAt γ' val✝
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

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✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ ⇑η) (Icc 0 1)
f : ↑unitInterval → M := fun t ↦ (γ ∘ ⇑η) ↑t
hf : ContMDiff (𝓡∂ 1) I 1 f
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
⊢ riemannianEDist I x y ≤ pathELength I γ a b

Tactic:
have A : riemannianEDist I x y ≤ ∫⁻ x, ‖mfderiv% g x 1‖ₑ := by
    rw [riemannianEDist]; exact biInf_le _ hf

Goal state after:
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✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ ⇑η) (Icc 0 1)
f : ↑unitInterval → M := fun t ↦ (γ ∘ ⇑η) ↑t
hf : ContMDiff (𝓡∂ 1) I 1 f
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A : riemannianEDist I x y ≤ ∫⁻ (x_1 : ↑unitInterval), ‖(mfderiv% ⇑g x_1) 1‖ₑ
⊢ riemannianEDist I x y ≤ pathELength I γ a b
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: case hst
𝕜 : 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 (minSmoothness 𝕜 2) M
inst✝¹ : IsManifold I' (minSmoothness 𝕜 2) M'
inst✝ : CompleteSpace E
n : ℕ∞ω
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s u : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hs : UniqueMDiff[s]
hu : UniqueMDiff[u]
hf : ContMDiffWithinAt I I' n f u x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
h'x₀ : x₀ ∈ closure[inst✝⁹] (interior u)
hsu : s ⊆ u
B :
  ContDiffWithinAt 𝕜 n (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (↑(extChartAt I x₀) x₀)
this✝ :
  ↑(extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target =ᶠ[𝓝 (↑(extChartAt I x₀) x₀)]
    ↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I
this :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target) (↑(extChartAt I x₀) x₀)
⊢ ↑(extChartAt I x₀).symm ⁻¹' u ∩ (extChartAt I x₀).target ∈
    𝓝[↑(extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target] ↑(extChartAt I x₀) x₀

Tactic:
apply mem_of_superset self_mem_nhdsWithin (inter_subset_inter_left _ (preimage_mono hsu))

Goal state after:
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

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✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C
r : ℝ
r_pos : r > 0
hr :
  ball (↑(extChartAt I x) x) r ∩ range ↑I ⊆
    (extChartAt I x).target ∩ {y | ‖mfderiv[range ↑I] ↑(extChartAt I x).symm y‖ₑ < ↑C}
⊢ range ↑I ∩ ball (↑(extChartAt I x) x) r ∈ 𝓝[range ↑I] ↑(extChartAt I x) x

Tactic:
exact inter_mem_nhdsWithin _ (ball_mem_nhds _ r_pos)

Goal state after: