awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
hg : MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) ((η : (a : ℝ) → E) t)
hf : MDiffAt[Icc 0 1] (⇑η : (a : ℝ) → E) 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))
have h : Subset (α := Set ℝ) (Icc 0 1) ((⇑η : (a : ℝ) → E) ⁻¹' range (↑I : H → E))
Tactic: apply mfderivWithin_comp
-- 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
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
hg : MDiffAt[range (↑I : H → E)] (↑(extChartAt I x).symm : E → M) ((η : (a : ℝ) → E) t)
hf : MDiffAt[Icc 0 1] (⇑η : (a : ℝ) → E) t
h : Subset (α := Set ℝ) (Icc 0 1) ((⇑η : (a : ℝ) → E) ⁻¹' range (↑I : H → E))
⊢ 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))
have hxs : UniqueMDiffWithinAt 𝓘(ℝ, ℝ) (Icc 0 1) t
Tactic: apply mfderivWithin_comp
-- 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
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
⊢ UniqueMDiffWithinAt 𝓘(ℝ, ℝ) (Icc 0 1) t
have hxs : UniqueDiffWithinAt ℝ (Icc 0 1) t
Tactic: rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
-- 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
x : M
c : ℝ≥0∞
hc : 0 < c
⊢ ∀ᶠ (y : M) in 𝓝 x, riemannianEDist I x y < c
have 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
Tactic: rcases eventually_riemannianEDist_le_edist_extChartAt I x with ⟨C, C_pos, hC⟩
-- 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
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
have apply : eball ((↑(extChartAt I x) : M → E) x) (c / (↑C : ℝ≥0∞)) ∈ 𝓝 ((↑(extChartAt I x) : M → E) x)
Tactic: apply (continuousAt_extChartAt x).preimage_mem_nhds
-- 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
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)
⊢ ∀ᶠ (y : M) in 𝓝 x, riemannianEDist I x y < c
have this : (↑(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))
-- 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
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) in 𝓝 x, riemannianEDist I x y < c
have 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
Tactic: filter_upwards [this, hC] with y hy h'y
-- 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
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)
⊢ riemannianEDist I x y < c
have h : (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) < c
Tactic: apply h'y.trans_lt
-- 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
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)
⊢ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) < c
have this₁ : 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
-- 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
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∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) < c
have h : (↑C : ℝ≥0∞) ≠ 0 ∨ edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) ≠ ∞
Tactic: rwa [ENNReal.lt_div_iff_mul_lt, mul_comm] at this
-- 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
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) ≠ ∞
⊢ (↑C : ℝ≥0∞) * edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) < c
have h₁ : (↑C : ℝ≥0∞) ≠ ∞ ∨ edist ((↑(extChartAt I x) : M → E) x) ((↑(extChartAt I x) : M → E) y) ≠ 0
Tactic: rwa [ENNReal.lt_div_iff_mul_lt, mul_comm] at this
-- 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, {y : M | riemannianEDist I x y < (↑c : ℝ≥0∞)} ⊆ s
have rcases : ∀ (C : ℝ≥0) (C_pos : C > 0)
  (hC :
    ∀ᶠ (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∞)),
  ∃ c > 0, {y : M | riemannianEDist I x y < (↑c : ℝ≥0∞)} ⊆ s
Tactic: rcases eventually_enorm_mfderiv_extChartAt_lt I x with ⟨C, C_pos, hC⟩
-- 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 :
  ∀ᶠ (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 ∈ 𝓝 x,
    IsClosed[inst_3] u ∧
      u ⊆ s ∧
        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∞)} ∧
          u ⊆ (extChartAt I x).source
have this : s ∩
      {x_1 : M |
        (fun (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∞))
          x_1} ∩
    (extChartAt I x).source ∈
  𝓝 x
Tactic: have := Filter.inter_mem (Filter.inter_mem hs hC) (extChartAt_source_mem_nhds (I := I) x)
-- 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 :
  ∀ᶠ (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∞)
this :
  s ∩
        {x_1 : M |
          (fun (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∞))
            x_1} ∩
      (extChartAt I x).source ∈
    𝓝 x
⊢ ∃ u ∈ 𝓝 x,
    IsClosed[inst_3] u ∧
      u ⊆ s ∧
        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∞)} ∧
          u ⊆ (extChartAt I x).source
have rcases : ∀ (u : Set M) (u_mem : u ∈ 𝓝 x) (u_closed : IsClosed[inst_3] u)
  (hu :
    u ⊆
      s ∩
          {x_1 : M |
            (fun (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∞))
              x_1} ∩
        (extChartAt I x).source),
  ∃ u ∈ 𝓝 x,
    IsClosed[inst_3] u ∧
      u ⊆ s ∧
        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∞)} ∧
          u ⊆ (extChartAt I x).source
Tactic: rcases exists_mem_nhds_isClosed_subset this with ⟨u, u_mem, u_closed, hu⟩
-- 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 :
  ∀ᶠ (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∞)
this :
  s ∩
        {x_1 : M |
          (fun (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∞))
            x_1} ∩
      (extChartAt I x).source ∈
    𝓝 x
u : Set M
u_mem : u ∈ 𝓝 x
u_closed : IsClosed[inst_3] u
hu :
  u ⊆
    s ∩
        {x_1 : M |
          (fun (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∞))
            x_1} ∩
      (extChartAt I x).source
⊢ ∃ u ∈ 𝓝 x,
    IsClosed[inst_3] u ∧
      u ⊆ s ∧
        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∞)} ∧
          u ⊆ (extChartAt I x).source
have hu₁ : (u ⊆ s ∧
    u ⊆
      {x_1 : M |
        enorm (E := TangentSpace I x_1 →L[ℝ] TangentSpace 𝓘(ℝ, E) ((↑(extChartAt I x) : M → E) x_1))
            (mfderiv% (↑(extChartAt I x) : M → E) x_1) <
          (↑C : ℝ≥0∞)}) ∧
  u ⊆ (extChartAt I x).source
Tactic: simp only [subset_inter_iff] at hu
Cleared hypotheses: hu