mathlib-initiative/mathlib-tactics huggingface dataset:
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
x : M
V W : (x : M) → TangentSpace I x
c : 𝕜
inst✝¹ : IsManifold I 2 M
inst✝ : CompleteSpace E
hV : MDiffAt (T% V) x
⊢ mlieBracketWithin I (c • V) W univ x = c • mlieBracketWithin I V W univ x

Tactic:
exact mlieBracketWithin_const_smul_left hV (uniqueMDiffWithinAt_univ _)

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
F : Type u_5
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
inst✝¹² : NormedAddCommGroup E'''
inst✝¹¹ : NormedSpace 𝕜 E'''
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁸ : TopologicalSpace H
G : Type u_9
inst✝⁷ : TopologicalSpace G
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
N : Type u_13
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
x : M
f : M → N
φ : N → N'
h : IsImmersionAtOfComplement F J J' n φ (f x)
h' : ContMDiffAt I J' n (φ ∘ f) x
t : Set M
ht : t ⊆ f ⁻¹' h.domChart.source
hxt : x ∈ t
⊢ ContDiffWithinAt 𝕜 n (↑(h.domChart.extend J) ∘ f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I)
    (↑(extChartAt I x) x)

Tactic:
set f' := (h.domChart.extend J) ∘ f ∘ (extChartAt I x).symm

