awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
      ⋯)
right :
  ∀ (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
⊢ Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) (optimalGHDist X Y)

Tactic:
assumption
-- 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
g : Cb X Y
hg : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) g
⊢ HD (optimalGHDist X Y) ≤ HD g

Tactic:
let ⟨_, Z2⟩ := Classical.choose_spec (exists_minimizer X Y)
  Z2 g hg

Premises used: _private.0.GromovHausdorff.exists_minimizer, LE.le, _private.0.GromovHausdorff.optimalGHDist, Classical.choose_spec, _private.0.GromovHausdorff.HD_optimalGHDist_le.match_1, GromovHausdorff.HD
-- 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
⊢ Isometry (β := OptimalGHCoupling X Y) (optimalGHInjl X Y)

Tactic:
Isometry.of_dist_eq fun _ _ => candidates_dist_inl (optimalGHDist_mem_candidatesB X Y) _ _

Premises used: Isometry.of_dist_eq, _private.0.GromovHausdorff.optimalGHDist_mem_candidatesB, _private.0.GromovHausdorff.candidates_dist_inl
-- 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
⊢ Isometry (β := OptimalGHCoupling X Y) (optimalGHInjr X Y)

Tactic:
Isometry.of_dist_eq fun _ _ => candidates_dist_inr (optimalGHDist_mem_candidatesB X Y) _ _

Premises used: Isometry.of_dist_eq, _private.0.GromovHausdorff.optimalGHDist_mem_candidatesB, _private.0.GromovHausdorff.candidates_dist_inr
-- 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
rw : IsCompact (X := OptimalGHCoupling X Y) (range Quotient.mk')
⊢ IsCompact (X := OptimalGHCoupling X Y) univ

Tactic:
rw [← range_quotient_mk']

Premises used: Set.range_quotient_mk'
-- 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
⊢ IsCompact (X := OptimalGHCoupling X Y) (range Quotient.mk')

Tactic:
isCompact_range (continuous_sum_dom.2
    ⟨(isometry_optimalGHInjl X Y).continuous, (isometry_optimalGHInjr X Y).continuous⟩)

Premises used: Iff.mpr, GromovHausdorff.isometry_optimalGHInjr, Isometry.continuous, isCompact_range, And.intro, SeparationQuotient, continuous_sum_dom, GromovHausdorff.isometry_optimalGHInjl, GromovHausdorff.OptimalGHCoupling
-- 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
⊢ IsCompact (X := OptimalGHCoupling X Y) (range Quotient.mk')

Tactic:
exact isCompact_range (continuous_sum_dom.2
    ⟨(isometry_optimalGHInjl X Y).continuous, (isometry_optimalGHInjr X Y).continuous⟩)

Premises used: Iff.mpr, GromovHausdorff.isometry_optimalGHInjr, Isometry.continuous, isCompact_range, And.intro, continuous_sum_dom, GromovHausdorff.isometry_optimalGHInjl
-- 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD f

Tactic:
le_trans (le_of_forall_gt_imp_ge_of_dense fun r hr => ?_) (HD_optimalGHDist_le X Y f h)

Premises used: le_of_forall_gt_imp_ge_of_dense, _private.0.GromovHausdorff.HD_optimalGHDist_le, 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
refine :
  ∀ (r : ℝ) (hr : HD (optimalGHDist X Y) < r),
    hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ r
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD f

Tactic:
refine le_trans (le_of_forall_gt_imp_ge_of_dense fun r hr => ?_) (HD_optimalGHDist_le X Y f h)

Premises used: le_of_forall_gt_imp_ge_of_dense, _private.0.GromovHausdorff.HD_optimalGHDist_le, 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
z : X
⊢ ⨆ (x : X), ⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) < r

Tactic:
have I1 : (⨆ x, ⨅ y, optimalGHDist X Y (inl x, inr y)) < r :=
      lt_of_le_of_lt (le_max_left _ _) hr
-- 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
z : X
I1 : ⨆ (x : X), ⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) < r
⊢ BddAbove (α := ℝ) (range fun (x : X) ↦ ⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))

Tactic:
simpa using HD_bound_aux1 _ 0

Premises used: _private.0.GromovHausdorff.HD_bound_aux1, OfNat.ofNat
-- 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
z : X
I1 : ⨆ (x : X), ⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) < r
⊢ LE.le (α := ℝ) (⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl z, inr y))
    (⨆ (x : X), ⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))

Tactic:
have I2 :
        ⨅ y, optimalGHDist X Y (inl z, inr y) ≤ ⨆ x, ⨅ y, optimalGHDist X Y (inl x, inr y) :=
      le_csSup (by simpa using HD_bound_aux1 _ 0) (mem_range_self _)
