-- Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean
theorem isCompact_candidatesB : IsCompact (candidatesB X Y)

Proof state:
case refine_1.mk
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace 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)

Tactic:
simp only [Set.mem_Icc]

Result:
case refine_1.mk
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace 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)

Proof state:
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ IsCompact (GromovHausdorff.candidatesB X Y)

Tactic:
refine arzela_ascoli₂
    (Icc 0 (maxVar X Y) : Set ℝ) isCompact_Icc (candidatesB X Y) closed_candidatesB ?_ ?_

Result:
case refine_1
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace 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✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ Equicontinuous fun x => ⇑↑x

Proof state:
case refine_2
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ Equicontinuous fun x => ⇑↑x

Tactic:
refine equicontinuous_of_continuity_modulus (fun t => 2 * maxVar X Y * t) ?_ _ ?_

Result:
case refine_2.refine_1
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace 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✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace 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)

Proof state:
case refine_2.refine_2
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace 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)

Tactic:
rintro x y ⟨f, hf⟩

Result:
case refine_2.refine_2.mk
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
x y : (X ⊕ Y) × (X ⊕ Y)
f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ
hf : f ∈ GromovHausdorff.candidatesB X Y
⊢ dist (↑⟨f, hf⟩ x) (↑⟨f, hf⟩ y) ≤ (fun t => 2 * ↑(GromovHausdorff.maxVar X Y) * t) (dist x y)

Proof state:
case refine_2.refine_1
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ Tendsto (fun t => 2 * ↑(GromovHausdorff.maxVar X Y) * t) (𝓝 0) (𝓝 0)

Tactic:
have : Tendsto (fun t : ℝ => 2 * (maxVar X Y : ℝ) * t) (𝓝 0) (𝓝 (2 * maxVar X Y * 0)) :=
  tendsto_const_nhds.mul tendsto_id

Result:
case refine_2.refine_1
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace 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)

Proof state:
case refine_1
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ ∀ (f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) (x : (X ⊕ Y) × (X ⊕ Y)),
    f ∈ GromovHausdorff.candidatesB X Y → f x ∈ Icc 0 ↑(GromovHausdorff.maxVar X Y)

Tactic:
rintro f ⟨x1, x2⟩ hf

Result:
case refine_1.mk
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace 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)

Proof state:
case refine_2.refine_2.mk
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
x y : (X ⊕ Y) × (X ⊕ Y)
f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ
hf : f ∈ GromovHausdorff.candidatesB X Y
⊢ dist (↑⟨f, hf⟩ x) (↑⟨f, hf⟩ y) ≤ (fun t => 2 * ↑(GromovHausdorff.maxVar X Y) * t) (dist x y)

Tactic:
exact (candidates_lipschitz hf).dist_le_mul _ _

Result:
no goals

Proof state:
case refine_1.mk
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace 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)

Tactic:
exact ⟨candidates_nonneg hf, candidates_le_maxVar hf⟩

Result:
no goals

Proof state:
case refine_2.refine_1
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace 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)

Tactic:
simpa using this

Result:
no goals