Goal state after:
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
F : Type u_5
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
inst✝¹² : NormedAddCommGroup E'''
inst✝¹¹ : NormedSpace 𝕜 E'''
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁸ : TopologicalSpace H
G : Type u_9
inst✝⁷ : TopologicalSpace G
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
N : Type u_13
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
x : M
f : M → N
φ : N → N'
h : IsImmersionAtOfComplement F J J' n φ (f x)
h' : ContMDiffAt I J' n (φ ∘ f) x
t : Set M
ht : t ⊆ f ⁻¹' h.domChart.source
hxt : x ∈ t
f' : E → E'' := ↑(h.domChart.extend J) ∘ f ∘ ↑(extChartAt I x).symm
⊢ ContDiffWithinAt 𝕜 n f' (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I) (↑(extChartAt I x) x)
Module: Mathlib.Geometry.Manifold.Immersion

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
F : Type u_5
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
inst✝¹² : NormedAddCommGroup E'''
inst✝¹¹ : NormedSpace 𝕜 E'''
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁸ : TopologicalSpace H
G : Type u_9
inst✝⁷ : TopologicalSpace G
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
N : Type u_13
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
x : M
f : M → N
φ : N → N'
h : IsImmersionAtOfComplement F J J' n φ (f x)
h' : ContMDiffAt I J' n (φ ∘ f) x
t : Set M
ht : t ⊆ f ⁻¹' h.domChart.source
hxt : x ∈ t
f' : E → E'' := ↑(h.domChart.extend J) ∘ f ∘ ↑(extChartAt I x).symm
φ' : E'' → E''' := ↑(h.codChart.extend J') ∘ φ ∘ ↑(h.domChart.extend J).symm
x' : E := ↑(extChartAt I x) x
s : Set E := ↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I
hx' : ↑(extChartAt I x) x ∈ s
h'loc :
  ContDiffWithinAt 𝕜 n (↑(h.codChart.extend J') ∘ (φ ∘ f) ∘ ↑(extChartAt I x).symm)
    (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I) (↑(extChartAt I x) x)
y : E
hy : y ∈ ↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I
⊢ ↑J' (↑h.codChart (φ (↑h.domChart.symm (↑h.domChart (f (↑(chartAt H x).symm (↑I.symm y))))))) =
    ↑J' (↑h.codChart (φ (f (↑(chartAt H x).symm (↑I.symm y)))))

Tactic:
rw [h.domChart.left_inv]

Goal state after:
𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
F : Type u_5
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
inst✝¹² : NormedAddCommGroup E'''
inst✝¹¹ : NormedSpace 𝕜 E'''
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁸ : TopologicalSpace H
G : Type u_9
inst✝⁷ : TopologicalSpace G
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
N : Type u_13
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
x : M
f : M → N
φ : N → N'
h : IsImmersionAtOfComplement F J J' n φ (f x)
h' : ContMDiffAt I J' n (φ ∘ f) x
t : Set M
ht : t ⊆ f ⁻¹' h.domChart.source
hxt : x ∈ t
f' : E → E'' := ↑(h.domChart.extend J) ∘ f ∘ ↑(extChartAt I x).symm
φ' : E'' → E''' := ↑(h.codChart.extend J') ∘ φ ∘ ↑(h.domChart.extend J).symm
x' : E := ↑(extChartAt I x) x
s : Set E := ↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I
hx' : ↑(extChartAt I x) x ∈ s
h'loc :
  ContDiffWithinAt 𝕜 n (↑(h.codChart.extend J') ∘ (φ ∘ f) ∘ ↑(extChartAt I x).symm)
    (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I) (↑(extChartAt I x) x)
y : E
hy : y ∈ ↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I
⊢ f (↑(chartAt H x).symm (↑I.symm y)) ∈ h.domChart.source
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
x : ↑(sphere 0 1)
hx : ↑x ≠ v
a : ℝ := ((innerSL ℝ) v) ↑x
y : ↥(ℝ ∙ v)ᗮ := (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x
split : ↑x = a • v + ↑y
hvy : ⟪v, ↑y⟫_ℝ = 0
pythag : 1 = a ^ 2 + ‖y‖ ^ 2
ha : 0 < 1 - a
⊢ ((|2| / (1 - a) * ‖y‖) ^ 2 + 4)⁻¹ * (((|2| / (1 - a) * ‖y‖) ^ 2 - 4) * 1) = a * 1

Tactic:
· field_simp
    linear_combination 4 * (a - 1) * pythag

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

Goal state before:
pp: E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
m : ℕ∞ω
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ F H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I m M
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
f : M → E
hf : ContMDiff I 𝓘(ℝ, E) m f
hf' : ∀ (x : M), f x ∈ sphere 0 1
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
h : ContDiffOn ℝ ω (⇑U) Set.univ
H₁ :
  ContMDiffOn 𝓘(ℝ, E) (𝓡 n) ω (⇑U ∘ stereoToFun ↑(-v))
    ({x | ((innerSL ℝ) ↑(-v)) x ≠ 1} ∩ stereoToFun ↑(-v) ⁻¹' Set.univ)
⊢ ContMDiffOn I (𝓡 n) m (↑(extChartAt (𝓡 n) v) ∘ Set.codRestrict f (sphere 0 1) hf')
    (Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt (𝓡 n) v).source)

Tactic:
have H₂ : CMDiff[Set.univ] m f := hf.contMDiffOn

Goal state after:
E : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
m : ℕ∞ω
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ F H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I m M
n : ℕ
inst✝ : Fact (finrank ℝ E = n + 1)
f : M → E
hf : ContMDiff I 𝓘(ℝ, E) m f
hf' : ∀ (x : M), f x ∈ sphere 0 1
v : ↑(sphere 0 1)
U : ↥(ℝ ∙ ↑(-v))ᗮ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n) := (OrthonormalBasis.fromOrthogonalSpanSingleton n ⋯).repr
h : ContDiffOn ℝ ω (⇑U) Set.univ
H₁ :
  ContMDiffOn 𝓘(ℝ, E) (𝓡 n) ω (⇑U ∘ stereoToFun ↑(-v))
    ({x | ((innerSL ℝ) ↑(-v)) x ≠ 1} ∩ stereoToFun ↑(-v) ⁻¹' Set.univ)
H₂ : ContMDiffOn I 𝓘(ℝ, E) m f Set.univ
⊢ ContMDiffOn I (𝓡 n) m (↑(extChartAt (𝓡 n) v) ∘ Set.codRestrict f (sphere 0 1) hf')
    (Set.codRestrict f (sphere 0 1) hf' ⁻¹' (extChartAt (𝓡 n) v).source)
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ a : ℝ
ha : a ≠ 0
ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
⊢ ε / |a| > 0

Tactic:
by positivity

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₀)
Y : (x : M') → TangentSpace I' x
this : (extChartAt I x₀).target ∈ 𝓝[↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x₀) x₀
y : E
hy : y ∈ ↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I
h'''y : y ∈ (extChartAt I x₀).target
h'y : f (↑(extChartAt I x₀).symm y) ∈ (extChartAt I' (f x₀)).source
h''y : f (↑(extChartAt I x₀).symm y) ∈ (chartAt H' (f x₀)).source
huy : UniqueMDiffAt[↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I] y
⊢ (mfderiv[range ↑I'] ↑(extChartAt I' (f x₀)).symm
      (↑(extChartAt I' (f x₀)) (f (↑(extChartAt I x₀).symm y)))).IsInvertible

Tactic:
exact isInvertible_mfderivWithin_extChartAt_symm (PartialEquiv.map_source _ h'y)

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)
a a' : ℝ
hpos : 0 < a'
hle : a' ≤ a
⊢ a' > 0

Tactic:
by positivity

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)
a a' : ℝ
hpos : 0 < a'
hle : a' ≤ a
⊢ 0 < a'

Tactic:
by positivity

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)
a t : ℝ
ht : t ∈ Ioo (-a) a
hlt : |t| + 1 < a
⊢ 0 < |t| + 1

Tactic:
by positivity

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)
⊢ |t| + 1 > 0

Tactic:
by positivity

Goal state after:
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)
a b : ℝ
γ : ℝ → M
⊢ pathELength I γ a b = ∫⁻ (t : ℝ) in Icc a b, ‖(mfderiv[Icc a b] γ t) 1‖ₑ

Tactic:
rw [pathELength_eq_lintegral_mfderiv_Icc, ← restrict_Ioo_eq_restrict_Icc]
  apply setLIntegral_congr_fun measurableSet_Ioo (fun t ht ↦ ?_)
  rw [mfderivWithin_of_mem_nhds]
  exact Icc_mem_nhds ht.1 ht.2

Goal state after:
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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := fun t ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ t < a', η t = 0
t : ℝ
ht : t < a'
⊢ (γ ∘ η) t = x

Tactic:
simp [A t ht, hγx]

Goal state after:
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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := fun t ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ t < a', η t = 0
⊢ ∃ γ,
    γ a = x ∧
      γ b = y ∧ ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun x_1 ↦ x) ∧ γ =ᶠ[𝓝 b] fun x ↦ y

Tactic:
have A' (t) (ht : t < a') : (γ ∘ η) t = x := by simp [A t ht, hγx]

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
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := fun t ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ t < a', η t = 0
A' : ∀ t < a', (γ ∘ η) t = x
⊢ ∃ γ,
    γ a = x ∧
      γ b = y ∧ ContMDiff 𝓘(ℝ, ℝ) I 1 γ ∧ pathELength I γ a b < r ∧ (γ =ᶠ[𝓝 a] fun x_1 ↦ x) ∧ γ =ᶠ[𝓝 b] fun x ↦ y
Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian

Goal state before:
pp: EB : Type u_1
inst✝¹¹ : NormedAddCommGroup EB
inst✝¹⁰ : NormedSpace ℝ EB
HB : Type u_2
inst✝⁹ : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst✝⁸ : TopologicalSpace B
inst✝⁷ : ChartedSpace HB B
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_5
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 : IsContMDiffRiemannianBundle IB n F E
h' : n' ≤ n
⊢ IsContMDiffRiemannianBundle IB n' F E

Tactic:
rcases h.exists_contMDiff with ⟨g, g_smooth, hg⟩

Goal state after:
EB : Type u_1
inst✝¹¹ : NormedAddCommGroup EB
inst✝¹⁰ : NormedSpace ℝ EB
HB : Type u_2
inst✝⁹ : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n n' : ℕ∞ω
B : Type u_3
inst✝⁸ : TopologicalSpace B
inst✝⁷ : ChartedSpace HB B
F : Type u_4
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_5
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 : IsContMDiffRiemannianBundle IB n F E
h' : n' ≤ n
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_smooth : ContMDiff IB (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) n fun b ↦ ⟨b, g b⟩
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
⊢ IsContMDiffRiemannianBundle IB n' F E
Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian

Goal state before:
pp: EB : Type u_1
inst✝¹⁶ : NormedAddCommGroup EB
inst✝¹⁵ : NormedSpace ℝ EB
HB : Type u_2
inst✝¹⁴ : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n : ℕ∞ω
B : Type u_3
inst✝¹³ : TopologicalSpace B
inst✝¹² : ChartedSpace HB B
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
E : B → Type u_5
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
EM : Type u_6
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace ℝ EM
HM : Type u_7
inst✝² : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB n F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ ⟨b m, v m⟩) s x
hw : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ ⟨b m, w m⟩) s x
⊢ ContMDiffWithinAt IM 𝓘(ℝ, ℝ) n (fun m ↦ ⟪v m, w m⟫) s x

Tactic:
rcases h.exists_contMDiff with ⟨g, g_smooth, hg⟩

Goal state after:
EB : Type u_1
inst✝¹⁶ : NormedAddCommGroup EB
inst✝¹⁵ : NormedSpace ℝ EB
HB : Type u_2
inst✝¹⁴ : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
n : ℕ∞ω
B : Type u_3
inst✝¹³ : TopologicalSpace B
inst✝¹² : ChartedSpace HB B
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
E : B → Type u_5
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
EM : Type u_6
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace ℝ EM
HM : Type u_7
inst✝² : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB n F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ ⟨b m, v m⟩) s x
hw : ContMDiffWithinAt IM (IB.prod 𝓘(ℝ, F)) n (fun m ↦ ⟨b m, w m⟩) s x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_smooth : ContMDiff IB (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) n fun b ↦ ⟨b, g b⟩
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
⊢ ContMDiffWithinAt IM 𝓘(ℝ, ℝ) n (fun m ↦ ⟪v m, w m⟫) s x
Module: Mathlib.Geometry.Manifold.VectorBundle.Riemannian

Goal state before:
pp: EB : Type u_1
inst✝¹⁶ : NormedAddCommGroup EB
inst✝¹⁵ : NormedSpace ℝ EB
HB : Type u_2
inst✝¹⁴ : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
B : Type u_3
inst✝¹³ : TopologicalSpace B
inst✝¹² : ChartedSpace HB B
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
E : B → Type u_5
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
EM : Type u_6
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace ℝ EM
HM : Type u_7
inst✝² : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB 1 F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : (MDiffAt[s] fun m ↦ ⟨b m, v m⟩) x
hw : (MDiffAt[s] fun m ↦ ⟨b m, w m⟩) x
⊢ (MDiffAt[s] fun m ↦ ⟪v m, w m⟫) x

Tactic:
rcases h.exists_contMDiff with ⟨g, g_smooth, hg⟩

Goal state after:
EB : Type u_1
inst✝¹⁶ : NormedAddCommGroup EB
inst✝¹⁵ : NormedSpace ℝ EB
HB : Type u_2
inst✝¹⁴ : TopologicalSpace HB
IB : ModelWithCorners ℝ EB HB
B : Type u_3
inst✝¹³ : TopologicalSpace B
inst✝¹² : ChartedSpace HB B
F : Type u_4
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
E : B → Type u_5
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
EM : Type u_6
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace ℝ EM
HM : Type u_7
inst✝² : TopologicalSpace HM
IM : ModelWithCorners ℝ EM HM
M : Type u_8
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
h : IsContMDiffRiemannianBundle IB 1 F E
b : M → B
v w : (x : M) → E (b x)
s : Set M
x : M
hv : (MDiffAt[s] fun m ↦ ⟨b m, v m⟩) x
hw : (MDiffAt[s] fun m ↦ ⟨b m, w m⟩) x
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_smooth : ContMDiff IB (IB.prod 𝓘(ℝ, F →L[ℝ] F →L[ℝ] ℝ)) 1 fun b ↦ ⟨b, g b⟩
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
⊢ (MDiffAt[s] fun m ↦ ⟪v m, w m⟫) x