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 : CompactSpace.{w} (↑s : Type w)
ΦΦ' : Φ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Φ'
⊢ Ψ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Ψ'

Tactic:
have ΨΨ' : Ψ = Subtype.val ∘ Ψ' := 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
γ : 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 : CompactSpace.{w} (↑s : Type w)
ΦΦ' : Φ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Φ'
ΨΨ' : Ψ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Ψ'
rw :
  hausdorffDist (Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' range Φ')
      (Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' range Ψ') =
    hausdorffDist (range Φ') (range Ψ')
⊢ hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')

Tactic:
rw [ΦΦ', ΨΨ', range_comp, range_comp]

Premises used: Set.range_comp
-- 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 : CompactSpace.{w} (↑s : Type w)
ΦΦ' : Φ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Φ'
ΨΨ' : Ψ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Ψ'
⊢ hausdorffDist (Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' range Φ')
      (Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' range Ψ') =
    hausdorffDist (range Φ') (range Ψ')

Tactic:
hausdorffDist_image isometry_subtype_coe

Premises used: Metric.hausdorffDist_image, isometry_subtype_coe
-- 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 : CompactSpace.{w} (↑s : Type w)
ΦΦ' : Φ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Φ'
ΨΨ' : Ψ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Ψ'
⊢ hausdorffDist (Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' range Φ')
      (Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' range Ψ') =
    hausdorffDist (range Φ') (range Ψ')

Tactic:
exact hausdorffDist_image isometry_subtype_coe

Premises used: Metric.hausdorffDist_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
γ : 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 : CompactSpace.{w} (↑s : Type w)
ΦΦ' : Φ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Φ'
ΨΨ' : Ψ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Ψ'
⊢ hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')

Tactic:
have : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ') := by
    rw [ΦΦ', ΨΨ', range_comp, range_comp]
    exact hausdorffDist_image isometry_subtype_coe
-- 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 : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
rw : ghDist X Y ≤ hausdorffDist (range Φ') (range Ψ')
⊢ ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)

Tactic:
rw [this]
-- 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 : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : (↑s : Type w) → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (↑s : Type w)
⊢ hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')

Tactic:
have : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ') :=
    hausdorffDist_image (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
γ : 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 Ψ')
rw : ghDist X Y ≤ hausdorffDist (F '' range Φ') (F '' range Ψ')
⊢ ghDist X Y ≤ hausdorffDist (range Φ') (range Ψ')

Tactic:
rw [← this]
-- 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' := ⋯ }
rw : ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑A : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ ⟦A⟧ = toGHSpace X

Tactic:
rw [eq_toGHSpace_iff]

Premises used: 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
γ : 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' := ⋯ }
⊢ ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑A : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))

Tactic:
⟨fun x => F (Φ' x), (kuratowskiEmbedding.isometry _).comp IΦ', range_comp _ _⟩

Premises used: Isometry.comp, Set.range_comp, And.intro, Exists.intro, 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
γ : 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' := ⋯ }
⊢ ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑A : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))

Tactic:
exact ⟨fun x => F (Φ' x), (kuratowskiEmbedding.isometry _).comp IΦ', range_comp _ _⟩
-- 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' := ⋯ }
⊢ ⟦A⟧ = toGHSpace X

Tactic:
have AX : ⟦A⟧ = toGHSpace X := by
    rw [eq_toGHSpace_iff]
    exact ⟨fun x => F (Φ' x), (kuratowskiEmbedding.isometry _).comp IΦ', range_comp _ _⟩
-- 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
rw : ∃ (Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑B : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ ⟦B⟧ = toGHSpace Y

Tactic:
rw [eq_toGHSpace_iff]

Premises used: 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
γ : 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
⊢ ∃ (Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑B : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))

Tactic:
⟨fun x => F (Ψ' x), (kuratowskiEmbedding.isometry _).comp IΨ', range_comp _ _⟩

Premises used: Isometry.comp, Set.range_comp, And.intro, Exists.intro, 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
γ : 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
⊢ ∃ (Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑B : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))

Tactic:
exact ⟨fun x => F (Ψ' x), (kuratowskiEmbedding.isometry _).comp IΨ', range_comp _ _⟩
-- 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
⊢ ⟦B⟧ = toGHSpace Y

Tactic:
have BY : ⟦B⟧ = toGHSpace Y := by
    rw [eq_toGHSpace_iff]
    exact ⟨fun x => F (Ψ' x), (kuratowskiEmbedding.isometry _).comp IΨ', range_comp _ _⟩
-- 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
⊢ ghDist X Y ≤ hausdorffDist (F '' range Φ') (F '' range Ψ')

Tactic:
csInf_le ⟨0, ?_⟩ ?_

Premises used: GromovHausdorff.ghDist, Exists.intro, OfNat.ofNat, csInf_le
-- 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 :
  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
refine_2 :
  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})
    (hausdorffDist (F '' range Φ') (F '' range Ψ'))
⊢ ghDist X Y ≤ hausdorffDist (F '' range Φ') (F '' range Ψ')

Tactic:
refine csInf_le ⟨0, ?_⟩ ?_

Premises used: Exists.intro, OfNat.ofNat, csInf_le