case intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
left✝ :
  choose
      (_ :
        ∃ f,
          f ∈ GromovHausdorff.candidatesB X Y ∧
            ∀ (g : GromovHausdorff.Cb X Y), g ∈ GromovHausdorff.candidatesB X Y → HD f ≤ HD g) ∈
    GromovHausdorff.candidatesB X Y
right✝ :
  ∀ (g : GromovHausdorff.Cb X Y),
    g ∈ GromovHausdorff.candidatesB X Y →
      HD
          (choose
            (_ :
              ∃ f,
                f ∈ GromovHausdorff.candidatesB X Y ∧
                  ∀ (g : GromovHausdorff.Cb X Y), g ∈ GromovHausdorff.candidatesB X Y → HD f ≤ HD g)) ≤
        HD g
⊢ GromovHausdorff.optimalGHDist X Y ∈ GromovHausdorff.candidatesB X Y
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
⊢ GromovHausdorff.optimalGHDist X Y ∈ GromovHausdorff.candidatesB X Y
cases Classical.choose_spec (exists_minimizer X Y)
no goals
case intro
X : Type u
Y : Type v
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
left✝ :
  choose
      (_ :
        ∃ f,
          f ∈ GromovHausdorff.candidatesB X Y ∧
            ∀ (g : GromovHausdorff.Cb X Y), g ∈ GromovHausdorff.candidatesB X Y → HD f ≤ HD g) ∈
    GromovHausdorff.candidatesB X Y
right✝ :
  ∀ (g : GromovHausdorff.Cb X Y),
    g ∈ GromovHausdorff.candidatesB X Y →
      HD
          (choose
            (_ :
              ∃ f,
                f ∈ GromovHausdorff.candidatesB X Y ∧
                  ∀ (g : GromovHausdorff.Cb X Y), g ∈ GromovHausdorff.candidatesB X Y → HD f ≤ HD g)) ≤
        HD g
⊢ GromovHausdorff.optimalGHDist X Y ∈ GromovHausdorff.candidatesB X Y
assumption