awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
h₁ : 0 ≤ diam.{u} (α := X) univ
h₂ : 0 ≤ diam.{v} (α := Y) univ
⊢ HMul.hMul (α := ℝ) 2 0 + 1 + HMul.hMul (α := ℝ) 2 0 ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
⊢ 0 ≤ diam.{u} (α := X) univ

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
⊢ 0 ≤ diam.{v} (α := Y) univ

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x y : X ⊕ Y
inst_2 : CompactSpace X
inst_3 : Nonempty X
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
rw rw₁ : diam (α := X ⊕ Y) univ = diam (α := X ⊕ Y) univ
⊢ diam (α := X ⊕ Y) univ = diam (α := X ⊕ Y) (range inl ∪ range inr)

Tactic:
rw [range_inl_union_range_inr]

Premises used: Set.range_inl_union_range_inr
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x y : X ⊕ Y
inst_2 : CompactSpace X
inst_3 : Nonempty X
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
rw :
  diam.{u} (α := X) univ + dist (α := X ⊕ Y) (inl default) (inr default) + diam.{v} (α := Y) univ =
    diam.{u} (α := X) univ + (dist.{u} (α := X) default default + 1 + dist.{v} (α := Y) default default) +
      diam.{v} (α := Y) univ
⊢ diam (α := X ⊕ Y) (range inl) + dist (α := X ⊕ Y) (inl default) (inr default) + diam (α := X ⊕ Y) (range inr) =
    diam.{u} (α := X) univ + (dist.{u} (α := X) default default + 1 + dist.{v} (α := Y) default default) +
      diam.{v} (α := Y) univ

Tactic:
rw [isometry_inl.diam_range, isometry_inr.diam_range]

Premises used: Isometry.diam_range, Metric.isometry_inl, Metric.isometry_inr
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x y : X ⊕ Y
inst_2 : CompactSpace X
inst_3 : Nonempty X
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
⊢ diam.{u} (α := X) univ + dist (α := X ⊕ Y) (inl default) (inr default) + diam.{v} (α := Y) univ =
    diam.{u} (α := X) univ + (dist.{u} (α := X) default default + 1 + dist.{v} (α := Y) default default) +
      diam.{v} (α := Y) univ

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x y : X ⊕ Y
inst_2 : CompactSpace X
inst_3 : Nonempty X
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
⊢ diam.{u} (α := X) univ + (dist.{u} (α := X) default default + 1 + dist.{v} (α := Y) default default) +
      diam.{v} (α := Y) univ =
    1 * diam.{u} (α := X) univ + 1 + 1 * diam.{v} (α := Y) univ

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x y : X ⊕ Y
inst_2 : CompactSpace X
inst_3 : Nonempty X
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
h₁ h₂ : LE.le (α := ℝ) 1 2
⊢ 1 * diam.{u} (α := X) univ + 1 + 1 * diam.{v} (α := Y) univ ≤
    2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
x y : X ⊕ Y
inst_2 : CompactSpace X
inst_3 : Nonempty X
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
⊢ LE.le (α := ℝ) 1 2

Tactic:
norm_num
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x y : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, y) = f (y, x)

Tactic:
fA.1.1.1.2 x y

Premises used: And.right, And.left
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x y z : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, z) ≤ f (x, y) + f (y, z)

Tactic:
fA.1.1.2 x y z

Premises used: And.right, And.left
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, x) = 0

Tactic:
fA.1.2 x

Premises used: And.right, And.left
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x y : X ⊕ Y
fA : f ∈ candidates X Y
⊢ 0 ≤ f (x, y)

Tactic:
grind [candidates_symm, candidates_triangle]

Premises used: _private.0.GromovHausdorff.candidates_symm, _private.0.GromovHausdorff.candidates_triangle
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : X
⊢ f (inl x, inl y) = dist x y

Tactic:
fA.1.1.1.1.1 x y

Premises used: And.left
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ f (inr x, inr y) = dist x y

Tactic:
fA.1.1.1.1.2 x y

Premises used: And.right, And.left
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x y : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, y) ≤ (↑(maxVar X Y) : ℝ)

Tactic:
fA.2 x y

Premises used: And.right
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : X
⊢ dist x y = Sum.dist.{u, v} (Y := Y) (inl x) (inl y)

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : X
⊢ dist (α := X ⊕ Y) (inl x) (inl y) = 1 * dist (α := X ⊕ Y) (inl x) (inl y)

