case a
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
⊢ ∀ (x y : (X ⊕ Y) × (X ⊕ Y)), dist (f x) (f y) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist 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
⊢ LipschitzWith (2 * GromovHausdorff.maxVar X Y) f
apply LipschitzWith.of_dist_le_mul
case a.mk.mk
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
x y z t : X ⊕ Y
⊢ dist (f (x, y)) (f (z, t)) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist (x, y) (z, t)
case a
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
⊢ ∀ (x y : (X ⊕ Y) × (X ⊕ Y)), dist (f x) (f y) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist x y
rintro ⟨x, y⟩ ⟨z, t⟩
case a.mk.mk
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
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)
case a.mk.mk
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
x y z t : X ⊕ Y
⊢ dist (f (x, y)) (f (z, t)) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist (x, y) (z, t)
rw [Real.dist_eq, abs_sub_le_iff]
case a.mk.mk
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
x y z t : X ⊕ Y
⊢ f (z, t) - f (x, y) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist (x, y) (z, t)
case a.mk.mk
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
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)
use candidates_lipschitz_aux fA
case a.mk.mk
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
x y z t : X ⊕ Y
⊢ f (z, t) - f (x, y) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist (z, t) (x, y)
case a.mk.mk
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
x y z t : X ⊕ Y
⊢ f (z, t) - f (x, y) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist (x, y) (z, t)
rw [dist_comm]
no goals
case a.mk.mk
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
x y z t : X ⊕ Y
⊢ f (z, t) - f (x, y) ≤ ↑(2 * GromovHausdorff.maxVar X Y) * dist (z, t) (x, y)
exact candidates_lipschitz_aux fA