mathlib-initiative/mathlib-tactics huggingface dataset:
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}
A : ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I) ∈ 𝓝 x
y : M
⊢ y ∈ ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I) →
    y ∈ (chartAt H x).source → riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)

Tactic:
hy

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✝² : 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}
A : ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I) ∈ 𝓝 x
y : M
hy : y ∈ ↑(extChartAt I x) ⁻¹' (ball (↑(extChartAt I x) x) r ∩ range ↑I)
⊢ y ∈ (chartAt H x).source → riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
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 (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 : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
this : mpullback I I' f (mlieBracketWithin I' V W t) x₀ = mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀
y : M
⊢ ContMDiffAt I I' 2 f y → y ∈ s → mpullbackWithin I I' f V s y = mpullback I I' f V y

Tactic:
hy

Goal state after:
𝕜 : 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 : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
this : mpullback I I' f (mlieBracketWithin I' V W t) x₀ = mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀
y : M
hy : ContMDiffAt I I' 2 f y
⊢ y ∈ s → mpullbackWithin I I' f V s y = mpullback I I' f V y
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 (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 : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
this : mpullback I I' f (mlieBracketWithin I' V W t) x₀ = mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀
y : M
hy : ContMDiffAt I I' 2 f y
h'y : y ∈ s
⊢ mfderiv[s] f y = mfderiv% f y

Tactic:
apply mfderivWithin_eq_mfderiv (hu _ h'y)

Goal state after:
𝕜 : 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 : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
this : mpullback I I' f (mlieBracketWithin I' V W t) x₀ = mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀
y : M
hy : ContMDiffAt I I' 2 f y
h'y : y ∈ s
⊢ MDiffAt f y
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 (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 : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
this : mpullback I I' f (mlieBracketWithin I' V W t) x₀ = mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀
y : M
⊢ ContMDiffAt I I' 2 f y → y ∈ s → mpullbackWithin I I' f W s y = mpullback I I' f W y

Tactic:
hy

Goal state after:
𝕜 : 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 : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffAt I I' n f x₀
hx₀ : x₀ ∈ s
hn : minSmoothness 𝕜 2 ≤ n
hst : f ⁻¹' t ∈ 𝓝[s] x₀
this : mpullback I I' f (mlieBracketWithin I' V W t) x₀ = mpullbackWithin I I' f (mlieBracketWithin I' V W t) s x₀
y : M
hy : ContMDiffAt I I' 2 f y
⊢ y ∈ s → mpullbackWithin I I' f W s y = mpullback I I' f W y
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
inst✝² : IsManifold I (minSmoothness 𝕜 2) M
inst✝¹ : CompleteSpace E
n : ℕ∞ω
inst✝ : IsManifold I (n + 1) M
m : ℕ∞ω
U V : (x : M) → TangentSpace I x
s : Set M
x : M
hU : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, U x⟩) s x
hV : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, V x⟩) s x
hs : UniqueMDiff[s]
hx : x ∈ s
hmn : minSmoothness 𝕜 (m + 1) ≤ n
min2 : minSmoothness 𝕜 2 ≤ n + 1
m' : ℕ∞ω
hm' : m' ≤ m
h'm' : m' ≠ ∞
hn : 1 ≤ m' + 1
hm'n : m' + 1 ≤ n
y : M
⊢ y ∈ s →
    y ∈ (extChartAt I x).source → y ∈ ↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)

Tactic:
hy

