α : Type u_1
β : Type ?u.422280
γ : Type ?u.422283
inst✝ : PseudoEMetricSpace α
⊢ ∀ (x y : α × α), edist x.fst x.snd ≤ edist y.fst y.snd + 2 * edist x y
α : Type u_1
β : Type ?u.422280
γ : Type ?u.422283
inst✝ : PseudoEMetricSpace α
⊢ Continuous fun p => edist p.fst p.snd
apply continuous_of_le_add_edist 2 (by norm_num)
case mk.mk
α : Type u_1
β : Type ?u.422280
γ : Type ?u.422283
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist (x, y).fst (x, y).snd ≤ edist (x', y').fst (x', y').snd + 2 * edist (x, y) (x', y')
α : Type u_1
β : Type ?u.422280
γ : Type ?u.422283
inst✝ : PseudoEMetricSpace α
⊢ ∀ (x y : α × α), edist x.fst x.snd ≤ edist y.fst y.snd + 2 * edist x y
rintro ⟨x, y⟩ ⟨x', y'⟩
no goals
case mk.mk
α : Type u_1
β : Type ?u.422280
γ : Type ?u.422283
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist (x, y).fst (x, y).snd ≤ edist (x', y').fst (x', y').snd + 2 * edist (x, y) (x', y')
calc
  edist x y ≤ edist x x' + edist x' y' + edist y' y := edist_triangle4 _ _ _ _
  _ = edist x' y' + (edist x x' + edist y y') := by simp only [edist_comm]; ac_rfl
  _ ≤ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y')) :=
    (add_le_add_left (add_le_add (le_max_left _ _) (le_max_right _ _)) _)
  _ = edist x' y' + 2 * edist (x, y) (x', y') := by rw [← mul_two, mul_comm]
no goals
α : Type u_1
β : Type ?u.422280
γ : Type ?u.422283
inst✝ : PseudoEMetricSpace α
⊢ 2 ≠ ⊤
norm_num
α : Type u_1
β : Type ?u.422280
γ : Type ?u.422283
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' + edist x' y' + edist y y' = edist x' y' + (edist x x' + edist y y')
α : Type u_1
β : Type ?u.422280
γ : Type ?u.422283
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' + edist x' y' + edist y' y = edist x' y' + (edist x x' + edist y y')
simp only [edist_comm]
no goals
α : Type u_1
β : Type ?u.422280
γ : Type ?u.422283
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' + edist x' y' + edist y y' = edist x' y' + (edist x x' + edist y y')
ac_rfl
no goals
α : Type u_1
β : Type ?u.422280
γ : Type ?u.422283
inst✝ : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y')) = edist x' y' + 2 * edist (x, y) (x', y')
rw [← mul_two, mul_comm]