Tactic:
ring
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : X
hbc : 1 ≤ (↑(maxVar X Y) : ℝ)
⊢ 1 * dist (α := X ⊕ Y) (inl x) (inl y) ≤ (↑(maxVar X Y) : ℝ) * dist (α := X ⊕ Y) (inl x) (inl y)

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : X
⊢ 1 ≤ (↑(maxVar X Y) : ℝ)

Tactic:
one_le_maxVar X Y

Premises used: _private.0.GromovHausdorff.one_le_maxVar, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : X
⊢ 1 ≤ (↑(maxVar X Y) : ℝ)

Tactic:
exact one_le_maxVar X Y

Premises used: _private.0.GromovHausdorff.one_le_maxVar
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : X
y : Y
⊢ (↑(maxVar X Y) : ℝ) = (↑(maxVar X Y) : ℝ) * 1

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : X
y : Y
hbc : 1 ≤ dist (inl x) (inr y)
⊢ (↑(maxVar X Y) : ℝ) * 1 ≤ (↑(maxVar X Y) : ℝ) * dist (inl x) (inr y)

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : X
y : Y
⊢ 1 ≤ dist (inl x) (inr y)

Tactic:
apply Sum.one_le_dist_inl_inr

Premises used: Metric.Sum.one_le_dist_inl_inr
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : Y
y : X
⊢ (↑(maxVar X Y) : ℝ) = (↑(maxVar X Y) : ℝ) * 1

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : Y
y : X
hbc : 1 ≤ dist (inl x) (inr y)
⊢ (↑(maxVar X Y) : ℝ) * 1 ≤ (↑(maxVar X Y) : ℝ) * dist (inl x) (inr y)

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : Y
y : X
⊢ 1 ≤ dist (inl x) (inr y)

Tactic:
apply Sum.one_le_dist_inl_inr

Premises used: Metric.Sum.one_le_dist_inl_inr
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ dist x y = Sum.dist.{u, v} (X := X) (inr x) (inr y)

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ dist (α := X ⊕ Y) (inr x) (inr y) = 1 * dist (α := X ⊕ Y) (inr x) (inr y)

Tactic:
ring
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
hbc : 1 ≤ (↑(maxVar X Y) : ℝ)
⊢ 1 * dist (α := X ⊕ Y) (inr x) (inr y) ≤ (↑(maxVar X Y) : ℝ) * dist (α := X ⊕ Y) (inr x) (inr y)

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ 1 ≤ (↑(maxVar X Y) : ℝ)

Tactic:
one_le_maxVar X Y

Premises used: _private.0.GromovHausdorff.one_le_maxVar, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ 1 ≤ (↑(maxVar X Y) : ℝ)

Tactic:
exact one_le_maxVar X Y

Premises used: _private.0.GromovHausdorff.one_le_maxVar
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, y) - f (z, t) ≤ f (x, z) + f (z, t) + f (t, y) - f (z, t)

Tactic:
grind [candidates_triangle]

Premises used: _private.0.GromovHausdorff.candidates_triangle
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : 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]

Premises used: add_assoc, sub_eq_add_neg
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
h₁ : f (x, z) ≤ (↑(maxVar X Y) : ℝ) * dist x z
h₂ : f (t, y) ≤ (↑(maxVar X Y) : ℝ) * dist t y
⊢ f (x, z) + f (t, y) ≤ (↑(maxVar X Y) : ℝ) * dist x z + (↑(maxVar X Y) : ℝ) * dist t y

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (x, z) ≤ (↑(maxVar X Y) : ℝ) * dist x z

Tactic:
apply candidates_dist_bound fA

Premises used: _private.0.GromovHausdorff.candidates_dist_bound
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ f (t, y) ≤ (↑(maxVar X Y) : ℝ) * dist t y

Tactic:
apply candidates_dist_bound fA

Premises used: _private.0.GromovHausdorff.candidates_dist_bound
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
h₁ : dist x z ≤ max (dist x z) (dist t y)
h₂ : dist t y ≤ max (dist x z) (dist t y)
⊢ (↑(maxVar X Y) : ℝ) * dist x z + (↑(maxVar X Y) : ℝ) * dist t y ≤
    (↑(maxVar X Y) : ℝ) * max (dist x z) (dist t y) + (↑(maxVar X Y) : ℝ) * max (dist x z) (dist t y)

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ dist x z ≤ max (dist x z) (dist t y)