Goal state after:
𝕜 : 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
inst✝² : IsManifold I (minSmoothness 𝕜 2) M
inst✝¹ : CompleteSpace E
n : ℕ∞ω
inst✝ : IsManifold I (n + 1) M
m : ℕ∞ω
U V : (x : M) → TangentSpace I x
s : Set M
x : M
hU : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, U x⟩) s x
hV : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, V x⟩) s x
hs : UniqueMDiff[s]
hx : x ∈ s
hmn : minSmoothness 𝕜 (m + 1) ≤ n
min2 : minSmoothness 𝕜 2 ≤ n + 1
m' : ℕ∞ω
hm' : m' ≤ m
h'm' : m' ≠ ∞
hn : 1 ≤ m' + 1
hm'n : m' + 1 ≤ n
y : M
hy : y ∈ s
⊢ y ∈ (extChartAt I x).source → y ∈ ↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)
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
inst✝² : IsManifold I (minSmoothness 𝕜 2) M
inst✝¹ : CompleteSpace E
n : ℕ∞ω
inst✝ : IsManifold I (n + 1) M
m : ℕ∞ω
U V : (x : M) → TangentSpace I x
s : Set M
x : M
hU : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, U x⟩) s x
hV : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, V x⟩) s x
hs : UniqueMDiff[s]
hx : x ∈ s
hmn : minSmoothness 𝕜 (m + 1) ≤ n
min2 : minSmoothness 𝕜 2 ≤ n + 1
m' : ℕ∞ω
hm' : m' ≤ m
h'm' : m' ≠ ∞
hn : 1 ≤ m' + 1
hm'n : m' + 1 ≤ n
pre_mem : ↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) ∈ 𝓝[s] x
U' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) U (range ↑I)
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)
⊢ ContMDiffWithinAt I I.tangent m' (fun x₀ ↦ ⟨x₀, mlieBracketWithin I U V s x₀⟩) s x

Tactic:
have A : ContDiffWithinAt 𝕜 m' (lieBracketWithin 𝕜 U' V'
      ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s))
      ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' s) (extChartAt I x x) :=
    ContDiffWithinAt.lieBracketWithin_vectorField
      (contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt.1
        (contMDiffWithinAt_mpullbackWithin_extChartAt_symm hU hs hx le_rfl))
      (contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt.1
        (contMDiffWithinAt_mpullbackWithin_extChartAt_symm hV hs hx le_rfl))
      (hs.uniqueDiffOn_target_inter x) hm'n (by simp [hx])

Goal state after:
𝕜 : 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
inst✝² : IsManifold I (minSmoothness 𝕜 2) M
inst✝¹ : CompleteSpace E
n : ℕ∞ω
inst✝ : IsManifold I (n + 1) M
m : ℕ∞ω
U V : (x : M) → TangentSpace I x
s : Set M
x : M
hU : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, U x⟩) s x
hV : ContMDiffWithinAt I I.tangent n (fun x ↦ ⟨x, V x⟩) s x
hs : UniqueMDiff[s]
hx : x ∈ s
hmn : minSmoothness 𝕜 (m + 1) ≤ n
min2 : minSmoothness 𝕜 2 ≤ n + 1
m' : ℕ∞ω
hm' : m' ≤ m
h'm' : m' ≠ ∞
hn : 1 ≤ m' + 1
hm'n : m' + 1 ≤ n
pre_mem : ↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) ∈ 𝓝[s] x
U' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) U (range ↑I)
V' : (x : E) → TangentSpace 𝓘(𝕜, E) x := mpullbackWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) V (range ↑I)
A :
  ContDiffWithinAt 𝕜 m' (lieBracketWithin 𝕜 U' V' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s))
    ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s) (↑(extChartAt I x) x)
⊢ ContMDiffWithinAt I I.tangent m' (fun x₀ ↦ ⟨x₀, mlieBracketWithin I U V s x₀⟩) s x
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
inst✝¹ : IsManifold I (minSmoothness 𝕜 3) M
inst✝ : CompleteSpace E
U V W : (x : M) → TangentSpace I x
s : Set M
x : M
hs : UniqueMDiff[s]
h's : x ∈ closure[inst✝³] (interior s)
hx : x ∈ s
hU : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, U x⟩) s x
hV : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, V x⟩) s x
hW : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, W x⟩) s x
A : minSmoothness 𝕜 2 + 1 ≤ minSmoothness 𝕜 3
s_inter_mem : s ∩ (extChartAt I x).source ∈ 𝓝[s] x
y : M
⊢ y ∈ s ∩ (extChartAt I x).source → y ∈ ↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)

Tactic:
hy

