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
x : M
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      (↑C : ℝ≥0∞)
r : ℝ
r_pos : r > 0
hr :
  ball ((↑(extChartAt I x) : M → E) x) r ∩ range (↑I : H → E) ⊆
    (extChartAt I x).target ∩
      {y : E |
        enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
            (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
          (↑C : ℝ≥0∞)}
A : (↑(extChartAt I x) : M → E) ⁻¹' (ball ((↑(extChartAt I x) : M → E) x) r ∩ range (↑I : H → E)) ∈ 𝓝 x
y : M
hy : y ∈ (↑(extChartAt I x) : M → E) ⁻¹' (ball ((↑(extChartAt I x) : M → E) x) r ∩ range (↑I : H → E))
h'y : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
η : ℝ →ᴬ[ℝ] E := ContinuousAffineMap.lineMap ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
γ : ℝ → M := (↑(extChartAt I x).symm : E → M) ∘ (⇑η : (a : ℝ) → E)
hη :
  Subset (α := Set ℝ) (Icc 0 1) ((⇑η : (a : ℝ) → E) ⁻¹' (extChartAt I x).target) ∧
    Subset (α := Set ℝ) (Icc 0 1)
      (preimage (β := E) (⇑η : (a : ℝ) → E)
        {y : E |
          enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
              (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
            (↑C : ℝ≥0∞)})
η_smooth : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) 𝓘(ℝ, E) (M' := E) 1 (⇑η : (a : ℝ) → E) (Icc 0 1)
this : riemannianEDist I x y ≤ pathELength I γ 0 1
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ Subset (α := Set ℝ) (Icc 0 1) ((⇑η : (a : ℝ) → E) ⁻¹' range (↑I : H → E))

Tactic:
exact hη.1.trans (preimage_mono (extChartAt_target_subset_range x))

Premises used: HasSubset.Subset.trans, extChartAt_target_subset_range, Set.preimage_mono, And.left
-- 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
x : M
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      (↑C : ℝ≥0∞)
r : ℝ
r_pos : r > 0
hr :
  ball ((↑(extChartAt I x) : M → E) x) r ∩ range (↑I : H → E) ⊆
    (extChartAt I x).target ∩
      {y : E |
        enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
            (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
          (↑C : ℝ≥0∞)}
A : (↑(extChartAt I x) : M → E) ⁻¹' (ball ((↑(extChartAt I x) : M → E) x) r ∩ range (↑I : H → E)) ∈ 𝓝 x
y : M
hy : y ∈ (↑(extChartAt I x) : M → E) ⁻¹' (ball ((↑(extChartAt I x) : M → E) x) r ∩ range (↑I : H → E))
h'y : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
η : ℝ →ᴬ[ℝ] E := ContinuousAffineMap.lineMap ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
γ : ℝ → M := (↑(extChartAt I x).symm : E → M) ∘ (⇑η : (a : ℝ) → E)
hη :
  Subset (α := Set ℝ) (Icc 0 1) ((⇑η : (a : ℝ) → E) ⁻¹' (extChartAt I x).target) ∧
    Subset (α := Set ℝ) (Icc 0 1)
      (preimage (β := E) (⇑η : (a : ℝ) → E)
        {y : E |
          enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
              (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
            (↑C : ℝ≥0∞)})
η_smooth : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) 𝓘(ℝ, E) (M' := E) 1 (⇑η : (a : ℝ) → E) (Icc 0 1)
this : riemannianEDist I x y ≤ pathELength I γ 0 1
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
hxs : UniqueDiffWithinAt ℝ (Icc 0 1) t
⊢ UniqueMDiffWithinAt 𝓘(ℝ, ℝ) (Icc 0 1) t

Tactic:
rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]

Premises used: uniqueMDiffWithinAt_iff_uniqueDiffWithinAt
-- 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
x : M
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      (↑C : ℝ≥0∞)
r : ℝ
r_pos : r > 0
hr :
  ball ((↑(extChartAt I x) : M → E) x) r ∩ range (↑I : H → E) ⊆
    (extChartAt I x).target ∩
      {y : E |
        enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
            (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
          (↑C : ℝ≥0∞)}
A : (↑(extChartAt I x) : M → E) ⁻¹' (ball ((↑(extChartAt I x) : M → E) x) r ∩ range (↑I : H → E)) ∈ 𝓝 x
y : M
hy : y ∈ (↑(extChartAt I x) : M → E) ⁻¹' (ball ((↑(extChartAt I x) : M → E) x) r ∩ range (↑I : H → E))
h'y : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
η : ℝ →ᴬ[ℝ] E := ContinuousAffineMap.lineMap ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
γ : ℝ → M := (↑(extChartAt I x).symm : E → M) ∘ (⇑η : (a : ℝ) → E)
hη :
  Subset (α := Set ℝ) (Icc 0 1) ((⇑η : (a : ℝ) → E) ⁻¹' (extChartAt I x).target) ∧
    Subset (α := Set ℝ) (Icc 0 1)
      (preimage (β := E) (⇑η : (a : ℝ) → E)
        {y : E |
          enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
              (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
            (↑C : ℝ≥0∞)})
η_smooth : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) 𝓘(ℝ, E) (M' := E) 1 (⇑η : (a : ℝ) → E) (Icc 0 1)
this : riemannianEDist I x y ≤ pathELength I γ 0 1
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ UniqueDiffWithinAt ℝ (Icc 0 1) t

Tactic:
uniqueDiffOn_Icc zero_lt_one t ht

Premises used: uniqueDiffOn_Icc, zero_lt_one
-- 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
x : M
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      (↑C : ℝ≥0∞)
r : ℝ
r_pos : r > 0
hr :
  ball ((↑(extChartAt I x) : M → E) x) r ∩ range (↑I : H → E) ⊆
    (extChartAt I x).target ∩
      {y : E |
        enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
            (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
          (↑C : ℝ≥0∞)}
A : (↑(extChartAt I x) : M → E) ⁻¹' (ball ((↑(extChartAt I x) : M → E) x) r ∩ range (↑I : H → E)) ∈ 𝓝 x
y : M
hy : y ∈ (↑(extChartAt I x) : M → E) ⁻¹' (ball ((↑(extChartAt I x) : M → E) x) r ∩ range (↑I : H → E))
h'y : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
η : ℝ →ᴬ[ℝ] E := ContinuousAffineMap.lineMap ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
γ : ℝ → M := (↑(extChartAt I x).symm : E → M) ∘ (⇑η : (a : ℝ) → E)
hη :
  Subset (α := Set ℝ) (Icc 0 1) ((⇑η : (a : ℝ) → E) ⁻¹' (extChartAt I x).target) ∧
    Subset (α := Set ℝ) (Icc 0 1)
      (preimage (β := E) (⇑η : (a : ℝ) → E)
        {y : E |
          enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
              (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
            (↑C : ℝ≥0∞)})
η_smooth : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) 𝓘(ℝ, E) (M' := E) 1 (⇑η : (a : ℝ) → E) (Icc 0 1)
this : riemannianEDist I x y ≤ pathELength I γ 0 1
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ UniqueDiffWithinAt ℝ (Icc 0 1) t

Tactic:
exact uniqueDiffOn_Icc zero_lt_one t ht

Premises used: uniqueDiffOn_Icc, zero_lt_one
-- 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
x : M
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : E) in 𝓝[range (↑I : H → E)] (↑(extChartAt I x) : M → E) x,
    enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
        (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
      (↑C : ℝ≥0∞)
r : ℝ
r_pos : r > 0
hr :
  ball ((↑(extChartAt I x) : M → E) x) r ∩ range (↑I : H → E) ⊆
    (extChartAt I x).target ∩
      {y : E |
        enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
            (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
          (↑C : ℝ≥0∞)}
A : (↑(extChartAt I x) : M → E) ⁻¹' (ball ((↑(extChartAt I x) : M → E) x) r ∩ range (↑I : H → E)) ∈ 𝓝 x
y : M
hy : y ∈ (↑(extChartAt I x) : M → E) ⁻¹' (ball ((↑(extChartAt I x) : M → E) x) r ∩ range (↑I : H → E))
h'y : y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
η : ℝ →ᴬ[ℝ] E := ContinuousAffineMap.lineMap ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
γ : ℝ → M := (↑(extChartAt I x).symm : E → M) ∘ (⇑η : (a : ℝ) → E)
hη :
  Subset (α := Set ℝ) (Icc 0 1) ((⇑η : (a : ℝ) → E) ⁻¹' (extChartAt I x).target) ∧
    Subset (α := Set ℝ) (Icc 0 1)
      (preimage (β := E) (⇑η : (a : ℝ) → E)
        {y : E |
          enorm (E := TangentSpace 𝓘(ℝ, E) y →L[ℝ] TangentSpace I ((↑(extChartAt I x).symm : E → M) y))
              (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) y) <
            (↑C : ℝ≥0∞)})
η_smooth : ContMDiffOn 𝓘(ℝ, ℝ) (M := ℝ) 𝓘(ℝ, E) (M' := E) 1 (⇑η : (a : ℝ) → E) (Icc 0 1)
this : riemannianEDist I x y ≤ pathELength I γ 0 1
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Icc 0 1) t
⊢ Eq (α := TangentSpace 𝓘(ℝ, ℝ) t →L[ℝ] TangentSpace I (γ t)) (mfderivWithin 𝓘(ℝ, ℝ) I γ (Icc 0 1) t)
    (ContinuousLinearMap.comp (M₂ := TangentSpace 𝓘(ℝ, E) (M := E) ((η : (a : ℝ) → E) t : E))
      (mfderivWithin 𝓘(ℝ, E) I (↑(extChartAt I x).symm : E → M) (range (↑I : H → E)) ((η : (a : ℝ) → E) t))
      (mfderivWithin 𝓘(ℝ, ℝ) 𝓘(ℝ, E) (⇑η : (a : ℝ) → E) (Icc 0 1) t))

Tactic:
have : mfderiv[Icc 0 1] γ t =
      (mfderiv[range I] (extChartAt I x).symm (η t)) ∘L (mfderiv[Icc 0 1] η t) := by
    apply mfderivWithin_comp
    · exact mdifferentiableWithinAt_extChartAt_symm (hη.1 ht)
    · exact η_smooth.mdifferentiableOn one_ne_zero t ht
    · exact hη.1.trans (preimage_mono (extChartAt_target_subset_range x))
    · rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
      exact uniqueDiffOn_Icc zero_lt_one t 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
x : M
c : ℝ≥0∞
hc : 0 < c
rcases :
  ∀ (C : ℝ≥0) (C_pos : C > 0)
    (hC :
      ∀ᶠ (y : M) in 𝓝 x,
        riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)),
    ∀ᶠ (y : M) in 𝓝 x, riemannianEDist I x y < c
⊢ ∀ᶠ (y : M) in 𝓝 x, riemannianEDist I x y < c

Tactic:
rcases eventually_riemannianEDist_le_edist_extChartAt I x with ⟨C, C_pos, hC⟩

Premises used: eventually_riemannianEDist_le_edist_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
x : M
c : ℝ≥0∞
hc : 0 < c
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
apply : eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞)) ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
⊢ (↑(extChartAt I x) : M → E) ⁻¹' eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞)) ∈ 𝓝 x

Tactic:
apply (continuousAt_extChartAt x).preimage_mem_nhds

Premises used: continuousAt_extChartAt, ContinuousAt.preimage_mem_nhds
-- 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
x : M
c : ℝ≥0∞
hc : 0 < c
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
⊢ (↑C : ℝ≥0∞) ≠ ∞

Tactic:
simp
-- 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
x : M
c : ℝ≥0∞
hc : 0 < c
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
⊢ eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞)) ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)

Tactic:
exact Metric.eball_mem_nhds _ (ENNReal.div_pos hc.ne' (by simp))

Premises used: LT.lt.ne', Metric.eball_mem_nhds, ENNReal.div_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
x : M
c : ℝ≥0∞
hc : 0 < c
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
⊢ (↑(extChartAt I x) : M → E) ⁻¹' eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞)) ∈ 𝓝 x

Tactic:
have : (extChartAt I x) ⁻¹' (Metric.eball (extChartAt I x x) (c / C)) ∈ 𝓝 x := by
    apply (continuousAt_extChartAt x).preimage_mem_nhds
    exact Metric.eball_mem_nhds _ (ENNReal.div_pos hc.ne' (by simp))
-- 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
x : M
c : ℝ≥0∞
hc : 0 < c
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
this : (↑(extChartAt I x) : M → E) ⁻¹' eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞)) ∈ 𝓝 x
h :
  ∀ (y : M) (hy : y ∈ (↑(extChartAt I x) : M → E) ⁻¹' eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞)))
    (h'y : riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)),
    riemannianEDist I x y < c
⊢ ∀ᶠ (y : M) in 𝓝 x, riemannianEDist I x y < c

Tactic:
filter_upwards [this, hC] with y hy h'y
-- 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
x : M
c : ℝ≥0∞
hc : 0 < c
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
this : (↑(extChartAt I x) : M → E) ⁻¹' eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞)) ∈ 𝓝 x
y : M
hy : y ∈ (↑(extChartAt I x) : M → E) ⁻¹' eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞))
h'y : riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
h : (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) < c
⊢ riemannianEDist I x y < c

Tactic:
apply h'y.trans_lt

Premises used: LE.le.trans_lt
-- 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
x : M
c : ℝ≥0∞
hc : 0 < c
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
this : (↑(extChartAt I x) : M → E) ⁻¹' eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞)) ∈ 𝓝 x
y : M
hy : y ∈ (↑(extChartAt I x) : M → E) ⁻¹' eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞))
h'y : riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
⊢ edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) < c / (↑C : ℝ≥0∞)

Tactic:
simpa only [mem_preimage, Metric.mem_eball'] using hy

Premises used: Metric.mem_eball', Set.mem_preimage
-- 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
x : M
c : ℝ≥0∞
hc : 0 < c
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
this : (↑(extChartAt I x) : M → E) ⁻¹' eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞)) ∈ 𝓝 x
y : M
hy : y ∈ (↑(extChartAt I x) : M → E) ⁻¹' eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞))
h'y : riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
⊢ edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) < c / (↑C : ℝ≥0∞)

Tactic:
have : edist (extChartAt I x x) (extChartAt I x y) < c / C := by
    simpa only [mem_preimage, Metric.mem_eball'] using hy
-- 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
x : M
c : ℝ≥0∞
hc : 0 < c
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
this_1 : (↑(extChartAt I x) : M → E) ⁻¹' eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞)) ∈ 𝓝 x
y : M
hy : y ∈ (↑(extChartAt I x) : M → E) ⁻¹' eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞))
h'y : riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
this : edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) < c / (↑C : ℝ≥0∞)
h : (↑C : ℝ≥0∞) ≠ 0 ∨ edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) ≠ ∞
h₁ : (↑C : ℝ≥0∞) ≠ ∞ ∨ edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) ≠ 0
⊢ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) < c

Tactic:
rwa [ENNReal.lt_div_iff_mul_lt, mul_comm] at this

Premises used: mul_comm, ENNReal.lt_div_iff_mul_lt
-- 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
x : M
c : ℝ≥0∞
hc : 0 < c
C : ℝ≥0
C_pos : C > 0
hC :
  ∀ᶠ (y : M) in 𝓝 x,
    riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
this_1 : (↑(extChartAt I x) : M → E) ⁻¹' eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞)) ∈ 𝓝 x
y : M
hy : y ∈ (↑(extChartAt I x) : M → E) ⁻¹' eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞))
h'y : riemannianEDist I x y ≤ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y)
this : edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) < c / (↑C : ℝ≥0∞)
⊢ (↑C : ℝ≥0∞) ≠ 0 ∨ edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) ≠ ∞

Tactic:
Or.inl (mod_cast C_pos.ne')

Premises used: ENNReal.ofNNReal, congrArg, cast, Ne, LT.lt.ne', Or.inl, ENNReal.coe_inj._simp_1, Nat.cast_zero, Eq.symm, Eq, Not, Eq.trans