[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f g : α →ᵈ β
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
g : α →ᵈ β
toFun✝ : α → β
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun✝ x) (toFun✝ y) = ↑r * edist x y
h : { toFun := toFun✝, edist_eq' := edist_eq'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, edist_eq' := edist_eq'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
toFun✝¹ : α → β
edist_eq'✝¹ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun✝¹ x) (toFun✝¹ y) = ↑r * edist x y
toFun✝ : α → β
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (toFun✝ x) (toFun✝ y) = ↑r * edist x y
h : { toFun := toFun✝¹, edist_eq' := edist_eq'✝¹ }.toFun = { toFun := toFun✝, edist_eq' := edist_eq'✝ }.toFun
⊢ { toFun := toFun✝¹, edist_eq' := edist_eq'✝¹ } = { toFun := toFun✝, edist_eq' := edist_eq'✝ }
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : Subsingleton α
inst✝ : DilationClass F α β
f : F
x y : α
⊢ edist x y = 0 ∨ edist x y = ⊤
[PROOFSTEP]
simp [Subsingleton.elim x y]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
⊢ ratio f ≠ 0
[PROOFSTEP]
rw [ratio]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
⊢ (if ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤ then 1
    else Exists.choose (_ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (↑f x) (↑f y) = ↑r * edist x y)) ≠
    0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
h✝ : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
h✝ : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ Exists.choose (_ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (↑f x) (↑f y) = ↑r * edist x y) ≠ 0
[PROOFSTEP]
exact (DilationClass.edist_eq' f).choose_spec.1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ edist (↑f x) (↑f y) = ↑(ratio f) * edist x y
[PROOFSTEP]
rw [ratio]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ edist (↑f x) (↑f y) =
    ↑(if ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤ then 1
        else Exists.choose (_ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (↑f x) (↑f y) = ↑r * edist x y)) *
      edist x y
[PROOFSTEP]
split_ifs with key
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ edist (↑f x) (↑f y) = ↑1 * edist x y
[PROOFSTEP]
rcases DilationClass.edist_eq' f with ⟨r, hne, hr⟩
[GOAL]
case pos.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
r : ℝ≥0
hne : r ≠ 0
hr : ∀ (x y : α), edist (↑f x) (↑f y) = ↑r * edist x y
⊢ edist (↑f x) (↑f y) = ↑1 * edist x y
[PROOFSTEP]
replace hr := hr x y
[GOAL]
case pos.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
r : ℝ≥0
hne : r ≠ 0
hr : edist (↑f x) (↑f y) = ↑r * edist x y
⊢ edist (↑f x) (↑f y) = ↑1 * edist x y
[PROOFSTEP]
cases' key x y with h h
[GOAL]
case pos.intro.intro.inl
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
r : ℝ≥0
hne : r ≠ 0
hr : edist (↑f x) (↑f y) = ↑r * edist x y
h : edist x y = 0
⊢ edist (↑f x) (↑f y) = ↑1 * edist x y
[PROOFSTEP]
simp only [hr, h, mul_zero]
[GOAL]
case pos.intro.intro.inr
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
r : ℝ≥0
hne : r ≠ 0
hr : edist (↑f x) (↑f y) = ↑r * edist x y
h : edist x y = ⊤
⊢ edist (↑f x) (↑f y) = ↑1 * edist x y
[PROOFSTEP]
simp [hr, h, hne]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
key : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ edist (↑f x) (↑f y) =
    ↑(Exists.choose (_ : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (↑f x) (↑f y) = ↑r * edist x y)) * edist x y
[PROOFSTEP]
exact (DilationClass.edist_eq' f).choose_spec.2 x y
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F✝ : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
α : Type u_6
β : Type u_7
F : Type u_8
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ nndist (↑f x) (↑f y) = ratio f * nndist x y
[PROOFSTEP]
simp only [← ENNReal.coe_eq_coe, ← edist_nndist, ENNReal.coe_mul, edist_eq]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F✝ : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
α : Type u_6
β : Type u_7
F : Type u_8
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ dist (↑f x) (↑f y) = ↑(ratio f) * dist x y
[PROOFSTEP]
simp only [dist_nndist, nndist_eq, NNReal.coe_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
h₀ : edist x y ≠ 0
htop : edist x y ≠ ⊤
hr : edist (↑f x) (↑f y) = ↑r * edist x y
⊢ r = ratio f
[PROOFSTEP]
simpa only [hr, ENNReal.mul_eq_mul_right h₀ htop, ENNReal.coe_eq_coe] using edist_eq f x y
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F✝ : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
α : Type u_6
β : Type u_7
F : Type u_8
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : nndist x y ≠ 0
hr : nndist (↑f x) (↑f y) = r * nndist x y
⊢ edist x y ≠ 0
[PROOFSTEP]
rwa [edist_nndist, ENNReal.coe_ne_zero]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F✝ : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
α : Type u_6
β : Type u_7
F : Type u_8
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : nndist x y ≠ 0
hr : nndist (↑f x) (↑f y) = r * nndist x y
⊢ edist (↑f x) (↑f y) = ↑r * edist x y
[PROOFSTEP]
rw [edist_nndist, edist_nndist, hr, ENNReal.coe_mul]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F✝ : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β✝
α : Type u_7
β : Type u_8
F : Type u_6
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : dist x y ≠ 0
hr : dist (↑f x) (↑f y) = ↑r * dist x y
⊢ ↑(nndist (↑f x) (↑f y)) = ↑(r * nndist x y)
[PROOFSTEP]
rw [coe_nndist, hr, NNReal.coe_mul, coe_nndist]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : PseudoEMetricSpace α✝
inst✝² : PseudoEMetricSpace β✝
α : Type ?u.24367
β : Type ?u.24370
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
⊢ ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y
[PROOFSTEP]
rcases h with ⟨r, hne, h⟩
[GOAL]
case intro.intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : PseudoEMetricSpace α✝
inst✝² : PseudoEMetricSpace β✝
α : Type ?u.24367
β : Type ?u.24370
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
r : ℝ≥0
hne : r ≠ 0
h : ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
⊢ ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y
[PROOFSTEP]
refine' ⟨r, hne, fun x y => _⟩
[GOAL]
case intro.intro
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : PseudoEMetricSpace α✝
inst✝² : PseudoEMetricSpace β✝
α : Type ?u.24367
β : Type ?u.24370
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
r : ℝ≥0
hne : r ≠ 0
h : ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
x y : α
⊢ edist (f x) (f y) = ↑r * edist x y
[PROOFSTEP]
rw [edist_nndist, edist_nndist, ← ENNReal.coe_mul, h x y]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝³ : PseudoEMetricSpace α✝
inst✝² : PseudoEMetricSpace β✝
α : Type ?u.25376
β : Type ?u.25379
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y
r : ℝ≥0
hr : r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y
x y : α
⊢ ↑(nndist (f x) (f y)) = ↑(r * nndist x y)
[PROOFSTEP]
rw [coe_nndist, hr.2, NNReal.coe_mul, coe_nndist]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x✝ y✝ z : α
s : Set α
x y : α
⊢ edist x y ≤ ↑(ratio f)⁻¹ * edist (↑f x) (↑f y)
[PROOFSTEP]
have hr : ratio f ≠ 0 := ratio_ne_zero f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x✝ y✝ z : α
s : Set α
x y : α
hr : ratio f ≠ 0
⊢ edist x y ≤ ↑(ratio f)⁻¹ * edist (↑f x) (↑f y)
[PROOFSTEP]
exact_mod_cast (ENNReal.mul_le_iff_le_inv (ENNReal.coe_ne_zero.2 hr) ENNReal.coe_ne_top).1 (edist_eq f x y).ge
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁵ : PseudoEMetricSpace α✝
inst✝⁴ : PseudoEMetricSpace β
inst✝³ : PseudoEMetricSpace γ
inst✝² : DilationClass F α✝ β
inst✝¹ : DilationClass G β γ
f : F
g : G
x✝ y✝ z : α✝
s : Set α✝
α : Type ?u.28806
inst✝ : PseudoEMetricSpace α
x y : α
⊢ edist (id x) (id y) = ↑1 * edist x y
[PROOFSTEP]
simp only [id.def, ENNReal.coe_one, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s : Set α
⊢ ratio (Dilation.id α) = 1
[PROOFSTEP]
by_cases h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s : Set α
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (Dilation.id α) = 1
[PROOFSTEP]
rw [ratio, if_pos h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s : Set α
h : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (Dilation.id α) = 1
[PROOFSTEP]
push_neg at h 
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s : Set α
h : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (Dilation.id α) = 1
[PROOFSTEP]
rcases h with ⟨x, y, hne⟩
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x✝ y✝ z : α
s : Set α
x y : α
hne : edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (Dilation.id α) = 1
[PROOFSTEP]
refine' (ratio_unique hne.1 hne.2 _).symm
[GOAL]
case neg.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x✝ y✝ z : α
s : Set α
x y : α
hne : edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ edist (↑(Dilation.id α) x) (↑(Dilation.id α) y) = ↑1 * edist x y
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f✝ : F
g✝ : G
x✝ y✝ z : α
s : Set α
g : β →ᵈ γ
f : α →ᵈ β
x y : α
⊢ edist ((↑g ∘ ↑f) x) ((↑g ∘ ↑f) y) = ↑(ratio g * ratio f) * edist x y
[PROOFSTEP]
simp_rw [Function.comp, edist_eq, ENNReal.coe_mul, mul_assoc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f✝ : F
g✝ : G
x y z : α
s : Set α
g : β →ᵈ γ
f : α →ᵈ β
hne : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (comp g f) = ratio g * ratio f
[PROOFSTEP]
rcases hne with ⟨x, y, hα⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f✝ : F
g✝ : G
x✝ y✝ z : α
s : Set α
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (comp g f) = ratio g * ratio f
[PROOFSTEP]
have hgf := (edist_eq (g.comp f) x y).symm
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f✝ : F
g✝ : G
x✝ y✝ z : α
s : Set α
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ⊤
hgf : ↑(ratio (comp g f)) * edist x y = edist (↑(comp g f) x) (↑(comp g f) y)
⊢ ratio (comp g f) = ratio g * ratio f
[PROOFSTEP]
simp_rw [coe_comp, Function.comp, edist_eq, ← mul_assoc, ENNReal.mul_eq_mul_right hα.1 hα.2] at hgf 
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f✝ : F
g✝ : G
x✝ y✝ z : α
s : Set α
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ⊤
hgf : ↑(ratio (comp g f)) = ↑(ratio g) * ↑(ratio f)
⊢ ratio (comp g f) = ratio g * ratio f
[PROOFSTEP]
rwa [← ENNReal.coe_eq_coe, ENNReal.coe_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f✝ : F
g✝ : G
x y z : α
s : Set α
f g : α →ᵈ α
⊢ ratio (f * g) = ratio f * ratio g
[PROOFSTEP]
by_cases h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f✝ : F
g✝ : G
x y z : α
s : Set α
f g : α →ᵈ α
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (f * g) = ratio f * ratio g
[PROOFSTEP]
simp [ratio_of_trivial, h]
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f✝ : F
g✝ : G
x y z : α
s : Set α
f g : α →ᵈ α
h : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (f * g) = ratio f * ratio g
[PROOFSTEP]
push_neg at h 
[GOAL]
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f✝ : F
g✝ : G
x y z : α
s : Set α
f g : α →ᵈ α
h : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (f * g) = ratio f * ratio g
[PROOFSTEP]
exact ratio_comp' h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g✝ : G
x✝ y z : α
s : Set α
g : β →ᵈ γ
f₁ f₂ : α →ᵈ β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
x : α
⊢ ↑g (↑f₁ x) = ↑g (↑f₂ x)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s✝ s : Set α
⊢ EMetric.diam (↑f '' s) = ↑(ratio f) * EMetric.diam s
[PROOFSTEP]
refine' ((lipschitz f).ediam_image_le s).antisymm _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s✝ s : Set α
⊢ ↑(ratio f) * EMetric.diam s ≤ EMetric.diam (↑f '' s)
[PROOFSTEP]
apply ENNReal.mul_le_of_le_div'
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s✝ s : Set α
⊢ EMetric.diam s ≤ EMetric.diam (↑f '' s) / ↑(ratio f)
[PROOFSTEP]
rw [div_eq_mul_inv, mul_comm, ← ENNReal.coe_inv]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s✝ s : Set α
⊢ EMetric.diam s ≤ ↑(ratio f)⁻¹ * EMetric.diam (↑f '' s)
case h
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s✝ s : Set α
⊢ ratio f ≠ 0
[PROOFSTEP]
exacts [(antilipschitz f).le_mul_ediam_image s, ratio_ne_zero f]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s : Set α
⊢ EMetric.diam (range ↑f) = ↑(ratio f) * EMetric.diam univ
[PROOFSTEP]
rw [← image_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x y z : α
s : Set α
⊢ EMetric.diam (↑f '' univ) = ↑(ratio f) * EMetric.diam univ
[PROOFSTEP]
exact ediam_image f univ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : DilationClass F α β
inst✝ : DilationClass G β γ
f : F
g : G
x✝ y✝ z : α
s : Set α
x : α
r' : ℝ≥0∞
y : α
hy : y ∈ EMetric.closedBall x r'
⊢ edist y x ≤ r'
[PROOFSTEP]
exact hy
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : DilationClass F α β
f : F
s : Set α
⊢ Metric.diam (↑f '' s) = ↑(ratio f) * Metric.diam s
[PROOFSTEP]
simp [Metric.diam, ediam_image, ENNReal.toReal_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
G : Type u_5
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : DilationClass F α β
f : F
⊢ Metric.diam (range ↑f) = ↑(ratio f) * Metric.diam univ
[PROOFSTEP]
rw [← image_univ, diam_image]