Goal state after:
𝕜 : 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
inst✝¹ : IsManifold I (minSmoothness 𝕜 3) M
inst✝ : CompleteSpace E
U V W : (x : M) → TangentSpace I x
s : Set M
x : M
hs : UniqueMDiff[s]
h's : x ∈ closure[inst✝³] (interior s)
hx : x ∈ s
hU : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, U x⟩) s x
hV : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, V x⟩) s x
hW : ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x ↦ ⟨x, W x⟩) s x
A : minSmoothness 𝕜 2 + 1 ≤ minSmoothness 𝕜 3
s_inter_mem : s ∩ (extChartAt I x).source ∈ 𝓝[s] x
y : M
hy : y ∈ s ∩ (extChartAt I x).source
⊢ y ∈ ↑(extChartAt I x) ⁻¹' ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)
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∞
hc : 0 < c
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
this : ↑(extChartAt I x) ⁻¹' eball (↑(extChartAt I x) x) (c / ↑C) ∈ 𝓝 x
y : M
⊢ y ∈ ↑(extChartAt I x) ⁻¹' eball (↑(extChartAt I x) x) (c / ↑C) →
    riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y) → riemannianEDist I x y < c

Tactic:
hy

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✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
c : ℝ≥0∞
hc : 0 < c
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
this : ↑(extChartAt I x) ⁻¹' eball (↑(extChartAt I x) x) (c / ↑C) ∈ 𝓝 x
y : M
hy : y ∈ ↑(extChartAt I x) ⁻¹' eball (↑(extChartAt I x) x) (c / ↑C)
⊢ riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y) → riemannianEDist I x y < c
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
inst✝ : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst✝⁵] u
us : u ⊆ s
hu : u ⊆ {y | ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (chartAt H x).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst✝⁵] v
r : ℝ≥0
hr : ball (↑(extChartAt I x) x) ↑r ⊆ ↑(extChartAt I x).symm ⁻¹' v
r_pos : 0 < r
y : M
⊢ y ∈ {y | riemannianEDist I x y < ↑(r / C)} → y ∈ s

Tactic:
hy

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✝³ : RiemannianBundle fun x ↦ TangentSpace I x
inst✝² : IsManifold I 1 M
inst✝¹ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
inst✝ : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst✝⁵] u
us : u ⊆ s
hu : u ⊆ {y | ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (chartAt H x).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst✝⁵] v
r : ℝ≥0
hr : ball (↑(extChartAt I x) x) ↑r ⊆ ↑(extChartAt I x).symm ⁻¹' v
r_pos : 0 < r
y : M
hy : y ∈ {y | riemannianEDist I x y < ↑(r / C)}
⊢ y ∈ s
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
hδ : (r' ^ 2)⁻¹ < 1 - δ * C
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
⊢ dist (g' y) (g' x) < δ →
    y ∈ (trivializationAt F E x).baseSet →
      ‖Trivialization.symmL ℝ (trivializationAt F E x) x ∘SL
            Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
        r

Tactic:
hy

Goal state after:
B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
hδ : (r' ^ 2)⁻¹ < 1 - δ * C
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
⊢ y ∈ (trivializationAt F E x).baseSet →
    ‖Trivialization.symmL ℝ (trivializationAt F E x) x ∘SL
          Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
      r
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
H : Type u_7
E : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
x : M
y : E
⊢ y ∈ ((chartAt H x).extend I).target →
    (↑((chartAt H x).extend I) ∘ id ∘ ↑((chartAt H x).extend I).symm) y =
      (Prod.fst ∘ ⇑(ContinuousLinearEquiv.prodUnique 𝕜 E PUnit.{u_15 + 1}).symm) y

Tactic:
hy

Goal state after:
𝕜 : Type u_1
H : Type u_7
E : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
x : M
y : E
hy : y ∈ ((chartAt H x).extend I).target
⊢ (↑((chartAt H x).extend I) ∘ id ∘ ↑((chartAt H x).extend I).symm) y =
    (Prod.fst ∘ ⇑(ContinuousLinearEquiv.prodUnique 𝕜 E PUnit.{u_15 + 1}).symm) y