[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
⊢ ∀ (e g : X ≃ᵈ Y),
    (fun f => ↑f.toEquiv) e = (fun f => ↑f.toEquiv) g → (fun f => ↑f.symm) e = (fun f => ↑f.symm) g → e = g
[PROOFSTEP]
rintro ⟨⟩ ⟨⟩ h -
[GOAL]
case mk.mk
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
toEquiv✝¹ : X ≃ Y
edist_eq'✝¹ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (Equiv.toFun toEquiv✝¹ x) (Equiv.toFun toEquiv✝¹ y) = ↑r * edist x y
toEquiv✝ : X ≃ Y
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (Equiv.toFun toEquiv✝ x) (Equiv.toFun toEquiv✝ y) = ↑r * edist x y
h :
  (fun f => ↑f.toEquiv) { toEquiv := toEquiv✝¹, edist_eq' := edist_eq'✝¹ } =
    (fun f => ↑f.toEquiv) { toEquiv := toEquiv✝, edist_eq' := edist_eq'✝ }
⊢ { toEquiv := toEquiv✝¹, edist_eq' := edist_eq'✝¹ } = { toEquiv := toEquiv✝, edist_eq' := edist_eq'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toEquiv
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
toEquiv✝¹ : X ≃ Y
edist_eq'✝¹ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (Equiv.toFun toEquiv✝¹ x) (Equiv.toFun toEquiv✝¹ y) = ↑r * edist x y
toEquiv✝ : X ≃ Y
edist_eq'✝ : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (Equiv.toFun toEquiv✝ x) (Equiv.toFun toEquiv✝ y) = ↑r * edist x y
h :
  (fun f => ↑f.toEquiv) { toEquiv := toEquiv✝¹, edist_eq' := edist_eq'✝¹ } =
    (fun f => ↑f.toEquiv) { toEquiv := toEquiv✝, edist_eq' := edist_eq'✝ }
⊢ toEquiv✝¹ = toEquiv✝
[PROOFSTEP]
exact FunLike.ext' h
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
⊢ ∃ r, r ≠ 0 ∧ ∀ (x y : Y), edist (Equiv.toFun e.symm x) (Equiv.toFun e.symm y) = ↑r * edist x y
[PROOFSTEP]
refine ⟨(ratio e)⁻¹, inv_ne_zero <| ratio_ne_zero e, e.surjective.forall₂.2 fun x y ↦ ?_⟩
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
x y : X
⊢ edist (Equiv.toFun e.symm (↑e.toEquiv x)) (Equiv.toFun e.symm (↑e.toEquiv y)) =
    ↑(ratio e)⁻¹ * edist (↑e.toEquiv x) (↑e.toEquiv y)
[PROOFSTEP]
simp_rw [Equiv.toFun_as_coe, Equiv.symm_apply_apply, coe_toEquiv, edist_eq]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
x y : X
⊢ edist x y = ↑(ratio e)⁻¹ * (↑(ratio e) * edist x y)
[PROOFSTEP]
rw [← mul_assoc, ← ENNReal.coe_mul, inv_mul_cancel (ratio_ne_zero e), ENNReal.coe_one, one_mul]
[GOAL]
X✝ : Type u_1
Y : Type u_2
Z : Type u_3
inst✝³ : PseudoEMetricSpace X✝
inst✝² : PseudoEMetricSpace Y
inst✝¹ : PseudoEMetricSpace Z
X : Type u_4
inst✝ : PseudoEMetricSpace X
x✝¹ x✝ : X
⊢ edist (Equiv.toFun (Equiv.refl X) x✝¹) (Equiv.toFun (Equiv.refl X) x✝) = ↑1 * edist x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
⊢ ratio (trans e e') = ratio e * ratio e'
[PROOFSTEP]
by_cases hX : ∀ x y : X, edist x y = 0 ∨ edist x y = ∞
[GOAL]
case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (trans e e') = ratio e * ratio e'
[PROOFSTEP]
have hY : ∀ x y : Y, edist x y = 0 ∨ edist x y = ∞ :=
  e.surjective.forall₂.2 fun x y ↦ by refine (hX x y).imp (fun h ↦ ?_) fun h ↦ ?_ <;> simp [*, Dilation.ratio_ne_zero]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ⊤
x y : X
⊢ edist (↑e x) (↑e y) = 0 ∨ edist (↑e x) (↑e y) = ⊤
[PROOFSTEP]
refine (hX x y).imp (fun h ↦ ?_) fun h ↦ ?_
[GOAL]
case refine_1
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ⊤
x y : X
h : edist x y = 0
⊢ edist (↑e x) (↑e y) = 0
[PROOFSTEP]
simp [*, Dilation.ratio_ne_zero]
[GOAL]
case refine_2
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ⊤
x y : X
h : edist x y = ⊤
⊢ edist (↑e x) (↑e y) = ⊤
[PROOFSTEP]
simp [*, Dilation.ratio_ne_zero]
[GOAL]
case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ⊤
hY : ∀ (x y : Y), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (trans e e') = ratio e * ratio e'
[PROOFSTEP]
simp [Dilation.ratio_of_trivial, *]
[GOAL]
case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ¬∀ (x y : X), edist x y = 0 ∨ edist x y = ⊤
⊢ ratio (trans e e') = ratio e * ratio e'
[PROOFSTEP]
push_neg at hX 
[GOAL]
case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∃ x y, edist x y ≠ 0 ∧ edist x y ≠ ⊤
⊢ ratio (trans e e') = ratio e * ratio e'
[PROOFSTEP]
exact (Dilation.ratio_comp' (g := e'.toDilation) (f := e.toDilation) hX).trans (mul_comm _ _)
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ Y
⊢ ratio (symm e) * ratio e = 1
[PROOFSTEP]
rw [← ratio_trans, symm_trans_self, ratio_refl]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ X
n : ℕ
⊢ ↑(e ^ n) = (↑e)^[n]
[PROOFSTEP]
rw [← coe_toEquiv, ← toPerm_apply, map_pow, Equiv.Perm.coe_pow]
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
e : X ≃ᵈ X
n : ℕ
⊢ (↑(↑toPerm e))^[n] = (↑e)^[n]
[PROOFSTEP]
rfl
