Module: Mathlib.Geometry.Manifold.Riemannian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ 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 * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
this✝ : ↑(extChartAt I x) ⁻¹' eball (↑(extChartAt I x) x) (c / ↑C) ∈ 𝓝 x
y : M
hy : y ∈ ↑(extChartAt I x) ⁻¹' eball (↑(extChartAt I x) x) (c / ↑C)
h'y : riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
this : edist (↑(extChartAt I x) x) (↑(extChartAt I x) y) < c / ↑C
⊢ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y) < c

Tactic:
ENNReal.lt_div_iff_mul_lt,

Goal state after:
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ 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 * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
this✝ : ↑(extChartAt I x) ⁻¹' eball (↑(extChartAt I x) x) (c / ↑C) ∈ 𝓝 x
y : M
hy : y ∈ ↑(extChartAt I x) ⁻¹' eball (↑(extChartAt I x) x) (c / ↑C)
h'y : riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
this : edist (↑(extChartAt I x) x) (↑(extChartAt I x) y) * ↑C < c
⊢ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y) < c

case hb0
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ 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 * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
this✝ : ↑(extChartAt I x) ⁻¹' eball (↑(extChartAt I x) x) (c / ↑C) ∈ 𝓝 x
y : M
hy : y ∈ ↑(extChartAt I x) ⁻¹' eball (↑(extChartAt I x) x) (c / ↑C)
h'y : riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
this : edist (↑(extChartAt I x) x) (↑(extChartAt I x) y) < c / ↑C
⊢ ↑C ≠ 0 ∨ edist (↑(extChartAt I x) x) (↑(extChartAt I x) y) ≠ ∞

case hbt
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ 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 * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
this✝ : ↑(extChartAt I x) ⁻¹' eball (↑(extChartAt I x) x) (c / ↑C) ∈ 𝓝 x
y : M
hy : y ∈ ↑(extChartAt I x) ⁻¹' eball (↑(extChartAt I x) x) (c / ↑C)
h'y : riemannianEDist I x y ≤ ↑C * edist (↑(extChartAt I x) x) (↑(extChartAt I x) y)
this : edist (↑(extChartAt I x) x) (↑(extChartAt I x) y) < c / ↑C
⊢ ↑C ≠ ∞ ∨ edist (↑(extChartAt I x) x) (↑(extChartAt I x) y) ≠ 0