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
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
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) =
    hausdorffDist (F '' range (optimalGHInjl X Y)) (F '' range (optimalGHInjr X Y))

Tactic:
(hausdorffDist_image (kuratowskiEmbedding.isometry _)).symm

Premises used: ENNReal.ofNNReal, Set.Mem, setOf, WithTop.some, Metric.hausdorffDist_image, Eq.symm, 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
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) =
    hausdorffDist (F '' range (optimalGHInjl X Y)) (F '' range (optimalGHInjr X Y))

Tactic:
exact (hausdorffDist_image (kuratowskiEmbedding.isometry _)).symm

Premises used: Metric.hausdorffDist_image, Eq.symm, kuratowskiEmbedding.isometry
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x : GHSpace
rcases : ∀ (y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (hy : ⟦y⟧ = x), dist x x = 0
⊢ dist x x = 0

Tactic:
rcases exists_rep x with ⟨y, hy⟩

Premises used: Quotient.exists_rep
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x : GHSpace
y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : ⟦y⟧ = x
⊢ dist x x = 0

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x : GHSpace
y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : ⟦y⟧ = x
refine_1 : dist x x ≤ 0
refine_2 : 0 ≤ dist x x
⊢ dist x x = 0

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x : GHSpace
y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : ⟦y⟧ = x
refine_1 :
  BddBelow (α := ℝ)
    ((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⟧ = x}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = x})
refine_1₁ :
  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⟧ = x}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = x})
    0
⊢ dist x x ≤ 0

Tactic:
apply csInf_le

Premises used: csInf_le
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x : GHSpace
y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : ⟦y⟧ = x
u v : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
⊢ LE.le (α := ℝ) 0
    ((fun (p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) × NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦
        hausdorffDist (↑p.1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑p.2 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)))
      (u, v))

Tactic:
hausdorffDist_nonneg

Premises used: Metric.hausdorffDist_nonneg
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x : GHSpace
y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : ⟦y⟧ = x
u v : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
⊢ LE.le (α := ℝ) 0
    ((fun (p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) × NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦
        hausdorffDist (↑p.1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑p.2 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)))
      (u, v))

Tactic:
exact hausdorffDist_nonneg

Premises used: Metric.hausdorffDist_nonneg
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x : GHSpace
y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : ⟦y⟧ = x
⊢ BddBelow (α := ℝ)
    ((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⟧ = x}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = x})

Tactic:
exact ⟨0, by rintro b ⟨⟨u, v⟩, -, rfl⟩; exact hausdorffDist_nonneg⟩
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x : GHSpace
y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : ⟦y⟧ = x
refine_1 :
  ∃ (a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    (⟦a⟧ = x ∧ ⟦b⟧ = x) ∧ hausdorffDist (↑a : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑b : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = 0
⊢ 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⟧ = x}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = x})
    0

Tactic:
simp only [mem_image, mem_prod, mem_setOf_eq, Prod.exists]

Premises used: Set.mem_image, Set.mem_setOf_eq, Set.mem_prod, Prod.exists
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x : GHSpace
y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : ⟦y⟧ = x
refine_1 :
  (⟦y⟧ = x ∧ ⟦y⟧ = x) ∧ hausdorffDist (↑y : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑y : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = 0
⊢ ∃ (a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    (⟦a⟧ = x ∧ ⟦b⟧ = x) ∧ hausdorffDist (↑a : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑b : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = 0

Tactic:
exists y, y
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x : GHSpace
y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : ⟦y⟧ = x
⊢ (⟦y⟧ = x ∧ ⟦y⟧ = x) ∧ hausdorffDist (↑y : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑y : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = 0

Tactic:
simpa only [and_self_iff, hausdorffDist_self_zero, eq_self_iff_true, and_true]

Premises used: and_true, Metric.hausdorffDist_self_zero, and_self_iff, eq_self_iff_true
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x : GHSpace
y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : ⟦y⟧ = x
refine_2 :
  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⟧ = x}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = x})
refine_2₁ :
  ∀ (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⟧ = x}
            {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = x})
        b →
      0 ≤ b
⊢ 0 ≤ dist x x

Tactic:
apply le_csInf

Premises used: le_csInf
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x : GHSpace
y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : ⟦y⟧ = x
⊢ 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⟧ = x}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = x})

Tactic:
Set.Nonempty.image _ <| Set.Nonempty.prod ⟨y, hy⟩ ⟨y, hy⟩

Premises used: Set.Nonempty.prod, Set.Nonempty.image, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x : GHSpace
y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : ⟦y⟧ = x
⊢ 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⟧ = x}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = x})

