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
γ : Type w
inst_6 : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h : Membership.mem (γ := Set X) univ xX
s : Set γ := range Φ ∪ range Ψ
Φ' : X → (↑s : Type w) := fun (y : X) ↦ Subtype.mk (p := fun (x : γ) ↦ x ∈ s) (Φ y) ⋯
Ψ' : Y → (↑s : Type w) := fun (y : Y) ↦ Subtype.mk (p := fun (x : γ) ↦ x ∈ s) (Ψ y) ⋯
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this_1 : IsCompact s
this_2 : CompactSpace.{w} (↑s : Type w)
ΦΦ' : Φ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Φ'
ΨΨ' : Ψ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Ψ'
this_3 : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : (↑s : Type w) → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (↑s : Type w)
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
AX : ⟦A⟧ = toGHSpace X
BY : ⟦B⟧ = toGHSpace Y
refine_1 :
  ∀ ⦃a : ℝ⦄ (x x_1 : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦x⟧ = toGHSpace X →
      ⟦x_1⟧ = toGHSpace Y →
        hausdorffDist (↑x : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑x_1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = a → 0 ≤ a
⊢ Membership.mem (γ := Set ℝ)
    (lowerBounds
      ((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}))
    0

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

Premises used: lowerBounds, and_imp, Set.mem_image, forall_exists_index, Set.mem_setOf_eq, Set.mem_prod, Prod.exists
-- 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
γ : Type w
inst_6 : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h : Membership.mem (γ := Set X) univ xX
s : Set γ := range Φ ∪ range Ψ
Φ' : X → (↑s : Type w) := fun (y : X) ↦ Subtype.mk (p := fun (x : γ) ↦ x ∈ s) (Φ y) ⋯
Ψ' : Y → (↑s : Type w) := fun (y : Y) ↦ Subtype.mk (p := fun (x : γ) ↦ x ∈ s) (Ψ y) ⋯
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this_1 : IsCompact s
this_2 : CompactSpace.{w} (↑s : Type w)
ΦΦ' : Φ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Φ'
ΨΨ' : Ψ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Ψ'
this_3 : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : (↑s : Type w) → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (↑s : Type w)
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
AX : ⟦A⟧ = toGHSpace X
BY : ⟦B⟧ = toGHSpace Y
t : ℝ
refine_1 :
  ∀ (x x_1 : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦x⟧ = toGHSpace X →
      ⟦x_1⟧ = toGHSpace Y →
        hausdorffDist (↑x : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑x_1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = t → 0 ≤ t
⊢ ∀ (x x_1 : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦x⟧ = toGHSpace X →
      ⟦x_1⟧ = toGHSpace Y →
        hausdorffDist (↑x : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑x_1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = t → 0 ≤ t

Tactic:
_
-- 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
γ : Type w
inst_6 : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h : Membership.mem (γ := Set X) univ xX
s : Set γ := range Φ ∪ range Ψ
Φ' : X → (↑s : Type w) := fun (y : X) ↦ Subtype.mk (p := fun (x : γ) ↦ x ∈ s) (Φ y) ⋯
Ψ' : Y → (↑s : Type w) := fun (y : Y) ↦ Subtype.mk (p := fun (x : γ) ↦ x ∈ s) (Ψ y) ⋯
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this_1 : IsCompact s
this_2 : CompactSpace.{w} (↑s : Type w)
ΦΦ' : Φ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Φ'
ΨΨ' : Ψ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Ψ'
this_3 : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : (↑s : Type w) → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (↑s : Type w)
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
AX : ⟦A⟧ = toGHSpace X
BY : ⟦B⟧ = toGHSpace Y
t : ℝ
x : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
refine_1 :
  ∀ (x_1 : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦x⟧ = toGHSpace X →
      ⟦x_1⟧ = toGHSpace Y →
        hausdorffDist (↑x : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑x_1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = t → 0 ≤ t
⊢ ∀ (x_1 : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦x⟧ = toGHSpace X →
      ⟦x_1⟧ = toGHSpace Y →
        hausdorffDist (↑x : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑x_1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = t → 0 ≤ t

Tactic:
_
-- 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
γ : Type w
inst_6 : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h : Membership.mem (γ := Set X) univ xX
s : Set γ := range Φ ∪ range Ψ
Φ' : X → (↑s : Type w) := fun (y : X) ↦ Subtype.mk (p := fun (x : γ) ↦ x ∈ s) (Φ y) ⋯
Ψ' : Y → (↑s : Type w) := fun (y : Y) ↦ Subtype.mk (p := fun (x : γ) ↦ x ∈ s) (Ψ y) ⋯
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this_1 : IsCompact s
this_2 : CompactSpace.{w} (↑s : Type w)
ΦΦ' : Φ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Φ'
ΨΨ' : Ψ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Ψ'
this_3 : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : (↑s : Type w) → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (↑s : Type w)
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
AX : ⟦A⟧ = toGHSpace X
BY : ⟦B⟧ = toGHSpace Y
t : ℝ
x x_1 : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
refine_1 :
  ⟦x⟧ = toGHSpace X →
    ⟦x_1⟧ = toGHSpace Y →
      hausdorffDist (↑x : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑x_1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = t → 0 ≤ t
⊢ ⟦x⟧ = toGHSpace X →
    ⟦x_1⟧ = toGHSpace Y →
      hausdorffDist (↑x : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑x_1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = t → 0 ≤ t

Tactic:
_
-- 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
γ : Type w
inst_6 : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h : Membership.mem (γ := Set X) univ xX
s : Set γ := range Φ ∪ range Ψ
Φ' : X → (↑s : Type w) := fun (y : X) ↦ Subtype.mk (p := fun (x : γ) ↦ x ∈ s) (Φ y) ⋯
Ψ' : Y → (↑s : Type w) := fun (y : Y) ↦ Subtype.mk (p := fun (x : γ) ↦ x ∈ s) (Ψ y) ⋯
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this_1 : IsCompact s
this_2 : CompactSpace.{w} (↑s : Type w)
ΦΦ' : Φ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Φ'
ΨΨ' : Ψ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Ψ'
this_3 : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : (↑s : Type w) → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (↑s : Type w)
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
AX : ⟦A⟧ = toGHSpace X
BY : ⟦B⟧ = toGHSpace Y
t : ℝ
x x_1 : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
h_1 : ⟦x⟧ = toGHSpace X
refine_1 :
  ⟦x_1⟧ = toGHSpace Y →
    hausdorffDist (↑x : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑x_1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = t → 0 ≤ t
⊢ ⟦x_1⟧ = toGHSpace Y →
    hausdorffDist (↑x : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑x_1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = t → 0 ≤ t

Tactic:
_
-- 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
γ : Type w
inst_6 : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h : Membership.mem (γ := Set X) univ xX
s : Set γ := range Φ ∪ range Ψ
Φ' : X → (↑s : Type w) := fun (y : X) ↦ Subtype.mk (p := fun (x : γ) ↦ x ∈ s) (Φ y) ⋯
Ψ' : Y → (↑s : Type w) := fun (y : Y) ↦ Subtype.mk (p := fun (x : γ) ↦ x ∈ s) (Ψ y) ⋯
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this_1 : IsCompact s
this_2 : CompactSpace.{w} (↑s : Type w)
ΦΦ' : Φ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Φ'
ΨΨ' : Ψ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Ψ'
this_3 : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : (↑s : Type w) → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (↑s : Type w)
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
AX : ⟦A⟧ = toGHSpace X
BY : ⟦B⟧ = toGHSpace Y
t : ℝ
x x_1 : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
h_1 : ⟦x⟧ = toGHSpace X
h_2 : ⟦x_1⟧ = toGHSpace Y
ht : hausdorffDist (↑x : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑x_1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = t
refine_1 : 0 ≤ hausdorffDist (↑x : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑x_1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ 0 ≤ t

Tactic:
rw [← ht]
-- 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
γ : Type w
inst_6 : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h : Membership.mem (γ := Set X) univ xX
s : Set γ := range Φ ∪ range Ψ
Φ' : X → (↑s : Type w) := fun (y : X) ↦ Subtype.mk (p := fun (x : γ) ↦ x ∈ s) (Φ y) ⋯
Ψ' : Y → (↑s : Type w) := fun (y : Y) ↦ Subtype.mk (p := fun (x : γ) ↦ x ∈ s) (Ψ y) ⋯
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this_1 : IsCompact s
this_2 : CompactSpace.{w} (↑s : Type w)
ΦΦ' : Φ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Φ'
ΨΨ' : Ψ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Ψ'
this_3 : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : (↑s : Type w) → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (↑s : Type w)
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
AX : ⟦A⟧ = toGHSpace X
BY : ⟦B⟧ = toGHSpace Y
t : ℝ
x x_1 : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
h_1 : ⟦x⟧ = toGHSpace X
h_2 : ⟦x_1⟧ = toGHSpace Y
ht : hausdorffDist (↑x : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑x_1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = t
⊢ 0 ≤ hausdorffDist (↑x : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑x_1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))

Tactic:
hausdorffDist_nonneg

Premises used: Metric.hausdorffDist_nonneg
-- 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
γ : Type w
inst_6 : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h : Membership.mem (γ := Set X) univ xX
s : Set γ := range Φ ∪ range Ψ
Φ' : X → (↑s : Type w) := fun (y : X) ↦ Subtype.mk (p := fun (x : γ) ↦ x ∈ s) (Φ y) ⋯
Ψ' : Y → (↑s : Type w) := fun (y : Y) ↦ Subtype.mk (p := fun (x : γ) ↦ x ∈ s) (Ψ y) ⋯
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this_1 : IsCompact s
this_2 : CompactSpace.{w} (↑s : Type w)
ΦΦ' : Φ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Φ'
ΨΨ' : Ψ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Ψ'
this_3 : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : (↑s : Type w) → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (↑s : Type w)
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
AX : ⟦A⟧ = toGHSpace X
BY : ⟦B⟧ = toGHSpace Y
t : ℝ
x x_1 : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
h_1 : ⟦x⟧ = toGHSpace X
h_2 : ⟦x_1⟧ = toGHSpace Y
ht : hausdorffDist (↑x : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑x_1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = t
⊢ 0 ≤ hausdorffDist (↑x : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑x_1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))

Tactic:
exact hausdorffDist_nonneg

Premises used: Metric.hausdorffDist_nonneg
-- 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
γ : Type w
inst_6 : MetricSpace γ
Φ : X → γ
Ψ : Y → γ
ha : Isometry Φ
hb : Isometry Ψ
xX : X
h : Membership.mem (γ := Set X) univ xX
s : Set γ := range Φ ∪ range Ψ
Φ' : X → (↑s : Type w) := fun (y : X) ↦ Subtype.mk (p := fun (x : γ) ↦ x ∈ s) (Φ y) ⋯
Ψ' : Y → (↑s : Type w) := fun (y : Y) ↦ Subtype.mk (p := fun (x : γ) ↦ x ∈ s) (Ψ y) ⋯
IΦ' : Isometry Φ'
IΨ' : Isometry Ψ'
this_1 : IsCompact s
this_2 : CompactSpace.{w} (↑s : Type w)
ΦΦ' : Φ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Φ'
ΨΨ' : Ψ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Ψ'
this_3 : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : (↑s : Type w) → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (↑s : Type w)
this : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
A : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) := { carrier := F '' range Φ', isCompact' := ⋯, nonempty' := ⋯ }
B : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) := { carrier := F '' range Ψ', isCompact' := ⋯, nonempty' := ⋯ }
AX : ⟦A⟧ = toGHSpace X
BY : ⟦B⟧ = toGHSpace Y
refine_2 refine_2₁ :
  (A, B) ∈
      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} ∧
    hausdorffDist (↑(A, B).1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑(A, B).2 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) =
      hausdorffDist (F '' range Φ') (F '' range Ψ')
⊢ ∃
    x ∈
      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},
    hausdorffDist (↑x.1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑x.2 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) =
      hausdorffDist (F '' range Φ') (F '' range Ψ')

Tactic:
exists (⟨A, B⟩ : NonemptyCompacts ℓ_infty_ℝ × NonemptyCompacts ℓ_infty_ℝ)

Premises used: Prod.mk
-- 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
inhabit :
  ∀ (inhabited_h : Inhabited X),
    hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y

Tactic:
inhabit X
-- 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 : Inhabited X
inhabit :
  ∀ (inhabited_h : Inhabited Y),
    hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y

Tactic:
inhabit Y
-- 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
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
rcases :
  ∀ (Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (Φisom : Isometry Φ) (Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))),
    hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
      hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
    hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))

Tactic:
rcases eq_toGHSpace_iff.1 hp with ⟨Φ, ⟨Φisom, Φrange⟩⟩

Premises used: Iff.mp, GromovHausdorff.eq_toGHSpace_iff
-- 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
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
rcases :
  ∀ (Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (Ψisom : Isometry Ψ) (Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))),
    hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
      hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
    hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))

Tactic:
rcases eq_toGHSpace_iff.1 hq with ⟨Ψ, ⟨Ψisom, Ψrange⟩⟩

Premises used: Iff.mp, GromovHausdorff.eq_toGHSpace_iff
-- 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
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
rcases :
  ∀ (xX : X),
    Membership.mem (γ := Set X) univ xX →
      diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
⊢ diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ

Tactic:
rcases exists_mem_of_nonempty X with ⟨xX, _⟩

Premises used: Set.exists_mem_of_nonempty
-- 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
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
xX : X
h : Membership.mem (γ := Set X) univ xX
rw : ∃ y ∈ (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), dist (Φ xX) y < diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
⊢ ∃ y ∈ range Ψ, dist (Φ xX) y < diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ

Tactic:
rw [Ψrange]
-- 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
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
xX : X
h : Membership.mem (γ := Set X) univ xX
⊢ Φ xX ∈ (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))

Tactic:
have : Φ xX ∈ (p : Set _) := Φrange ▸ (mem_range_self _)
-- 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
p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound :
  hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
    diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
xX : X
h : Membership.mem (γ := Set X) univ xX
this : Φ xX ∈ (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ ∃ y ∈ (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), dist (Φ xX) y < diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ

Tactic:
exists_dist_lt_of_hausdorffDist_lt this bound
            (hausdorffEDist_ne_top_of_nonempty_of_bounded p.nonempty q.nonempty
              p.isCompact.isBounded q.isCompact.isBounded)

Premises used: IsCompact.isBounded, Metric.hausdorffEDist_ne_top_of_nonempty_of_bounded, Metric.exists_dist_lt_of_hausdorffDist_lt, TopologicalSpace.NonemptyCompacts.nonempty, TopologicalSpace.NonemptyCompacts.isCompact