case a
α : Type u
β : Type v
X : Type ?u.5599
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z ≤ edist y z

case a
α : Type u
β : Type v
X : Type ?u.5599
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist y z ≤ edist x z
α : Type u
β : Type v
X : Type ?u.5599
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z = edist y z
apply le_antisymm
case a
α : Type u
β : Type v
X : Type ?u.5599
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z ≤ edist x y + edist y z
case a
α : Type u
β : Type v
X : Type ?u.5599
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z ≤ edist y z
rw [← zero_add (edist y z), ← h]
no goals
case a
α : Type u
β : Type v
X : Type ?u.5599
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z ≤ edist x y + edist y z
apply edist_triangle
case a
α : Type u
β : Type v
X : Type ?u.5599
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist y x = 0
⊢ edist y z ≤ edist x z
case a
α : Type u
β : Type v
X : Type ?u.5599
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist y z ≤ edist x z
rw [edist_comm] at h
case a
α : Type u
β : Type v
X : Type ?u.5599
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist y x = 0
⊢ edist y z ≤ edist y x + edist x z
case a
α : Type u
β : Type v
X : Type ?u.5599
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist y x = 0
⊢ edist y z ≤ edist x z
rw [← zero_add (edist x z), ← h]
no goals
case a
α : Type u
β : Type v
X : Type ?u.5599
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist y x = 0
⊢ edist y z ≤ edist y x + edist x z
apply edist_triangle