Tactic:
exact Set.Nonempty.image _ <| Set.Nonempty.prod ⟨y, hy⟩ ⟨y, hy⟩

Premises used: Set.Nonempty.prod, Set.Nonempty.image, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
h :
  ∀ (x_1 : ℝ),
    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⟧ = x}
            {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = y})
        x_1 ↔
      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 : ℕ) ↦ ℝ) ∞))) ∘
            Prod.swap ''
          SProd.sprod (α := Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) (β :=
            Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = x}
            {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = y})
        x_1
⊢ Eq (α := 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⟧ = x}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = y})
    ((fun (p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) × NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦
          hausdorffDist (↑p.1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑p.2 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) ∘
        Prod.swap ''
      SProd.sprod (α := Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) (β :=
        Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = x}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = y})

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
x_1 : ℝ
⊢ 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⟧ = x}
          {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = y})
      x_1 ↔
    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 : ℕ) ↦ ℝ) ∞))) ∘
          Prod.swap ''
        SProd.sprod (α := Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) (β :=
          Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = x}
          {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = y})
      x_1

Tactic:
simp only [comp_apply, Prod.fst_swap, Prod.snd_swap, hausdorffDist_comm]

Premises used: Prod.fst_swap, Metric.hausdorffDist_comm, Prod.snd_swap, Function.comp_apply
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
⊢ Eq (α := 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⟧ = x}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = y})
    ((fun (p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) × NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦
          hausdorffDist (↑p.1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑p.2 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) ∘
        Prod.swap ''
      SProd.sprod (α := Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) (β :=
        Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = x}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = y})

Tactic:
have A :
      (fun p : NonemptyCompacts ℓ_infty_ℝ × NonemptyCompacts ℓ_infty_ℝ =>
            hausdorffDist (p.1 : Set ℓ_infty_ℝ) p.2) ''
          { a | ⟦a⟧ = x } ×ˢ { b | ⟦b⟧ = y } =
        (fun p : NonemptyCompacts ℓ_infty_ℝ × NonemptyCompacts ℓ_infty_ℝ =>
              hausdorffDist (p.1 : Set ℓ_infty_ℝ) p.2) ∘
            Prod.swap ''
          { a | ⟦a⟧ = x } ×ˢ { b | ⟦b⟧ = y } := by
      ext
      simp only [comp_apply, Prod.fst_swap, Prod.snd_swap, hausdorffDist_comm]
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
A :
  Eq (α := 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⟧ = x}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = y})
    ((fun (p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) × NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦
          hausdorffDist (↑p.1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑p.2 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) ∘
        Prod.swap ''
      SProd.sprod (α := Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) (β :=
        Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = x}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = y})
⊢ dist x y = dist y x

Tactic:
simp only [dist, A, image_comp, image_swap_prod]

Premises used: Set.image_swap_prod, Set.image_comp, Dist.dist
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
⊢ Isometry Φ

Tactic:
have hΦ : Isometry Φ := isometry_optimalGHInjr X Y
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
⊢ Isometry Ψ

Tactic:
have hΨ : Isometry Ψ := isometry_optimalGHInjl Y Z
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
⊢ Eq (α := Y → GlueSpace hΦ hΨ) (toGlueL hΦ hΨ ∘ optimalGHInjr X Y) (toGlueR hΦ hΨ ∘ optimalGHInjl Y Z)

Tactic:
have Comm : toGlueL hΦ hΨ ∘ optimalGHInjr X Y = toGlueR hΦ hΨ ∘ optimalGHInjl Y Z :=
      toGlue_commute hΦ hΨ
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : Eq (α := Y → GlueSpace hΦ hΨ) (toGlueL hΦ hΨ ∘ optimalGHInjr X Y) (toGlueR hΦ hΨ ∘ optimalGHInjl Y Z)
rw : dist x z = dist x (toGHSpace Z)
rw₁ rw₂ : dist x z = dist x z
⊢ dist x z = dist (toGHSpace X) (toGHSpace Z)

Tactic:
rw [x.toGHSpace_rep, z.toGHSpace_rep]

Premises used: GromovHausdorff.GHSpace.toGHSpace_rep
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : Eq (α := Y → GlueSpace hΦ hΨ) (toGlueL hΦ hΨ ∘ optimalGHInjr X Y) (toGlueR hΦ hΨ ∘ optimalGHInjl Y Z)
⊢ dist (toGHSpace X) (toGHSpace Z) ≤
    hausdorffDist (α := GlueSpace hΦ hΨ) (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y))
      (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z))