-- 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
z : X
I1 : ⨆ (x : X), ⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) < r
I2 :
  LE.le (α := ℝ) (⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl z, inr y))
    (⨆ (x : X), ⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
⊢ ⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl z, inr y) < r

Tactic:
have I : ⨅ y, optimalGHDist X Y (inl z, inr y) < r := lt_of_le_of_lt I2 I1
-- 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
z : X
I1 : ⨆ (x : X), ⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) < r
I2 :
  LE.le (α := ℝ) (⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl z, inr y))
    (⨆ (x : X), ⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
I : ⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl z, inr y) < r
rcases :
  ∀ (z' : Y) (hr' : (fun (y : Y) ↦ ((optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl z, inr y) : ℝ)) z' < r),
    ∃ (y : OptimalGHCoupling X Y),
      Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist (optimalGHInjl X Y z) y ≤ r
⊢ ∃ (y : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist (optimalGHInjl X Y z) y ≤ r

Tactic:
rcases exists_lt_of_csInf_lt (range_nonempty _) I with ⟨r', ⟨z', rfl⟩, hr'⟩

Premises used: Set.range_nonempty, rfl, exists_lt_of_csInf_lt
-- 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
z : X
I1 : ⨆ (x : X), ⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) < r
I2 :
  LE.le (α := ℝ) (⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl z, inr y))
    (⨆ (x : X), ⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
I : ⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl z, inr y) < r
z' : Y
hr' : (fun (y : Y) ↦ ((optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl z, inr y) : ℝ)) z' < r
⊢ ∃ (y : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist (optimalGHInjl X Y z) y ≤ r

Tactic:
⟨optimalGHInjr X Y z', mem_range_self _, le_of_lt hr'⟩

Premises used: Set.mem_range_self, le_of_lt, And.intro, Exists.intro, GromovHausdorff.optimalGHInjr
-- 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
z : X
I1 : ⨆ (x : X), ⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) < r
I2 :
  LE.le (α := ℝ) (⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl z, inr y))
    (⨆ (x : X), ⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
I : ⨅ (y : Y), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl z, inr y) < r
z' : Y
hr' : (fun (y : Y) ↦ ((optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl z, inr y) : ℝ)) z' < r
⊢ ∃ (y : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist (optimalGHInjl X Y z) y ≤ r

Tactic:
exact ⟨optimalGHInjr X Y z', mem_range_self _, le_of_lt hr'⟩
-- 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
⊢ ∀ (x : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) x →
      ∃ (y : OptimalGHCoupling X Y),
        Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist x y ≤ r

Tactic:
have A : ∀ x ∈ range (optimalGHInjl X Y), ∃ y ∈ range (optimalGHInjr X Y), dist x y ≤ r := by
    rintro _ ⟨z, rfl⟩
    have I1 : (⨆ x, ⨅ y, optimalGHDist X Y (inl x, inr y)) < r :=
      lt_of_le_of_lt (le_max_left _ _) hr
    have I2 :
        ⨅ y, optimalGHDist X Y (inl z, inr y) ≤ ⨆ x, ⨅ y, optimalGHDist X Y (inl x, inr y) :=
      le_csSup (by simpa using HD_bound_aux1 _ 0) (mem_range_self _)
    have I : ⨅ y, optimalGHDist X Y (inl z, inr y) < r := lt_of_le_of_lt I2 I1
    rcases exists_lt_of_csInf_lt (range_nonempty _) I with ⟨r', ⟨z', rfl⟩, hr'⟩
    exact ⟨optimalGHInjr X Y z', mem_range_self _, le_of_lt hr'⟩
-- 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
A :
  ∀ (x : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) x →
      ∃ (y : OptimalGHCoupling X Y),
        Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist x y ≤ r
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ r

Tactic:
hausdorffDist_le_of_mem_dist ?_ A ?_

Premises used: Metric.hausdorffDist_le_of_mem_dist
-- 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
A :
  ∀ (x : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) x →
      ∃ (y : OptimalGHCoupling X Y),
        Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist x y ≤ r
refine_1 : 0 ≤ r
refine_2 :
  ∀ (x : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) x →
      ∃ (y : OptimalGHCoupling X Y),
        Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) y ∧ dist x y ≤ r
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ r

Tactic:
refine hausdorffDist_le_of_mem_dist ?_ A ?_

Premises used: Metric.hausdorffDist_le_of_mem_dist
-- 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
A :
  ∀ (x : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) x →
      ∃ (y : OptimalGHCoupling X Y),
        Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist x y ≤ r
refine_1 : ∀ (inhabited_h : Inhabited X), 0 ≤ r
⊢ 0 ≤ r

