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
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
refine_2 : Tendsto (β := ℝ) (fun (t : ℝ) ↦ 2 * (↑(maxVar X Y) : ℝ) * t) (𝓝 0) (𝓝 0)
refine_2₁ :
  ∀ (x y : (X ⊕ Y) × (X ⊕ Y)) (i : (↑(candidatesB X Y) : Type (max u v))),
    dist (α := ℝ) (((↑i : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) x : ℝ)
        (((↑i : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) y : ℝ) ≤
      (fun (t : ℝ) ↦ 2 * (↑(maxVar X Y) : ℝ) * t) (dist x y)
⊢ Equicontinuous (X := (X ⊕ Y) × (X ⊕ Y)) (α := ℝ) fun (x : (↑(candidatesB X Y) : Type (max u v))) ↦
    (⇑(↑x : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ)

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

Premises used: HMul.hMul, Metric.equicontinuous_of_continuity_modulus, OfNat.ofNat, _private.0.GromovHausdorff.maxVar, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
⊢ Tendsto (fun (t : ℝ) ↦ 2 * (↑(maxVar X Y) : ℝ) * t) (𝓝 0) (𝓝 (2 * (↑(maxVar X Y) : ℝ) * 0))

Tactic:
have : Tendsto (fun t : ℝ => 2 * (maxVar X Y : ℝ) * t) (𝓝 0) (𝓝 (2 * maxVar X Y * 0)) :=
        tendsto_const_nhds.mul tendsto_id
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
this : Tendsto (fun (t : ℝ) ↦ 2 * (↑(maxVar X Y) : ℝ) * t) (𝓝 0) (𝓝 (2 * (↑(maxVar X Y) : ℝ) * 0))
⊢ Tendsto (β := ℝ) (fun (t : ℝ) ↦ 2 * (↑(maxVar X Y) : ℝ) * t) (𝓝 0) (𝓝 0)

Tactic:
simpa using this
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
x y : (X ⊕ Y) × (X ⊕ Y)
f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ
hf : Membership.mem (γ := Set ((X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ)) (candidatesB X Y) f
⊢ dist (α := ℝ)
      (((↑(Subtype.mk (p := fun (x : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) ↦
                  Membership.mem (γ := Set ((X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ)) (candidatesB X Y) x) f hf) :
              (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) :
            (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ)
          x :
        ℝ)
      (((↑(Subtype.mk (p := fun (x : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) ↦
                  Membership.mem (γ := Set ((X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ)) (candidatesB X Y) x) f hf) :
              (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) :
            (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ)
          y :
        ℝ) ≤
    (fun (t : ℝ) ↦ 2 * (↑(maxVar X Y) : ℝ) * t) (dist x y)

Tactic:
(candidates_lipschitz hf).dist_le_mul _ _

Premises used: LipschitzWith.dist_le_mul, _private.0.GromovHausdorff.candidates_lipschitz, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
x y : (X ⊕ Y) × (X ⊕ Y)
f : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ
hf : Membership.mem (γ := Set ((X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ)) (candidatesB X Y) f
⊢ dist (α := ℝ)
      (((↑(Subtype.mk (p := fun (x : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) ↦
                  Membership.mem (γ := Set ((X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ)) (candidatesB X Y) x) f hf) :
              (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) :
            (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ)
          x :
        ℝ)
      (((↑(Subtype.mk (p := fun (x : (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) ↦
                  Membership.mem (γ := Set ((X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ)) (candidatesB X Y) x) f hf) :
              (X ⊕ Y) × (X ⊕ Y) →ᵇ ℝ) :
            (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ)
          y :
        ℝ) ≤
    (fun (t : ℝ) ↦ 2 * (↑(maxVar X Y) : ℝ) * t) (dist x y)

Tactic:
exact (candidates_lipschitz hf).dist_le_mul _ _

Premises used: LipschitzWith.dist_le_mul, _private.0.GromovHausdorff.candidates_lipschitz
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
⊢ Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) (candidatesBOfCandidates f fA)

Tactic:
fA

Premises used: Set.Mem, setOf, GromovHausdorff.candidates, _private.0.GromovHausdorff.candidatesB
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
simp_rw :
  (∀ (x y : X), dist (α := X ⊕ Y) (inl x) (inl y) = dist x y) ∧
    ∀ (x y : Y), dist (α := X ⊕ Y) (inr x) (inr y) = dist x y
⊢ (fun (p : (X ⊕ Y) × (X ⊕ Y)) ↦ dist p.1 p.2) ∈ candidates X Y

Tactic:
simp_rw [candidates, Set.mem_setOf_eq, dist_comm, dist_triangle, dist_self, maxVar_bound,
    forall_const, and_true]

Premises used: dist_triangle, _private.0.GromovHausdorff.maxVar_bound, and_true, GromovHausdorff.candidates, dist_comm, Set.mem_setOf_eq, dist_self, forall_const
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
⊢ (∀ (x y : X), dist (α := X ⊕ Y) (inl x) (inl y) = dist x y) ∧
    ∀ (x y : Y), dist (α := X ⊕ Y) (inr x) (inr y) = dist x y

Tactic:
⟨fun x y => rfl, fun x y => rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
⊢ (∀ (x y : X), dist (α := X ⊕ Y) (inl x) (inl y) = dist x y) ∧
    ∀ (x y : Y), dist (α := X ⊕ Y) (inr x) (inr y) = dist x y

Tactic:
exact ⟨fun x y => rfl, fun x y => rfl⟩
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
⊢ Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) (candidatesBDist X Y)

Tactic:
candidatesBOfCandidates_mem _ _

Premises used: GromovHausdorff.candidatesBOfCandidates_mem, GromovHausdorff.candidatesBDist, BoundedContinuousFunction.mkOfCompact
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
⊢ Set.Nonempty (α := Cb X Y) (candidatesB X Y)

Tactic:
⟨_, candidatesBDist_mem_candidatesB⟩

Premises used: Set.Nonempty, GromovHausdorff.candidatesBDist_mem_candidatesB, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
⊢ HD (candidatesBDist X Y) ≤ diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ

Tactic:
max_le (ciSup_le fun x => ?_) (ciSup_le fun y => ?_)

Premises used: max_le, GromovHausdorff.HD, ciSup_le
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
refine_1 :
  ∀ (x : X),
    ⨅ (y : Y), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤
      diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
refine_2 :
  ∀ (y : Y),
    ⨅ (x : X), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤
      diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
⊢ HD (candidatesBDist X Y) ≤ diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ

Tactic:
refine max_le (ciSup_le fun x => ?_) (ciSup_le fun y => ?_)

Premises used: max_le
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
x : X
⊢ BddBelow (α := ℝ) (range fun (y : Y) ↦ (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))

Tactic:
simpa using HD_below_aux1 0

Premises used: OfNat.ofNat, GromovHausdorff.HD_below_aux1
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
x : X
⊢ LE.le (α := ℝ) (⨅ (y : Y), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ)
    ((candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr default) : ℝ)

Tactic:
have A : ⨅ y, candidatesBDist X Y (inl x, inr y) ≤ candidatesBDist X Y (inl x, inr default) :=
      ciInf_le (by simpa using HD_below_aux1 0) default
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
x : X
A :
  LE.le (α := ℝ) (⨅ (y : Y), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ)
    ((candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr default) : ℝ)
h₁ : dist x default ≤ diam.{u} (α := X) univ
h₂ : dist.{v} (α := Y) default default ≤ diam.{v} (α := Y) univ
⊢ dist x default + 1 + dist.{v} (α := Y) default default ≤ diam.{u} (α := X) univ + 1 + 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
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
x : X
A :
  LE.le (α := ℝ) (⨅ (y : Y), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ)
    ((candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr default) : ℝ)
⊢ dist x default ≤ diam.{u} (α := X) univ

Tactic:
dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)

Premises used: Metric.isBounded_of_compactSpace, Metric.dist_le_diam_of_mem, Set.mem_univ
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
x : X
A :
  LE.le (α := ℝ) (⨅ (y : Y), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ)
    ((candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr default) : ℝ)
⊢ dist x default ≤ diam.{u} (α := X) univ

Tactic:
exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)

Premises used: Metric.isBounded_of_compactSpace, Metric.dist_le_diam_of_mem, Set.mem_univ
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
x : X
A :
  LE.le (α := ℝ) (⨅ (y : Y), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ)
    ((candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr default) : ℝ)
⊢ dist.{v} (α := Y) default default ≤ diam.{v} (α := Y) univ

Tactic:
dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)

Premises used: Metric.isBounded_of_compactSpace, Metric.dist_le_diam_of_mem, Set.mem_univ
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
x : X
A :
  LE.le (α := ℝ) (⨅ (y : Y), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ)
    ((candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr default) : ℝ)
⊢ dist.{v} (α := Y) default default ≤ diam.{v} (α := Y) univ

Tactic:
exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)

Premises used: Metric.isBounded_of_compactSpace, Metric.dist_le_diam_of_mem, Set.mem_univ
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
x : X
A :
  LE.le (α := ℝ) (⨅ (y : Y), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ)
    ((candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr default) : ℝ)
⊢ dist (α := X ⊕ Y) (inl x) (inr default) ≤ diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ

Tactic:
have B : dist (inl x) (inr default) ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) :=
      calc
        dist (inl x) (inr (default : Y)) = dist x (default : X) + 1 + dist default default := rfl
        _ ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := by
          gcongr <;>
            exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
x : X
A :
  LE.le (α := ℝ) (⨅ (y : Y), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ)
    ((candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr default) : ℝ)
B : dist (α := X ⊕ Y) (inl x) (inr default) ≤ diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
⊢ ⨅ (y : Y), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ

Tactic:
le_trans A B

Premises used: Unit.unit, sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, Function.const, Lean.Name, OfNat.ofNat, le_trans
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
x : X
A :
  LE.le (α := ℝ) (⨅ (y : Y), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ)
    ((candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr default) : ℝ)
B : dist (α := X ⊕ Y) (inl x) (inr default) ≤ diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
⊢ ⨅ (y : Y), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ

Tactic:
exact le_trans A B

Premises used: le_trans
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
y : Y
⊢ BddBelow (α := ℝ) (range fun (x : X) ↦ (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))

Tactic:
simpa using HD_below_aux2 0

Premises used: GromovHausdorff.HD_below_aux2, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
y : Y
⊢ LE.le (α := ℝ) (⨅ (x : X), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ)
    ((candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl default, inr y) : ℝ)

Tactic:
have A : ⨅ x, candidatesBDist X Y (inl x, inr y) ≤ candidatesBDist X Y (inl default, inr y) :=
      ciInf_le (by simpa using HD_below_aux2 0) default
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
y : Y
A :
  LE.le (α := ℝ) (⨅ (x : X), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ)
    ((candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl default, inr y) : ℝ)
h₁ : dist.{u} (α := X) default default ≤ diam.{u} (α := X) univ
h₂ : dist default y ≤ diam.{v} (α := Y) univ
⊢ dist.{u} (α := X) default default + 1 + dist default y ≤ diam.{u} (α := X) univ + 1 + 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
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
y : Y
A :
  LE.le (α := ℝ) (⨅ (x : X), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ)
    ((candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl default, inr y) : ℝ)
⊢ dist.{u} (α := X) default default ≤ diam.{u} (α := X) univ

Tactic:
dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)

Premises used: Metric.isBounded_of_compactSpace, Metric.dist_le_diam_of_mem, Set.mem_univ
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
y : Y
A :
  LE.le (α := ℝ) (⨅ (x : X), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ)
    ((candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl default, inr y) : ℝ)
⊢ dist.{u} (α := X) default default ≤ diam.{u} (α := X) univ

Tactic:
exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)

Premises used: Metric.isBounded_of_compactSpace, Metric.dist_le_diam_of_mem, Set.mem_univ
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
y : Y
A :
  LE.le (α := ℝ) (⨅ (x : X), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ)
    ((candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl default, inr y) : ℝ)
⊢ dist default y ≤ diam.{v} (α := Y) univ

Tactic:
dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)

Premises used: Metric.isBounded_of_compactSpace, Metric.dist_le_diam_of_mem, Set.mem_univ
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
y : Y
A :
  LE.le (α := ℝ) (⨅ (x : X), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ)
    ((candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl default, inr y) : ℝ)
⊢ dist default y ≤ diam.{v} (α := Y) univ

Tactic:
exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)

Premises used: Metric.isBounded_of_compactSpace, Metric.dist_le_diam_of_mem, Set.mem_univ
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
y : Y
A :
  LE.le (α := ℝ) (⨅ (x : X), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ)
    ((candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl default, inr y) : ℝ)
⊢ dist (α := X ⊕ Y) (inl default) (inr y) ≤ diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ

Tactic:
have B : dist (inl default) (inr y) ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) :=
      calc
        dist (inl (default : X)) (inr y) = dist default default + 1 + dist default y := rfl
        _ ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := by
          gcongr <;>
            exact dist_le_diam_of_mem isBounded_of_compactSpace (mem_univ _) (mem_univ _)
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
y : Y
A :
  LE.le (α := ℝ) (⨅ (x : X), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ)
    ((candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl default, inr y) : ℝ)
B : dist (α := X ⊕ Y) (inl default) (inr y) ≤ diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
⊢ ⨅ (x : X), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ

Tactic:
le_trans A B

Premises used: Unit.unit, sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, Function.const, Lean.Name, OfNat.ofNat, le_trans
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : MetricSpace Y
inst_2 : CompactSpace X
inst_3 : CompactSpace Y
inst_4 : Nonempty X
inst_5 : Nonempty Y
y : Y
A :
  LE.le (α := ℝ) (⨅ (x : X), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) : ℝ)
    ((candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl default, inr y) : ℝ)
B : dist (α := X ⊕ Y) (inl default) (inr y) ≤ diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
⊢ ⨅ (x : X), (candidatesBDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) ≤
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ

Tactic:
exact le_trans A B

Premises used: le_trans
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
⊢ ∃ (f : Cb X Y),
    Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f ∧
      ∀ (g : Cb X Y), Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) g → HD f ≤ HD g

Tactic:
isCompact_candidatesB.exists_isMinOn candidatesB_nonempty HD_continuous.continuousOn

Premises used: Continuous.continuousOn, _private.0.GromovHausdorff.candidatesB_nonempty, Set.Mem, _private.0.GromovHausdorff.HD_continuous, Filter.Eventually, setOf, IsMinFilter, IsMinOn, Set.Subset, IsCompact.exists_isMinOn, _private.0.GromovHausdorff.isCompact_candidatesB
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
⊢ Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y)
    (Classical.choose (p := fun (x : Cb X Y) ↦
      Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) x ∧
        ∀ (g : Cb X Y), Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) g → HD x ≤ HD g)
      ⋯)

Tactic:
cases Classical.choose_spec (exists_minimizer X Y)

Premises used: _private.0.GromovHausdorff.exists_minimizer, Classical.choose_spec
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized
Goal:
X : Type u
Y : Type v
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
left :
  Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y)
    (Classical.choose (p := fun (x : Cb X Y) ↦
      Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) x ∧
        ∀ (g : Cb X Y), Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) g → HD x ≤ HD g)
      ⋯)
⊢ ∀ (g : Cb X Y),
    Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) g →
      HD
          (Classical.choose (p := fun (x : Cb X Y) ↦
            Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) x ∧
              ∀ (g : Cb X Y), Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) g → HD x ≤ HD g)
            ⋯) ≤
        HD g

Tactic:
cases Classical.choose_spec (exists_minimizer X Y)

Premises used: _private.0.GromovHausdorff.exists_minimizer, Classical.choose_spec