-- Mathlib/Topology/MetricSpace/Dilation.lean
theorem edist_eq [DilationClass F α β] (f : F) (x y : α) :
    edist (f x) (f y) = ratio f * edist x y

Proof state:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
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 ⋯.choose) * edist x y

Tactic:
split_ifs with key

Result:
case pos
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
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

case neg
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
key : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ edist (f x) (f y) = ↑⋯.choose * edist x y

Proof state:
case pos.intro.intro.inl
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
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

Tactic:
simp only [hr, h, mul_zero]

Result:
no goals

Proof state:
case pos.intro.intro.inr
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
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

Tactic:
simp [hr, h, hne]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
⊢ edist (f x) (f y) = ↑(ratio f) * edist x y

Tactic:
rw [ratio]

Result:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
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 ⋯.choose) * edist x y

Proof state:
case neg
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
x y : α
key : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ edist (f x) (f y) = ↑⋯.choose * edist x y

Tactic:
exact (DilationClass.edist_eq' f).choose_spec.2 x y

Result:
no goals

Proof state:
case pos.intro.intro
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
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

Tactic:
replace hr := hr x y

Result:
case pos.intro.intro
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
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

Proof state:
case pos.intro.intro
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
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

Tactic:
rcases key x y with h | h

Result:
case pos.intro.intro.inl
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
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

case pos.intro.intro.inr
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
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

Proof state:
case pos
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
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

Tactic:
rcases DilationClass.edist_eq' f with ⟨r, hne, hr⟩

Result:
case pos.intro.intro
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
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