-- Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
theorem candidates_dist_bound (fA : f ∈ candidates X Y) :
    ∀ {x y : X ⊕ Y}, f (x, y) ≤ maxVar X Y * dist x y
  | inl x, inl y =>
    calc
      f (inl x, inl y) = dist x y := candidates_dist_inl fA x y
      _ = dist (α := X ⊕ Y) (inl x) (inl y)

Proof state:
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
⊢ 1 * dist (inl x) (inl y) ≤ ↑(GromovHausdorff.maxVar X Y) * dist (inl x) (inl y)

Tactic:
gcongr

Result:
case h
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
⊢ 1 ≤ ↑(GromovHausdorff.maxVar X Y)

Proof state:
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
⊢ dist x y = Sum.dist (inl x) (inl y)

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ dist x y = Sum.dist (inr x) (inr y)

Tactic:
rfl

Result:
no goals

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

Tactic:
gcongr

Result:
case h
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ 1 ≤ ↑(GromovHausdorff.maxVar X Y)

Proof state:
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
⊢ dist x y = dist (inl x) (inl y)

Tactic:
rw [@Sum.dist_eq X Y]

Result:
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
⊢ dist x y = Sum.dist (inl x) (inl y)

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ dist (inr x) (inr y) = 1 * dist (inr x) (inr y)

Tactic:
ring

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ dist x y = dist (inr x) (inr y)

Tactic:
rw [@Sum.dist_eq X Y]

Result:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ dist x y = Sum.dist (inr x) (inr y)

Proof state:
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
⊢ dist (inl x) (inl y) = 1 * dist (inl x) (inl y)

Tactic:
ring

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : Y
y : X
⊢ ↑(GromovHausdorff.maxVar X Y) * 1 ≤ ↑(GromovHausdorff.maxVar X Y) * dist (inl x) (inr y)

Tactic:
gcongr

Result:
case h
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : Y
y : X
⊢ 1 ≤ dist (inl x) (inr y)

Proof state:
case h
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y : Y
⊢ 1 ≤ ↑(GromovHausdorff.maxVar X Y)

Tactic:
exact one_le_maxVar X Y

Result:
no goals

Proof state:
case h
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.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

Result:
no goals

Proof state:
case h
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.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

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : X
y : Y
⊢ ↑(GromovHausdorff.maxVar X Y) = ↑(GromovHausdorff.maxVar X Y) * 1

Tactic:
simp

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : X
y : Y
⊢ ↑(GromovHausdorff.maxVar X Y) * 1 ≤ ↑(GromovHausdorff.maxVar X Y) * dist (inl x) (inr y)

Tactic:
gcongr

Result:
case h
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : X
y : Y
⊢ 1 ≤ dist (inl x) (inr y)

Proof state:
case h
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
⊢ 1 ≤ ↑(GromovHausdorff.maxVar X Y)

Tactic:
exact one_le_maxVar X Y

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : GromovHausdorff.ProdSpaceFun X Y
fA : f ∈ candidates X Y
x : Y
y : X
⊢ ↑(GromovHausdorff.maxVar X Y) = ↑(GromovHausdorff.maxVar X Y) * 1

Tactic:
simp

Result:
no goals