X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
this : 0 ≤ 2 * f (x, y)
⊢ 0 ≤ f (x, y)
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ 0 ≤ f (x, y)
have : 0 ≤ 2 * f (x, y) :=
  calc
    0 = f (x, x) := (candidates_refl fA).symm
    _ ≤ f (x, y) + f (y, x) := (candidates_triangle fA)
    _ = f (x, y) + f (x, y) := by rw [candidates_symm fA]
    _ = 2 * f (x, y) := by ring
no goals
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
this : 0 ≤ 2 * f (x, y)
⊢ 0 ≤ f (x, y)
linarith
no goals
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, y) + f (y, x) = f (x, y) + f (x, y)
rw [candidates_symm fA]
no goals
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, y) + f (x, y) = 2 * f (x, y)
ring