Tactic:
apply le_max_left

Premises used: le_max_left
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ dist t y ≤ max (dist x z) (dist t y)

Tactic:
apply le_max_right

Premises used: le_max_right
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
rw :
  (↑(maxVar X Y) : ℝ) * max (dist x z) (dist y t) + (↑(maxVar X Y) : ℝ) * max (dist x z) (dist y t) =
    2 * (↑(maxVar X Y) : ℝ) * max (dist x z) (dist y t)
⊢ (↑(maxVar X Y) : ℝ) * max (dist x z) (dist t y) + (↑(maxVar X Y) : ℝ) * max (dist x z) (dist t y) =
    2 * (↑(maxVar X Y) : ℝ) * max (dist x z) (dist y t)

Tactic:
rw [dist_comm t y]

Premises used: dist_comm
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
x y z t : X ⊕ Y
fA : f ∈ candidates X Y
⊢ (↑(maxVar X Y) : ℝ) * max (dist x z) (dist y t) + (↑(maxVar X Y) : ℝ) * max (dist x z) (dist y t) =
    2 * (↑(maxVar X Y) : ℝ) * max (dist x z) (dist y t)

Tactic:
ring
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
a : ∀ (x y : (X ⊕ Y) × (X ⊕ Y)), dist (f x) (f y) ≤ (↑(2 * maxVar X Y) : ℝ) * dist x y
⊢ LipschitzWith (2 * maxVar X Y) f

Tactic:
apply LipschitzWith.of_dist_le_mul

Premises used: LipschitzWith.of_dist_le_mul
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
a :
  f (x, y) - f (z, t) ≤ (↑(2 * maxVar X Y) : ℝ) * dist (x, y) (z, t) ∧
    f (z, t) - f (x, y) ≤ (↑(2 * maxVar X Y) : ℝ) * dist (x, y) (z, t)
⊢ dist (f (x, y)) (f (z, t)) ≤ (↑(2 * maxVar X Y) : ℝ) * dist (x, y) (z, t)

Tactic:
rw [Real.dist_eq, abs_sub_le_iff]

Premises used: abs_sub_le_iff, Real.dist_eq
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
right : f (z, t) - f (x, y) ≤ (↑(2 * maxVar X Y) : ℝ) * dist (x, y) (z, t)
⊢ f (x, y) - f (z, t) ≤ (↑(2 * maxVar X Y) : ℝ) * dist (x, y) (z, t) ∧
    f (z, t) - f (x, y) ≤ (↑(2 * maxVar X Y) : ℝ) * dist (x, y) (z, t)

Tactic:
use candidates_lipschitz_aux fA

Premises used: _private.0.GromovHausdorff.candidates_lipschitz_aux
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
right : f (z, t) - f (x, y) ≤ (↑(2 * maxVar X Y) : ℝ) * dist (z, t) (x, y)
⊢ f (z, t) - f (x, y) ≤ (↑(2 * maxVar X Y) : ℝ) * dist (x, y) (z, t)

Tactic:
rw [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
⊢ f (z, t) - f (x, y) ≤ (↑(2 * maxVar X Y) : ℝ) * dist (z, t) (x, y)

Tactic:
candidates_lipschitz_aux fA

Premises used: _private.0.GromovHausdorff.candidates_lipschitz_aux, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
⊢ f (z, t) - f (x, y) ≤ (↑(2 * maxVar X Y) : ℝ) * dist (z, t) (x, y)

Tactic:
exact candidates_lipschitz_aux fA

Premises used: _private.0.GromovHausdorff.candidates_lipschitz_aux
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
⊢ ∀ (x y : X), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inl y) = dist x y}

Tactic:
have I1 : ∀ x y, IsClosed { f : Cb X Y | f (inl x, inl y) = dist x y } := fun x y =>
    isClosed_eq (continuous_eval_const _) continuous_const
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
I1 : ∀ (x y : X), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inl y) = dist x y}
⊢ ∀ (x y : Y), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inr x, inr y) = dist x y}

Tactic:
have I2 : ∀ x y, IsClosed { f : Cb X Y | f (inr x, inr y) = dist x y } := fun x y =>
    isClosed_eq (continuous_eval_const _) continuous_const
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
I1 : ∀ (x y : X), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inr x, inr y) = dist x y}
⊢ ∀ (x y : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, x) : ℝ)}

