case refine'_1
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
⊢ ∀ (f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) (x : (X ⊕ Y) × (X ⊕ Y)),
    f ∈ GromovHausdorff.candidatesB X Y → ↑f x ∈ Icc 0 ↑(GromovHausdorff.maxVar X Y)

case refine'_2
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
⊢ Equicontinuous fun x => ↑↑x
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
⊢ IsCompact (GromovHausdorff.candidatesB X Y)
refine' arzela_ascoli₂
    (Icc 0 (maxVar X Y) : Set ℝ) isCompact_Icc (candidatesB X Y) closed_candidatesB _ _
case refine'_1.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
f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ
x1 x2 : X ⊕ Y
hf : f ∈ GromovHausdorff.candidatesB X Y
⊢ ↑f (x1, x2) ∈ Icc 0 ↑(GromovHausdorff.maxVar X Y)
case refine'_1
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
⊢ ∀ (f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) (x : (X ⊕ Y) × (X ⊕ Y)),
    f ∈ GromovHausdorff.candidatesB X Y → ↑f x ∈ Icc 0 ↑(GromovHausdorff.maxVar X Y)
rintro f ⟨x1, x2⟩ hf
case refine'_1.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
f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ
x1 x2 : X ⊕ Y
hf : f ∈ GromovHausdorff.candidatesB X Y
⊢ 0 ≤ ↑f (x1, x2) ∧ ↑f (x1, x2) ≤ ↑(GromovHausdorff.maxVar X Y)
case refine'_1.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
f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ
x1 x2 : X ⊕ Y
hf : f ∈ GromovHausdorff.candidatesB X Y
⊢ ↑f (x1, x2) ∈ Icc 0 ↑(GromovHausdorff.maxVar X Y)
simp only [Set.mem_Icc]
no goals
case refine'_1.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
f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ
x1 x2 : X ⊕ Y
hf : f ∈ GromovHausdorff.candidatesB X Y
⊢ 0 ≤ ↑f (x1, x2) ∧ ↑f (x1, x2) ≤ ↑(GromovHausdorff.maxVar X Y)
exact ⟨candidates_nonneg hf, candidates_le_maxVar hf⟩
case refine'_2.refine'_1
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
⊢ Tendsto (fun t => 2 * ↑(GromovHausdorff.maxVar X Y) * t) (𝓝 0) (𝓝 0)

case refine'_2.refine'_2
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
⊢ ∀ (x y : (X ⊕ Y) × (X ⊕ Y)) (i : ↑(GromovHausdorff.candidatesB X Y)),
    dist (↑↑i x) (↑↑i y) ≤ (fun t => 2 * ↑(GromovHausdorff.maxVar X Y) * t) (dist x y)
case refine'_2
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
⊢ Equicontinuous fun x => ↑↑x
refine' equicontinuous_of_continuity_modulus (fun t => 2 * maxVar X Y * t) _ _ _
case refine'_2.refine'_1
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
this : Tendsto (fun t => 2 * ↑(GromovHausdorff.maxVar X Y) * t) (𝓝 0) (𝓝 (2 * ↑(GromovHausdorff.maxVar X Y) * 0))
⊢ Tendsto (fun t => 2 * ↑(GromovHausdorff.maxVar X Y) * t) (𝓝 0) (𝓝 0)
case refine'_2.refine'_1
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
⊢ Tendsto (fun t => 2 * ↑(GromovHausdorff.maxVar X Y) * t) (𝓝 0) (𝓝 0)
have : Tendsto (fun t : ℝ => 2 * (maxVar X Y : ℝ) * t) (𝓝 0) (𝓝 (2 * maxVar X Y * 0)) :=
  tendsto_const_nhds.mul tendsto_id
no goals
case refine'_2.refine'_1
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
this : Tendsto (fun t => 2 * ↑(GromovHausdorff.maxVar X Y) * t) (𝓝 0) (𝓝 (2 * ↑(GromovHausdorff.maxVar X Y) * 0))
⊢ Tendsto (fun t => 2 * ↑(GromovHausdorff.maxVar X Y) * t) (𝓝 0) (𝓝 0)
simpa using this
case refine'_2.refine'_2.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
x y : (X ⊕ Y) × (X ⊕ Y)
f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ
hf : f ∈ GromovHausdorff.candidatesB X Y
⊢ dist (↑↑{ val := f, property := hf } x) (↑↑{ val := f, property := hf } y) ≤
    (fun t => 2 * ↑(GromovHausdorff.maxVar X Y) * t) (dist x y)
case refine'_2.refine'_2
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
⊢ ∀ (x y : (X ⊕ Y) × (X ⊕ Y)) (i : ↑(GromovHausdorff.candidatesB X Y)),
    dist (↑↑i x) (↑↑i y) ≤ (fun t => 2 * ↑(GromovHausdorff.maxVar X Y) * t) (dist x y)
rintro x y ⟨f, hf⟩
no goals
case refine'_2.refine'_2.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
x y : (X ⊕ Y) × (X ⊕ Y)
f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ
hf : f ∈ GromovHausdorff.candidatesB X Y
⊢ dist (↑↑{ val := f, property := hf } x) (↑↑{ val := f, property := hf } y) ≤
    (fun t => 2 * ↑(GromovHausdorff.maxVar X Y) * t) (dist x y)
exact (candidates_lipschitz hf).dist_le_mul _ _