Tactic:
inhabit X
-- 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
A :
  ∀ (x : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) x →
      ∃ (y : OptimalGHCoupling X Y),
        Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist x y ≤ r
inhabited_h : Inhabited X
refine_1 : ∀ (y : OptimalGHCoupling X Y) (hy : dist (optimalGHInjl X Y default) y ≤ r), 0 ≤ r
⊢ 0 ≤ r

Tactic:
rcases A _ (mem_range_self default) with ⟨y, -, hy⟩

Premises used: Set.mem_range_self, Inhabited.default
-- 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
A :
  ∀ (x : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) x →
      ∃ (y : OptimalGHCoupling X Y),
        Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist x y ≤ r
inhabited_h : Inhabited X
y : OptimalGHCoupling X Y
hy : dist (optimalGHInjl X Y default) y ≤ r
⊢ 0 ≤ r

Tactic:
le_trans dist_nonneg hy

Premises used: dist_nonneg, 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
A :
  ∀ (x : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) x →
      ∃ (y : OptimalGHCoupling X Y),
        Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist x y ≤ r
inhabited_h : Inhabited X
y : OptimalGHCoupling X Y
hy : dist (optimalGHInjl X Y default) y ≤ r
⊢ 0 ≤ r

Tactic:
exact le_trans dist_nonneg hy

Premises used: dist_nonneg, 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
A :
  ∀ (x : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) x →
      ∃ (y : OptimalGHCoupling X Y),
        Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist x y ≤ r
z : Y
⊢ ⨆ (y : Y), ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) < r

Tactic:
have I1 : (⨆ y, ⨅ x, optimalGHDist X Y (inl x, inr y)) < r :=
      lt_of_le_of_lt (le_max_right _ _) hr
-- 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
A :
  ∀ (x : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) x →
      ∃ (y : OptimalGHCoupling X Y),
        Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist x y ≤ r
z : Y
I1 : ⨆ (y : Y), ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) < r
⊢ BddAbove (α := ℝ) (range fun (y : Y) ↦ ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))

Tactic:
simpa using HD_bound_aux2 _ 0

Premises used: _private.0.GromovHausdorff.HD_bound_aux2, OfNat.ofNat
-- 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
A :
  ∀ (x : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) x →
      ∃ (y : OptimalGHCoupling X Y),
        Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist x y ≤ r
z : Y
I1 : ⨆ (y : Y), ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) < r
⊢ LE.le (α := ℝ) (⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr z))
    (⨆ (y : Y), ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))

Tactic:
have I2 :
        ⨅ x, optimalGHDist X Y (inl x, inr z) ≤ ⨆ y, ⨅ x, optimalGHDist X Y (inl x, inr y) :=
      le_csSup (by simpa using HD_bound_aux2 _ 0) (mem_range_self _)
-- 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
A :
  ∀ (x : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) x →
      ∃ (y : OptimalGHCoupling X Y),
        Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist x y ≤ r
z : Y
I1 : ⨆ (y : Y), ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) < r
I2 :
  LE.le (α := ℝ) (⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr z))
    (⨆ (y : Y), ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
⊢ ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr z) < r

Tactic:
have I : ⨅ x, optimalGHDist X Y (inl x, inr z) < r := lt_of_le_of_lt I2 I1
-- 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
h : Membership.mem (γ := Set (Cb X Y)) (candidatesB X Y) f
r : ℝ
hr : HD (optimalGHDist X Y) < r
A :
  ∀ (x : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) x →
      ∃ (y : OptimalGHCoupling X Y),
        Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjr X Y)) y ∧ dist x y ≤ r
z : Y
I1 : ⨆ (y : Y), ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y) < r
I2 :
  LE.le (α := ℝ) (⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr z))
    (⨆ (y : Y), ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr y))
I : ⨅ (x : X), (optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr z) < r
refine_2 :
  ∀ (z' : X) (hr' : (fun (x : X) ↦ ((optimalGHDist X Y : (a : (X ⊕ Y) × (X ⊕ Y)) → ℝ) (inl x, inr z) : ℝ)) z' < r),
    ∃ (y : OptimalGHCoupling X Y),
      Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) y ∧ dist (optimalGHInjr X Y z) y ≤ r
⊢ ∃ (y : OptimalGHCoupling X Y),
    Membership.mem (γ := Set (OptimalGHCoupling X Y)) (range (optimalGHInjl X Y)) y ∧ dist (optimalGHInjr X Y z) y ≤ r

Tactic:
rcases exists_lt_of_csInf_lt (range_nonempty _) I with ⟨r', ⟨z', rfl⟩, hr'⟩

Premises used: Set.range_nonempty, rfl, exists_lt_of_csInf_lt