awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (hypothesis)
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₁
⊢ 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'))
have this : 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: have : mfderiv[Icc 0 t₁] γ' t' =
          (mfderiv% (extChartAt I x) (γ t')) ∘L (mfderiv[Icc 0 t₁] γ t') := by
        apply mfderiv_comp_mfderivWithin
        · refine mdifferentiableAt_extChartAt (uc' ?_)
          apply t₁_mem ht'
        · exact (γ_smooth.mdifferentiable one_ne_zero).mdifferentiableOn _ ht'
        · rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
          exact uniqueDiffOn_Icc h't' _ ht'
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (hypothesis)
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₁
this :
  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'))
⊢ 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'))
have this₁ : Eq (α := TangentSpace 𝓘(ℝ, E) (γ' t'))
  ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, E) γ' (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace 𝓘(ℝ, E) (γ' t')) 1 :
    TangentSpace 𝓘(ℝ, E) (γ' t'))
  ((mfderiv% (↑(extChartAt I x) : M → E) (γ t') :
        (a : TangentSpace I (γ t')) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) (γ t')))
      ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace I (γ t')) 1) :
    TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) (γ t')))
Tactic: have : mfderiv[Icc 0 t₁] γ' t' 1 =
          (mfderiv% (extChartAt I x) (γ t')) (mfderiv[Icc 0 t₁] γ t' 1) :=
        congr($this 1)
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (goal)
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₁
this_1 :
  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'))
this :
  Eq (α := TangentSpace 𝓘(ℝ, E) (γ' t'))
    ((mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, E) γ' (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace 𝓘(ℝ, E) (γ' t')) 1 :
      TangentSpace 𝓘(ℝ, E) (γ' t'))
    ((mfderiv% (↑(extChartAt I x) : M → E) (γ t') :
          (a : TangentSpace I (γ t')) → TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) (γ t')))
        ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace I (γ t')) 1) :
      TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) (γ t')))
⊢ enorm (E := TangentSpace I (γ t') →L[ℝ] TangentSpace 𝓘(ℝ, E) (γ' t')) (mfderiv% (↑(extChartAt I x) : M → E) (γ t')) ≤
    (↑C : ℝ≥0∞)
have bc : γ t' ∈ u
Tactic: refine (hu ?_).le
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (goal)
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₁,
      (↑C : ℝ≥0∞) *
        enorm (E := TangentSpace I (γ t'))
          ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 t₁) t' : (a : TangentSpace 𝓘(ℝ, ℝ) t') → TangentSpace I (γ t')) 1 :
            TangentSpace I (γ t')) =
    (↑C : ℝ≥0∞) * pathELength I γ 0 t₁
have rw : (↑C : ℝ≥0∞) *
    ∫⁻ (a : ℝ) in Icc 0 t₁,
      enorm (E := TangentSpace I (γ a))
        ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 t₁) a : (a_1 : TangentSpace 𝓘(ℝ, ℝ) a) → TangentSpace I (γ a)) 1 :
          TangentSpace I (γ a)) =
  (↑C : ℝ≥0∞) * pathELength I γ 0 t₁
Tactic: rw [lintegral_const_mul' _ _ ENNReal.coe_ne_top,
          pathELength_eq_lintegral_mfderivWithin_Icc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (goal)
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₁
rw :
  (↑C : ℝ≥0∞) *
      ∫⁻ (a : ℝ) in Icc 0 t₁,
        enorm (E := TangentSpace I (γ a))
          ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 t₁) a : (a_1 : TangentSpace 𝓘(ℝ, ℝ) a) → TangentSpace I (γ a)) 1 :
            TangentSpace I (γ a)) =
    (↑C : ℝ≥0∞) * pathELength I γ 0 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')) =
    (↑C : ℝ≥0∞) * pathELength I γ 0 t₁
have rw₁ : (↑C : ℝ≥0∞) *
    ∫⁻ (a : ℝ) in Icc 0 t₁,
      enorm (E := TangentSpace I (γ a))
        ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 t₁) a : (a_1 : TangentSpace 𝓘(ℝ, ℝ) a) → TangentSpace I (γ a)) 1 :
          TangentSpace I (γ a)) =
  (↑C : ℝ≥0∞) *
    ∫⁻ (t : ℝ) in Icc 0 t₁,
      enorm (E := TangentSpace I (γ t))
        ((mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 t₁) t : (a : TangentSpace 𝓘(ℝ, ℝ) t) → TangentSpace I (γ t)) 1 :
          TangentSpace I (γ t))
Tactic: rw [lintegral_const_mul' _ _ ENNReal.coe_ne_top,
          pathELength_eq_lintegral_mfderivWithin_Icc]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (goal)
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₁
⊢ (↑C : ℝ≥0∞) * pathELength I γ 0 1 < (↑C : ℝ≥0∞) * ((↑r : ℝ≥0∞) / (↑C : ℝ≥0∞))
have hinf : (↑C : ℝ≥0∞) ≠ ∞
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (goal)
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₁
hinf : (↑C : ℝ≥0∞) ≠ ∞
⊢ (↑C : ℝ≥0∞) * pathELength I γ 0 1 < (↑C : ℝ≥0∞) * ((↑r : ℝ≥0∞) / (↑C : ℝ≥0∞))
have bc : pathELength I γ 0 1 < (↑r : ℝ≥0∞) / (↑C : ℝ≥0∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (goal)
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₁)
this : ‖γ' t₁ - γ' 0‖ₑ < (↑r : ℝ≥0∞)
⊢ γ' t₁ ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' v
have a : γ' t₁ ∈ ball ((↑(extChartAt I x) : M → E) x) (↑r : ℝ)
Tactic: apply hr
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (goal)
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₁)
this : ‖γ' t₁ - γ' 0‖ₑ < (↑r : ℝ≥0∞)
⊢ γ' t₁ ∈ ball ((↑(extChartAt I x) : M → E) x) (↑r : ℝ)
have a : ‖γ' t₁ - (↑(extChartAt I x) : M → E) x‖ₑ < (↑r : ℝ≥0∞)
Tactic: rw [← Metric.eball_coe, Metric.mem_eball, edist_eq_enorm_sub]
-- Lean 4 proof step from Mathlib.Geometry.Manifold.Riemannian.Basic (goal)
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₁)
this : ‖γ' t₁ - γ' 0‖ₑ < (↑r : ℝ≥0∞)
⊢ ‖γ' t₁ - (↑(extChartAt I x) : M → E) x‖ₑ < (↑r : ℝ≥0∞)
have h : (↑(extChartAt I x) : M → E) x = γ' 0
Tactic: convert! this