awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
            diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ →
          hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
          hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
refine_1 :
  hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ ghDist X Y
refine_2 :
  ghDist X Y ≤ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y))
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
            diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ →
          hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
          hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
refine_1 :
  Set.Nonempty (α := ℝ)
    ((fun (p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) × NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦
        hausdorffDist (↑p.1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑p.2 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) ''
      SProd.sprod (α := Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) (β :=
        Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)))
        {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = toGHSpace X}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = toGHSpace Y})
refine_1₁ :
  ∀ (b : ℝ),
    Membership.mem (γ := Set ℝ)
        ((fun (p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) × NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦
            hausdorffDist (↑p.1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑p.2 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) ''
          SProd.sprod (α := Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) (β :=
            Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)))
            {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = toGHSpace X}
            {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = toGHSpace Y})
        b →
      hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ b
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ ghDist X Y

Tactic:
apply le_csInf

Premises used: le_csInf
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
            diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ →
          hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
          hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ Set.Nonempty (α := ℝ)
    ((fun (p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) × NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦
        hausdorffDist (↑p.1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑p.2 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) ''
      SProd.sprod (α := Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) (β :=
        Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)))
        {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = toGHSpace X}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = toGHSpace Y})

Tactic:
(Set.Nonempty.prod ?_ ?_).image _

Premises used: Set.Nonempty.prod, Set.Nonempty.image
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
            diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ →
          hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
          hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
refine_1 :
  Set.Nonempty (α := NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
    {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = toGHSpace X}
refine_1₁ :
  Set.Nonempty (α := NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
    {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = toGHSpace Y}
⊢ Set.Nonempty (α := ℝ)
    ((fun (p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) × NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦
        hausdorffDist (↑p.1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑p.2 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) ''
      SProd.sprod (α := Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) (β :=
        Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)))
        {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = toGHSpace X}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = toGHSpace Y})

Tactic:
refine (Set.Nonempty.prod ?_ ?_).image _

Premises used: Set.Nonempty.prod, Set.Nonempty.image
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
            diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ →
          hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
          hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ Set.Nonempty (α := NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
    {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = toGHSpace X}

Tactic:
⟨_, rfl⟩

Premises used: Set.Nonempty, Exists.intro, rfl
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
            diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ →
          hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
          hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ Set.Nonempty (α := NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
    {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = toGHSpace X}

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
            diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ →
          hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
          hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ Set.Nonempty (α := NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
    {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = toGHSpace Y}

Tactic:
⟨_, rfl⟩

Premises used: Set.Nonempty, Exists.intro, rfl
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
            diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ →
          hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
          hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ Set.Nonempty (α := NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
    {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = toGHSpace Y}

Tactic:
exact ⟨_, rfl⟩
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
            diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ →
          hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
          hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp :
  Membership.mem (γ := Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)))
    {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = toGHSpace X} (p, q).1
hq :
  Membership.mem (γ := Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)))
    {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = toGHSpace Y} (p, q).2
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
    (fun (p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) × NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦
        hausdorffDist (↑p.1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑p.2 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)))
      (p, q)

Tactic:
B p q hp hq
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
            diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ →
          hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
          hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp :
  Membership.mem (γ := Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)))
    {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = toGHSpace X} (p, q).1
hq :
  Membership.mem (γ := Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)))
    {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = toGHSpace Y} (p, q).2
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
    (fun (p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) × NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦
        hausdorffDist (↑p.1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑p.2 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)))
      (p, q)

Tactic:
exact B p q hp hq
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
            diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ →
          hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
          hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ ghDist X Y ≤ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y))

Tactic:
ghDist_le_hausdorffDist (isometry_optimalGHInjl X Y) (isometry_optimalGHInjr X Y)

Premises used: GromovHausdorff.isometry_optimalGHInjr, GromovHausdorff.ghDist_le_hausdorffDist, GromovHausdorff.isometry_optimalGHInjl
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
            diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ →
          hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
          hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ ghDist X Y ≤ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y))

Tactic:
exact ghDist_le_hausdorffDist (isometry_optimalGHInjl X Y) (isometry_optimalGHInjr X Y)

Premises used: GromovHausdorff.isometry_optimalGHInjr, GromovHausdorff.ghDist_le_hausdorffDist, GromovHausdorff.isometry_optimalGHInjl
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjr X Y
⊢ ∃ (Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

Tactic:
⟨Φ, Ψ, ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjr X Y
refine_1 : Isometry Φ
refine_2 : Isometry Ψ
refine_3 : ghDist X Y = hausdorffDist (range Φ) (range Ψ)
⊢ ∃ (Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

Tactic:
refine ⟨Φ, Ψ, ?_, ?_, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjr X Y
⊢ Isometry Φ

Tactic:
(kuratowskiEmbedding.isometry _).comp (isometry_optimalGHInjl X Y)

Premises used: Isometry.comp, GromovHausdorff.isometry_optimalGHInjl, kuratowskiEmbedding.isometry
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjr X Y
⊢ Isometry Φ

Tactic:
exact (kuratowskiEmbedding.isometry _).comp (isometry_optimalGHInjl X Y)

Premises used: Isometry.comp, GromovHausdorff.isometry_optimalGHInjl, kuratowskiEmbedding.isometry
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjr X Y
⊢ Isometry Ψ

Tactic:
(kuratowskiEmbedding.isometry _).comp (isometry_optimalGHInjr X Y)

Premises used: Isometry.comp, GromovHausdorff.isometry_optimalGHInjr, kuratowskiEmbedding.isometry
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjr X Y
⊢ Isometry Ψ

Tactic:
exact (kuratowskiEmbedding.isometry _).comp (isometry_optimalGHInjr X Y)

Premises used: Isometry.comp, GromovHausdorff.isometry_optimalGHInjr, kuratowskiEmbedding.isometry
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
F : OptimalGHCoupling X Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjr X Y
refine_3 :
  hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) =
    hausdorffDist (F '' range (optimalGHInjl X Y)) (F '' range (optimalGHInjr X Y))
⊢ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

Tactic:
rw [← image_univ, ← image_univ, image_comp F, image_univ, image_comp F (optimalGHInjr X Y),
      image_univ, ← hausdorffDist_optimal]

Premises used: GromovHausdorff.hausdorffDist_optimal, Set.image_univ, Set.image_comp, GromovHausdorff.optimalGHInjr