Tactic:
(ghDist_le_hausdorffDist ((toGlueL_isometry hΦ hΨ).comp (isometry_optimalGHInjl X Y))
          ((toGlueR_isometry hΦ hΨ).comp (isometry_optimalGHInjr Y Z)))

Premises used: Isometry.comp, GromovHausdorff.isometry_optimalGHInjr, GromovHausdorff.ghDist, Metric.toGlueL_isometry, GromovHausdorff.ghDist_le_hausdorffDist, Metric.toGlueR_isometry, GromovHausdorff.isometry_optimalGHInjl
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : Eq (α := Y → GlueSpace hΦ hΨ) (toGlueL hΦ hΨ ∘ optimalGHInjr X Y) (toGlueR hΦ hΨ ∘ optimalGHInjl Y Z)
⊢ hausdorffDist (α := GlueSpace hΦ hΨ) (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y))
      (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z)) ≤
    hausdorffDist (α := GlueSpace hΦ hΨ) (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y))
        (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y)) +
      hausdorffDist (α := GlueSpace hΦ hΨ) (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y))
        (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z))

Tactic:
hausdorffDist_triangle <| hausdorffEDist_ne_top_of_nonempty_of_bounded
          (range_nonempty _) (range_nonempty _) ?_ ?_

Premises used: Metric.hausdorffDist_triangle, Metric.hausdorffEDist_ne_top_of_nonempty_of_bounded, Set.range_nonempty
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : Eq (α := Y → GlueSpace hΦ hΨ) (toGlueL hΦ hΨ ∘ optimalGHInjr X Y) (toGlueR hΦ hΨ ∘ optimalGHInjl Y Z)
refine_1 : Bornology.IsBounded (α := GlueSpace hΦ hΨ) (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y))
refine_2 : Bornology.IsBounded (α := GlueSpace hΦ hΨ) (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y))
⊢ hausdorffDist (α := GlueSpace hΦ hΨ) (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y))
      (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z)) ≤
    hausdorffDist (α := GlueSpace hΦ hΨ) (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y))
        (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y)) +
      hausdorffDist (α := GlueSpace hΦ hΨ) (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y))
        (range (toGlueR hΦ hΨ ∘ optimalGHInjr Y Z))

Tactic:
refine hausdorffDist_triangle <| hausdorffEDist_ne_top_of_nonempty_of_bounded
          (range_nonempty _) (range_nonempty _) ?_ ?_

Premises used: Metric.hausdorffDist_triangle, Metric.hausdorffEDist_ne_top_of_nonempty_of_bounded, Set.range_nonempty
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : Eq (α := Y → GlueSpace hΦ hΨ) (toGlueL hΦ hΨ ∘ optimalGHInjr X Y) (toGlueR hΦ hΨ ∘ optimalGHInjl Y Z)
⊢ Bornology.IsBounded (α := GlueSpace hΦ hΨ) (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y))

Tactic:
(isCompact_range (Isometry.continuous
            ((toGlueL_isometry hΦ hΨ).comp (isometry_optimalGHInjl X Y)))).isBounded

Premises used: Isometry.comp, IsCompact.isBounded, Metric.toGlueL_isometry, Isometry.continuous, isCompact_range, GromovHausdorff.isometry_optimalGHInjl
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : Eq (α := Y → GlueSpace hΦ hΨ) (toGlueL hΦ hΨ ∘ optimalGHInjr X Y) (toGlueR hΦ hΨ ∘ optimalGHInjl Y Z)
⊢ Bornology.IsBounded (α := GlueSpace hΦ hΨ) (range (toGlueL hΦ hΨ ∘ optimalGHInjl X Y))

Tactic:
exact (isCompact_range (Isometry.continuous
            ((toGlueL_isometry hΦ hΨ).comp (isometry_optimalGHInjl X Y)))).isBounded

Premises used: Isometry.comp, IsCompact.isBounded, Metric.toGlueL_isometry, Isometry.continuous, isCompact_range, GromovHausdorff.isometry_optimalGHInjl
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : Eq (α := Y → GlueSpace hΦ hΨ) (toGlueL hΦ hΨ ∘ optimalGHInjr X Y) (toGlueR hΦ hΨ ∘ optimalGHInjl Y Z)
⊢ Bornology.IsBounded (α := GlueSpace hΦ hΨ) (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y))

Tactic:
(isCompact_range (Isometry.continuous
            ((toGlueL_isometry hΦ hΨ).comp (isometry_optimalGHInjr X Y)))).isBounded

Premises used: Isometry.comp, GromovHausdorff.isometry_optimalGHInjr, IsCompact.isBounded, Metric.toGlueL_isometry, Isometry.continuous, isCompact_range