α : Type u_1
β : Type ?u.24924
inst✝ : EDist α
x y : α
s t : Set α
⊢ ∀ (x_1 : α),
    x_1 = x ∨ x_1 = y →
      ∀ (y_1 : α), y_1 = x ∨ y_1 = y → x_1 ≠ y_1 → edist x y ≤ edist x_1 y_1 ∨ edist y x ≤ edist x_1 y_1
α : Type u_1
β : Type ?u.24924
inst✝ : EDist α
x y : α
s t : Set α
⊢ edist x y ⊓ edist y x ≤ einfsep {x, y}
simp_rw [le_einfsep_iff, inf_le_iff, mem_insert_iff, mem_singleton_iff]
no goals
α : Type u_1
β : Type ?u.24924
inst✝ : EDist α
x y : α
s t : Set α
⊢ ∀ (x_1 : α),
    x_1 = x ∨ x_1 = y →
      ∀ (y_1 : α), y_1 = x ∨ y_1 = y → x_1 ≠ y_1 → edist x y ≤ edist x_1 y_1 ∨ edist y x ≤ edist x_1 y_1
rintro a (rfl | rfl) b (rfl | rfl) hab <;> simp only [le_refl, true_or, or_true] <;> contradiction