-- Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
theorem candidates_lipschitz_aux (fA : f ∈ candidates X Y) :
    f (x, y) - f (z, t) ≤ 2 * maxVar X Y * dist (x, y) (z, t) :=
  calc
    f (x, y) - f (z, t) ≤ f (x, t) + f (t, y) - f (z, t)

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, z) + f (z, t) + f (t, y) - f (z, t) = f (x, z) + f (t, y)

Tactic:
simp [sub_eq_add_neg, add_assoc]

Result:
no goals

Proof state:
case h₂.h
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ dist t y ≤ dist x z ⊔ dist t y

Tactic:
apply le_max_right

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, y) - f (z, t) ≤ f (x, t) + f (t, y) - f (z, t)

Tactic:
gcongr

Result:
case h
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, y) ≤ f (x, t) + f (t, y)

Proof state:
case h
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, y) ≤ f (x, t) + f (t, y)

Tactic:
exact candidates_triangle fA

Result:
no goals

Proof state:
case h₁.h
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ dist x z ≤ dist x z ⊔ dist t y

Tactic:
apply le_max_left

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ ↑(GromovHausdorff.maxVar X Y) * (dist x z ⊔ dist y t) + ↑(GromovHausdorff.maxVar X Y) * (dist x z ⊔ dist y t) =
    2 * ↑(GromovHausdorff.maxVar X Y) * (dist x z ⊔ dist y t)

Tactic:
ring

Result:
no goals

Proof state:
case h.bc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, t) ≤ f (x, z) + f (z, t)

Tactic:
exact candidates_triangle fA

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ ↑(GromovHausdorff.maxVar X Y) * dist x z + ↑(GromovHausdorff.maxVar X Y) * dist t y ≤
    ↑(GromovHausdorff.maxVar X Y) * (dist x z ⊔ dist t y) + ↑(GromovHausdorff.maxVar X Y) * (dist x z ⊔ dist t y)

Tactic:
gcongr

Result:
case h₁.h
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ dist x z ≤ dist x z ⊔ dist t y

case h₂.h
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ dist t y ≤ dist x z ⊔ dist t y

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ ↑(GromovHausdorff.maxVar X Y) * (dist x z ⊔ dist t y) + ↑(GromovHausdorff.maxVar X Y) * (dist x z ⊔ dist t y) =
    2 * ↑(GromovHausdorff.maxVar X Y) * (dist x z ⊔ dist y t)

Tactic:
rw [dist_comm t y]

Result:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ ↑(GromovHausdorff.maxVar X Y) * (dist x z ⊔ dist y t) + ↑(GromovHausdorff.maxVar X Y) * (dist x z ⊔ dist y t) =
    2 * ↑(GromovHausdorff.maxVar X Y) * (dist x z ⊔ dist y t)

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, t) + f (t, y) - f (z, t) ≤ f (x, z) + f (z, t) + f (t, y) - f (z, t)

Tactic:
gcongr

Result:
case h.bc
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, t) ≤ f (x, z) + f (z, t)

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, z) + f (t, y) ≤ ↑(GromovHausdorff.maxVar X Y) * dist x z + ↑(GromovHausdorff.maxVar X Y) * dist t y

Tactic:
gcongr <;> apply candidates_dist_bound fA

Result:
no goals