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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ (↑(fderivWithin ℝ (writtenInExtChartAt (𝓡 n) 𝓘(ℝ, E) v Subtype.val) (Set.range ↑(𝓡 n))
          (↑(extChartAt (𝓡 n) v) v))).range =
    (ℝ ∙ ↑v)ᗮ

Tactic:
]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ (↑(fderivWithin ℝ (writtenInExtChartAt (𝓡 n) 𝓘(ℝ, E) v Subtype.val) (Set.range ↑(𝓡 n))
          (↑(extChartAt (𝓡 n) v) v))).range =
    (ℝ ∙ ↑v)ᗮ
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : (↑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0)).range = (ℝ ∙ ↑v)ᗮ
⊢ (↑(fderiv ℝ (Subtype.val ∘ ↑(ChartedSpace.chartAt v).symm) (↑(ChartedSpace.chartAt v) v))).range =
    (↑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0)).range

Tactic:
]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : (↑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0)).range = (ℝ ∙ ↑v)ᗮ
⊢ (↑(fderiv ℝ (Subtype.val ∘ ↑(ChartedSpace.chartAt v).symm) (↑(ChartedSpace.chartAt v) v))).range =
    (↑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0)).range
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 0

Tactic:
]

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 0
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
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) univ (x₀, g x₀)
hg : ContMDiffWithinAt J I m g univ x₀
hmn : m + 1 ≤ n
⊢ ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv% (f x) (g x)) x₀) univ x₀

Tactic:
]

Goal state after:
𝕜 : 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
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) univ (x₀, g x₀)
hg : ContMDiffWithinAt J I m g univ x₀
hmn : m + 1 ≤ n
⊢ ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv% (f x) (g x)) x₀) univ x₀
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
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst✝ : CompleteSpace E
hv :
  ContinuousAt (fun x ↦ ⟨x, v x⟩) x₀ ∧
    ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (range ↑I)
      (↑(extChartAt I x₀) x₀)
hx : I.IsInteriorPoint x₀
⊢ ∃ γ, γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀

Tactic:
]

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
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst✝ : CompleteSpace E
hv :
  ContinuousAt (fun x ↦ ⟨x, v x⟩) x₀ ∧
    ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (range ↑I)
      (↑(extChartAt I x₀) x₀)
hx : I.IsInteriorPoint x₀
⊢ ∃ γ, γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
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
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (univ ×ˢ univ) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g univ x₀
hmn : m + 1 ≤ n
⊢ ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv% (f x) (g x)) x₀) univ x₀

Tactic:
]

Goal state after:
𝕜 : 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
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (univ ×ˢ univ) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g univ x₀
hmn : m + 1 ≤ n
⊢ ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv% (f x) (g x)) x₀) univ x₀
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
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) univ (x₀, g x₀)
hg : ContMDiffWithinAt J I m g univ x₀
hmn : m + 1 ≤ n
⊢ ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv% (f x) (g x)) x₀) univ x₀

Tactic:
rw [← univ_prod_univ] at hf

Goal state after:
𝕜 : 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
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (univ ×ˢ univ) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g univ x₀
hmn : m + 1 ≤ n
⊢ ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (inTangentCoordinates I I' g (fun x ↦ f x (g x)) (fun x ↦ mfderiv% (f x) (g x)) x₀) univ x₀
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
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst✝ : CompleteSpace E
hx : I.IsInteriorPoint x₀
left✝ : ContinuousAt (fun x ↦ ⟨x, v x⟩) x₀
hv :
  ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (range ↑I)
    (↑(extChartAt I x₀) x₀)
f : ℝ → E
hf1 : f t₀ = ↑(extChartAt I x₀) x₀
hf2 :
  ∀ᶠ (y : ℝ) in 𝓝 t₀,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y
a : ℝ
ha : a > 0
hf2' :
  ∀ y ∈ Metric.ball t₀ a,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y
hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀
⊢ ∃ γ, γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀

Tactic:
]

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
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst✝ : CompleteSpace E
hx : I.IsInteriorPoint x₀
left✝ : ContinuousAt (fun x ↦ ⟨x, v x⟩) x₀
hv :
  ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (range ↑I)
    (↑(extChartAt I x₀) x₀)
f : ℝ → E
hf1 : f t₀ = ↑(extChartAt I x₀) x₀
hf2 :
  ∀ᶠ (y : ℝ) in 𝓝 t₀,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y
a : ℝ
ha : a > 0
hf2' :
  ∀ y ∈ Metric.ball t₀ a,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y
hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀
⊢ ∃ γ, γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: case e'_3.hs
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (ℝ ∙ ↑(-v))ᗮ.subtypeL (U.symm 0)
⊢ -↑v ∈ ℝ ∙ -↑v

Tactic:
]

Goal state after:
case e'_3.hs
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (ℝ ∙ ↑(-v))ᗮ.subtypeL (U.symm 0)
⊢ -↑v ∈ ℝ ∙ -↑v
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
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst✝ : CompleteSpace E
hx : I.IsInteriorPoint x₀
left✝ : ContinuousAt (fun x ↦ ⟨x, v x⟩) x₀
hv :
  ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (range ↑I)
    (↑(extChartAt I x₀) x₀)
f : ℝ → E
hf1 : f t₀ = ↑(extChartAt I x₀) x₀
hf2 :
  ∀ᶠ (y : ℝ) in 𝓝 t₀,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y
a : ℝ
ha : a > 0
hf2' :
  ∀ y ∈ Metric.ball t₀ a,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y
hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀
hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'
⊢ ∃ γ, γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀

Tactic:
]

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
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst✝ : CompleteSpace E
hx : I.IsInteriorPoint x₀
left✝ : ContinuousAt (fun x ↦ ⟨x, v x⟩) x₀
hv :
  ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (range ↑I)
    (↑(extChartAt I x₀) x₀)