Tactic:
have I3 : ∀ x y, IsClosed { f : Cb X Y | f (x, y) = f (y, x) } := fun x y =>
    isClosed_eq (continuous_eval_const _) (continuous_eval_const _)
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
I1 : ∀ (x y : X), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inr x, inr y) = dist x y}
I3 :
  ∀ (x y : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, x) : ℝ)}
⊢ ∀ (x y z : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, z) ≤
          HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ)
            ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, z) : ℝ)}

Tactic:
have I4 : ∀ x y z, IsClosed { f : Cb X Y | f (x, z) ≤ f (x, y) + f (y, z) } := fun x y z =>
    isClosed_le (continuous_eval_const _) ((continuous_eval_const _).add (continuous_eval_const _))
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
I1 : ∀ (x y : X), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inr x, inr y) = dist x y}
I3 :
  ∀ (x y : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, x) : ℝ)}
I4 :
  ∀ (x y z : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, z) ≤
          HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ)
            ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, z) : ℝ)}
⊢ ∀ (x : X ⊕ Y),
    IsClosed (X := Cb X Y) {f : Cb X Y | Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, x) : ℝ) (0 : ℝ)}

Tactic:
have I5 : ∀ x, IsClosed { f : Cb X Y | f (x, x) = 0 } := fun x =>
    isClosed_eq (continuous_eval_const _) continuous_const
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
I1 : ∀ (x y : X), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inr x, inr y) = dist x y}
I3 :
  ∀ (x y : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, x) : ℝ)}
I4 :
  ∀ (x y z : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, z) ≤
          HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ)
            ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, z) : ℝ)}
I5 :
  ∀ (x : X ⊕ Y),
    IsClosed (X := Cb X Y) {f : Cb X Y | Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, x) : ℝ) (0 : ℝ)}
⊢ ∀ (x y : X ⊕ Y), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) ≤ (↑(maxVar X Y) : ℝ)}

Tactic:
have I6 : ∀ x y, IsClosed { f : Cb X Y | f (x, y) ≤ maxVar X Y } := fun x y =>
    isClosed_le (continuous_eval_const _) continuous_const
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
I1 : ∀ (x y : X), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inl y) = dist x y}
I2 : ∀ (x y : Y), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inr x, inr y) = dist x y}
I3 :
  ∀ (x y : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, x) : ℝ)}
I4 :
  ∀ (x y z : X ⊕ Y),
    IsClosed (X := Cb X Y)
      {f : Cb X Y |
        (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, z) ≤
          HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ)
            ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, z) : ℝ)}
I5 :
  ∀ (x : X ⊕ Y),
    IsClosed (X := Cb X Y) {f : Cb X Y | Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, x) : ℝ) (0 : ℝ)}
I6 :
  ∀ (x y : X ⊕ Y), IsClosed (X := Cb X Y) {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) ≤ (↑(maxVar X Y) : ℝ)}
x : Cb X Y
⊢ Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) x ↔
    Membership.mem (γ := Set (Cb X Y))
      ((((((⋂ (x : X), ⋂ (y : X), {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inl y) = dist x y}) ∩
                ⋂ (x : Y), ⋂ (y : Y), {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inr x, inr y) = dist x y}) ∩
              ⋂ (x : X ⊕ Y),
                ⋂ (y : X ⊕ Y),
                  {f : Cb X Y |
                    Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ)
                      ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, x) : ℝ)}) ∩
            ⋂ (x : X ⊕ Y),
              ⋂ (y : X ⊕ Y),
                ⋂ (z : X ⊕ Y),
                  {f : Cb X Y |
                    (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, z) ≤
                      HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) : ℝ)
                        ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (y, z) : ℝ)}) ∩
          ⋂ (x : X ⊕ Y), {f : Cb X Y | Eq (α := ℝ) ((f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, x) : ℝ) (0 : ℝ)}) ∩
        ⋂ (x : X ⊕ Y), ⋂ (y : X ⊕ Y), {f : Cb X Y | (f : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (x, y) ≤ (↑(maxVar X Y) : ℝ)})
      x

Tactic:
simp only [candidatesB, candidates, mem_inter_iff, mem_iInter, mem_setOf_eq]

Premises used: Set.mem_inter_iff, GromovHausdorff.candidates, _private.0.GromovHausdorff.candidatesB, Set.mem_setOf_eq, Set.mem_iInter