awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC_1 :
  ∀ᶠ (y : M) in 𝓝 x,
    enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ≥0∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
r : ℝ≥0
hr : ball ((↑(extChartAt I x) : M → E) x) (↑r : ℝ) ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v
r_pos : 0 < r
y : M
hy : Membership.mem (γ := Set M) {y : M | riemannianEDist I x y < (↑(r / C) : ℝ≥0∞)} y
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < (↑(r / C) : ℝ≥0∞)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
γ' : ℝ → E := (↑(extChartAt I x) : M → E) ∘ γ
ht₁0 : LE.le (α := ℝ) 0 0
ht₁1 : LT.lt (α := ℝ) 0 1
t₁_mem : Icc 0 0 ⊆ A
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 0)
⊢ ‖γ' 0 - γ' 0‖ₑ < (↑r : ℝ≥0∞)

Tactic:
simp [r_pos]
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC_1 :
  ∀ᶠ (y : M) in 𝓝 x,
    enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ≥0∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
r : ℝ≥0
hr : ball ((↑(extChartAt I x) : M → E) x) (↑r : ℝ) ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v
r_pos : 0 < r
y : M
hy : Membership.mem (γ := Set M) {y : M | riemannianEDist I x y < (↑(r / C) : ℝ≥0∞)} y
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < (↑(r / C) : ℝ≥0∞)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := (↑(extChartAt I x) : M → E) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
apply : ContDiffOn ℝ 1 γ' (Icc 0 t₁)
⊢ ‖γ' t₁ - γ' 0‖ₑ ≤ ∫⁻ (t' : ℝ) in Icc 0 t₁, ‖derivWithin γ' (Icc 0 t₁) t'‖ₑ

Tactic:
apply enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc _ ht₁0

Premises used: enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC_1 :
  ∀ᶠ (y : M) in 𝓝 x,
    enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ≥0∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
r : ℝ≥0
hr : ball ((↑(extChartAt I x) : M → E) x) (↑r : ℝ) ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v
r_pos : 0 < r
y : M
hy : Membership.mem (γ := Set M) {y : M | riemannianEDist I x y < (↑(r / C) : ℝ≥0∞)} y
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < (↑(r / C) : ℝ≥0∞)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := (↑(extChartAt I x) : M → E) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
rwa rwa₁ rwa₂ rwa₃ : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
⊢ ContDiffOn ℝ 1 γ' (Icc 0 t₁)

Tactic:
rwa [← contMDiffOn_iff_contDiffOn]

Premises used: contMDiffOn_iff_contDiffOn
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC_1 :
  ∀ᶠ (y : M) in 𝓝 x,
    enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ≥0∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
r : ℝ≥0
hr : ball ((↑(extChartAt I x) : M → E) x) (↑r : ℝ) ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v
r_pos : 0 < r
y : M
hy : Membership.mem (γ := Set M) {y : M | riemannianEDist I x y < (↑(r / C) : ℝ≥0∞)} y
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < (↑(r / C) : ℝ≥0∞)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := (↑(extChartAt I x) : M → E) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
simp_rw :
  ∫⁻ (t' : ℝ) in Icc 0 t₁, enorm (E := E) ((fderivWithin ℝ γ' (Icc 0 t₁) t' : (a : ℝ) → E) 1 : E) =
    ∫⁻ (t' : ℝ) in Icc 0 t₁,
      enorm (E := TangentSpace 𝓘(ℝ, E) (γ' t'))
        ((fderivWithin ℝ γ' (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace 𝓘(ℝ, E) (γ' t')) 1 :
          TangentSpace 𝓘(ℝ, E) (γ' t'))
⊢ ∫⁻ (t' : ℝ) in Icc 0 t₁, ‖derivWithin γ' (Icc 0 t₁) t'‖ₑ =
    ∫⁻ (t' : ℝ) in Icc 0 t₁,
      enorm (E := TangentSpace 𝓘(ℝ, E) (γ' t'))
        ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, E) γ' (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace 𝓘(ℝ, E) (γ' t'))
            1 :
          TangentSpace 𝓘(ℝ, E) (γ' t'))

Tactic:
simp_rw [← fderivWithin_derivWithin, mfderivWithin_eq_fderivWithin]

Premises used: mfderivWithin_eq_fderivWithin, fderivWithin_derivWithin
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC_1 :
  ∀ᶠ (y : M) in 𝓝 x,
    enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ≥0∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
r : ℝ≥0
hr : ball ((↑(extChartAt I x) : M → E) x) (↑r : ℝ) ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v
r_pos : 0 < r
y : M
hy : Membership.mem (γ := Set M) {y : M | riemannianEDist I x y < (↑(r / C) : ℝ≥0∞)} y
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < (↑(r / C) : ℝ≥0∞)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := (↑(extChartAt I x) : M → E) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
⊢ ∫⁻ (t' : ℝ) in Icc 0 t₁, enorm (E := E) ((fderivWithin ℝ γ' (Icc 0 t₁) t' : (a : ℝ) → E) 1 : E) =
    ∫⁻ (t' : ℝ) in Icc 0 t₁,
      enorm (E := TangentSpace 𝓘(ℝ, E) (γ' t'))
        ((fderivWithin ℝ γ' (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace 𝓘(ℝ, E) (γ' t')) 1 :
          TangentSpace 𝓘(ℝ, E) (γ' t'))

Tactic:
rfl
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC_1 :
  ∀ᶠ (y : M) in 𝓝 x,
    enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ≥0∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
r : ℝ≥0
hr : ball ((↑(extChartAt I x) : M → E) x) (↑r : ℝ) ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v
r_pos : 0 < r
y : M
hy : Membership.mem (γ := Set M) {y : M | riemannianEDist I x y < (↑(r / C) : ℝ≥0∞)} y
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < (↑(r / C) : ℝ≥0∞)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := (↑(extChartAt I x) : M → E) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
apply :
  ∀ (t' : ℝ) (ht' : t' ∈ Icc 0 t₁),
    enorm (E := TangentSpace 𝓘(ℝ, E) (γ' t'))
        ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, E) γ' (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace 𝓘(ℝ, E) (γ' t'))
            1 :
          TangentSpace 𝓘(ℝ, E) (γ' t')) ≤
      (↑C : ℝ≥0∞) *
        enorm (E := TangentSpace I (γ t'))
          ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace I (γ t')) 1 :
            TangentSpace I (γ t'))
⊢ ∫⁻ (t' : ℝ) in Icc 0 t₁,
      enorm (E := TangentSpace 𝓘(ℝ, E) (γ' t'))
        ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, E) γ' (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace 𝓘(ℝ, E) (γ' t'))
            1 :
          TangentSpace 𝓘(ℝ, E) (γ' t')) ≤
    ∫⁻ (t' : ℝ) in Icc 0 t₁,
      (↑C : ℝ≥0∞) *
        enorm (E := TangentSpace I (γ t'))
          ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace I (γ t')) 1 :
            TangentSpace I (γ t'))

Tactic:
apply setLIntegral_mono' measurableSet_Icc (fun t' ht' ↦ ?_)

Premises used: measurableSet_Icc, MeasureTheory.setLIntegral_mono'
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC_1 :
  ∀ᶠ (y : M) in 𝓝 x,
    enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ≥0∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
r : ℝ≥0
hr : ball ((↑(extChartAt I x) : M → E) x) (↑r : ℝ) ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v
r_pos : 0 < r
y : M
hy : Membership.mem (γ := Set M) {y : M | riemannianEDist I x y < (↑(r / C) : ℝ≥0∞)} y
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < (↑(r / C) : ℝ≥0∞)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := (↑(extChartAt I x) : M → E) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
t' : ℝ
ht' : t' ∈ Icc 0 t₁
hg : MDiffAt (↑(extChartAt I x) : M → E) (γ t')
hf : MDiffAt[Icc 0 t₁] γ t'
hxs : UniqueMDiffWithinAt 𝓘(ℝ, ℝ) (Icc 0 t₁) t'
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) t' →L[ℝ] TangentSpace 𝓘(ℝ, E) (γ' t')) (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, E) γ' (Icc 0 t₁) t')
    (ContinuousLinearMap.comp (M₂ := TangentSpace I (γ t')) (mfderiv% (↑(extChartAt I x) : M → E) (γ t'))
      (mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 t₁) t'))

Tactic:
apply mfderiv_comp_mfderivWithin

Premises used: mfderiv_comp_mfderivWithin
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC_1 :
  ∀ᶠ (y : M) in 𝓝 x,
    enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ≥0∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
r : ℝ≥0
hr : ball ((↑(extChartAt I x) : M → E) x) (↑r : ℝ) ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v
r_pos : 0 < r
y : M
hy : Membership.mem (γ := Set M) {y : M | riemannianEDist I x y < (↑(r / C) : ℝ≥0∞)} y
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < (↑(r / C) : ℝ≥0∞)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := (↑(extChartAt I x) : M → E) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
t' : ℝ
ht' : t' ∈ Icc 0 t₁
⊢ MDiffAt (↑(extChartAt I x) : M → E) (γ t')

Tactic:
mdifferentiableAt_extChartAt (uc' ?_)

Premises used: mdifferentiableAt_extChartAt
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC_1 :
  ∀ᶠ (y : M) in 𝓝 x,
    enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ≥0∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
r : ℝ≥0
hr : ball ((↑(extChartAt I x) : M → E) x) (↑r : ℝ) ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v
r_pos : 0 < r
y : M
hy : Membership.mem (γ := Set M) {y : M | riemannianEDist I x y < (↑(r / C) : ℝ≥0∞)} y
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < (↑(r / C) : ℝ≥0∞)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := (↑(extChartAt I x) : M → E) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
t' : ℝ
ht' : t' ∈ Icc 0 t₁
hg : γ t' ∈ u
⊢ MDiffAt (↑(extChartAt I x) : M → E) (γ t')

Tactic:
refine mdifferentiableAt_extChartAt (uc' ?_)

Premises used: mdifferentiableAt_extChartAt
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC_1 :
  ∀ᶠ (y : M) in 𝓝 x,
    enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ≥0∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
r : ℝ≥0
hr : ball ((↑(extChartAt I x) : M → E) x) (↑r : ℝ) ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v
r_pos : 0 < r
y : M
hy : Membership.mem (γ := Set M) {y : M | riemannianEDist I x y < (↑(r / C) : ℝ≥0∞)} y
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < (↑(r / C) : ℝ≥0∞)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := (↑(extChartAt I x) : M → E) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
t' : ℝ
ht' : t' ∈ Icc 0 t₁
⊢ γ t' ∈ u

Tactic:
apply t₁_mem ht'
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC_1 :
  ∀ᶠ (y : M) in 𝓝 x,
    enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ≥0∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
r : ℝ≥0
hr : ball ((↑(extChartAt I x) : M → E) x) (↑r : ℝ) ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v
r_pos : 0 < r
y : M
hy : Membership.mem (γ := Set M) {y : M | riemannianEDist I x y < (↑(r / C) : ℝ≥0∞)} y
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < (↑(r / C) : ℝ≥0∞)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := (↑(extChartAt I x) : M → E) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
t' : ℝ
ht' : t' ∈ Icc 0 t₁
⊢ MDiffAt[Icc 0 t₁] γ t'

Tactic:
(γ_smooth.mdifferentiable one_ne_zero).mdifferentiableOn _ ht'

Premises used: ContMDiff.mdifferentiable, one_ne_zero, MDifferentiable.mdifferentiableOn
-- Module: Mathlib.Geometry.Manifold.Riemannian.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
H : Type u_2
inst_2 : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst_3 : TopologicalSpace M
inst_4 : ChartedSpace H M
inst_5 : RiemannianBundle.{u_3, u_1} fun (x : M) ↦ TangentSpace I x
inst_6 : IsManifold I 1 M
inst_7 : IsContinuousRiemannianBundle E fun (x : M) ↦ TangentSpace I x
inst_8 : RegularSpace M
x : M
s : Set M
hs : s ∈ 𝓝 x
C : ℝ≥0
C_pos : C > 0
hC_1 :
  ∀ᶠ (y : M) in 𝓝 x,
    enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
        (mfderiv% (↑(extChartAt I x) : M → E) y) <
      (↑C : ℝ≥0∞)
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
us : u ⊆ s
hu :
  u ⊆
    {y : M |
      enorm (E := TangentSpace I y →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) y))
          (mfderiv% (↑(extChartAt I x) : M → E) y) <
        (↑C : ℝ≥0∞)}
uc : u ⊆ (extChartAt I x).source
uc' : u ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
v : Set M
hv : v ⊆ u
v_mem : v ∈ 𝓝 x
v_open : IsOpen[inst_3] v
r : ℝ≥0
hr : ball ((↑(extChartAt I x) : M → E) x) (↑r : ℝ) ⊆ (↑(extChartAt I x).symm : E → M) ⁻¹' v
r_pos : 0 < r
y : M
hy : Membership.mem (γ := Set M) {y : M | riemannianEDist I x y < (↑(r / C) : ℝ≥0∞)} y
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < (↑(r / C) : ℝ≥0∞)
A : Set ℝ := γ ⁻¹' u
zero_mem : 0 ∈ A
A_closed : IsClosed (A ∩ Icc 0 1)
t₁ : ℝ
ht₁0 : 0 ≤ t₁
ht₁1 : t₁ < 1
t₁_mem : Icc 0 t₁ ⊆ A
γ' : ℝ → E := (↑(extChartAt I x) : M → E) ∘ γ
hC : ContMDiffOn 𝓘(ℝ, ℝ) 𝓘(ℝ, E) 1 γ' (Icc 0 t₁)
h't' : 0 < t₁
t' : ℝ
ht' : t' ∈ Icc 0 t₁
⊢ MDiffAt[Icc 0 t₁] γ t'

Tactic:
exact (γ_smooth.mdifferentiable one_ne_zero).mdifferentiableOn _ ht'

Premises used: ContMDiff.mdifferentiable, one_ne_zero, MDifferentiable.mdifferentiableOn