-- Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
theorem candidates_lipschitz (fA : f ∈ candidates X Y) :
    LipschitzWith (2 * maxVar X Y) f

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

Tactic:
rw [dist_comm]

Result:
case right
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
⊢ f (z, t) - f (x, y) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist (z, t) (x, y)

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

Tactic:
exact candidates_lipschitz_aux fA

Result:
no goals

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

Tactic:
rw [Real.dist_eq, abs_sub_le_iff]

Result:
case a.mk.mk
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
⊢ f (x, y) - f (z, t) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist (x, y) (z, t) ∧
    f (z, t) - f (x, y) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist (x, y) (z, t)

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

Tactic:
use candidates_lipschitz_aux fA

Result:
case right
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
⊢ f (z, t) - f (x, y) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist (x, y) (z, t)

Proof state:
case a
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
⊢ ∀ (x y : (X ⊕ Y) × (X ⊕ Y)), dist (f x) (f y) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist x y

Tactic:
rintro ⟨x, y⟩ ⟨z, t⟩

Result:
case a.mk.mk
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
⊢ dist (f (x, y)) (f (z, t)) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist (x, y) (z, t)

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
⊢ LipschitzWith (2 * GromovHausdorff.maxVar X Y) f

Tactic:
apply LipschitzWith.of_dist_le_mul

Result:
case a
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
⊢ ∀ (x y : (X ⊕ Y) × (X ⊕ Y)), dist (f x) (f y) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist x y