f : ℝ → E
hf1 : f t₀ = ↑(extChartAt I x₀) x₀
hf2 :
  ∀ᶠ (y : ℝ) in 𝓝 t₀,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y
a : ℝ
ha : a > 0
hf2' :
  ∀ y ∈ Metric.ball t₀ a,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y
hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) x₀), f ⁻¹' A ∈ 𝓝 t₀
hnhds : ∀ᶠ (x' : ℝ) in 𝓝 t₀, f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 x'
⊢ ∃ γ, γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: case e'_3.ht
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (ℝ ∙ ↑(-v))ᗮ.subtypeL (U.symm 0)
⊢ ↑v ∈ ℝ ∙ ↑v

Tactic:
]

Goal state after:
case e'_3.ht
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (ℝ ∙ ↑(-v))ᗮ.subtypeL (U.symm 0)
⊢ ↑v ∈ ℝ ∙ ↑v
Module: Mathlib.Geometry.Manifold.Instances.Sphere

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ Injective
    ⇑(fderivWithin ℝ (writtenInExtChartAt (𝓡 n) 𝓘(ℝ, E) v Subtype.val) (Set.range ↑(𝓡 n)) (↑(extChartAt (𝓡 n) v) v))

Tactic:
]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
⊢ Injective
    ⇑(fderivWithin ℝ (writtenInExtChartAt (𝓡 n) 𝓘(ℝ, E) v Subtype.val) (Set.range ↑(𝓡 n)) (↑(extChartAt (𝓡 n) v) v))
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
v : (x : M) → TangentSpace I x
t₀ : ℝ
x₀ : M
inst✝ : CompleteSpace E
hx : I.IsInteriorPoint x₀
left✝ : ContinuousAt (fun x ↦ ⟨x, v x⟩) x₀
hv :
  ContDiffWithinAt ℝ 1 (↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (range ↑I)
    (↑(extChartAt I x₀) x₀)
f : ℝ → E
hf1 : f t₀ = ↑(extChartAt I x₀) x₀
hf2 :
  ∀ᶠ (y : ℝ) in 𝓝 t₀,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y
a : ℝ
ha : a > 0
hf2' :
  ∀ y ∈ Metric.ball t₀ a,
    HasDerivAt f ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y
hcont : ∀ A ∈ 𝓝 (↑(extChartAt I x₀) 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 ((↑(extChartAt I.tangent ⟨x₀, v x₀⟩) ∘ (fun x ↦ ⟨x, v x⟩) ∘ ↑(extChartAt I x₀).symm) (f y)).2 y ∧
      f ⁻¹' interior (extChartAt I x₀).target ∈ 𝓝 y
⊢ x₀ = x₀

Tactic:
]

Goal state after:
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 : M → M'
s : Set M
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiff[s]
x₀ : TangentBundle I M
hx₀ : x₀ ∈ TotalSpace.proj ⁻¹' s
s' : Set (TangentBundle I M) := TotalSpace.proj ⁻¹' s
b₁ : TangentBundle I M → M := fun p ↦ p.proj
v : (y : TangentBundle I M) → TangentSpace I (b₁ y) := fun y ↦ y.snd
hv : ContMDiffWithinAt I.tangent I.tangent m (fun y ↦ ⟨b₁ y, v y⟩) s' x₀
b₂ : TangentBundle I M → M' := f ∘ b₁
hb₂ : ContMDiffWithinAt I.tangent I' m b₂ s' x₀
ϕ : (y : TangentBundle I M) → TangentSpace I (b₁ y) →L[𝕜] TangentSpace I' (b₂ y) := fun y ↦ mfderiv[s] f (b₁ y)
hϕ :
  ContMDiffWithinAt I.tangent 𝓘(𝕜, E →L[𝕜] E') m
    (fun y ↦
      ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') (b₁ x₀) (b₁ y) (b₂ x₀) (b₂ y) (ϕ y))
    s' x₀
⊢ ContMDiffWithinAt I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s) x₀

Tactic:
exact ContMDiffWithinAt.clm_apply_of_inCoordinates hϕ hv hb₂

Goal state after:
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 : M → M'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f univ
hmn : m + 1 ≤ n
⊢ ContMDiffOn I.tangent I'.tangent m (tangentMap I I' f) univ

Tactic:
]

Goal state after:
𝕜 : 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 : M → M'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f univ
hmn : m + 1 ≤ n
⊢ ContMDiffOn I.tangent I'.tangent m (tangentMap I I' f) univ
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: case e'_22
𝕜 : 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 : M → M'
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
hf : ContMDiffOn I I' n f univ
hmn : m + 1 ≤ n
⊢ tangentMap I I' f = tangentMap I I' f

Tactic:
]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this✝ : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (ℝ ∙ ↑(-v))ᗮ.subtypeL (U.symm 0)
this : ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0) = ⇑((ℝ ∙ ↑(-v))ᗮ.subtypeL ∘SL ↑↑U.symm)
⊢ Injective (⇑(ℝ ∙ ↑(-v))ᗮ.subtypeL ∘ ⇑↑U.symm)

Tactic:
]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
this✝ : HasFDerivAt (stereoInvFunAux (-↑v) ∘ Subtype.val) (ℝ ∙ ↑(-v))ᗮ.subtypeL (U.symm 0)
this : ⇑(fderiv ℝ ((stereoInvFunAux (-↑v) ∘ Subtype.val) ∘ ⇑U.symm) 0) = ⇑((ℝ ∙ ↑(-v))ᗮ.subtypeL ∘SL ↑↑U.symm)
⊢ Injective (⇑(ℝ ∙ ↑(-v))ᗮ.subtypeL ∘ ⇑↑U.symm)