awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 Ψ')
⊢ ghDist X Y ≤ hausdorffDist (range Φ') (range Ψ')
have rw : ghDist X Y ≤ hausdorffDist (F '' range Φ') (F '' range Ψ')
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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
have rw : ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑A : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Tactic: rw [eq_toGHSpace_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
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' := ⋯ }
⊢ ghDist X Y ≤ hausdorffDist (F '' range Φ') (F '' range Ψ')
have AX : ⟦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 _ _⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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
have rw : ∃ (Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑B : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Tactic: rw [eq_toGHSpace_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
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
⊢ ghDist X Y ≤ hausdorffDist (F '' range Φ') (F '' range Ψ')
have BY : ⟦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 _ _⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 Ψ')
have 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
Tactic: refine csInf_le ⟨0, ?_⟩ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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
⊢ ghDist X Y ≤ hausdorffDist (F '' range Φ') (F '' range Ψ')
have 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 Ψ'))
Tactic: refine csInf_le ⟨0, ?_⟩ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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
⊢ 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
have 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
Tactic: simp only [lowerBounds, mem_image, mem_prod, mem_setOf_eq, Prod.exists, and_imp,
      forall_exists_index]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 ≤ t
have refine_1 : 0 ≤ hausdorffDist (↑x : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑x_1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Tactic: rw [← ht]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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
⊢ ∃
    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 Ψ')
have 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 Ψ')
Tactic: exists (⟨A, B⟩ : NonemptyCompacts ℓ_infty_ℝ × NonemptyCompacts ℓ_infty_ℝ)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y
have inhabit : ∀ (inhabited_h : Inhabited X),
  hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y
Tactic: inhabit X
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y
have inhabit : ∀ (inhabited_h : Inhabited Y),
  hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y
Tactic: inhabit Y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
    hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
have 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 : ℕ) ↦ ℝ) ∞))
Tactic: rcases eq_toGHSpace_iff.1 hp with ⟨Φ, ⟨Φisom, Φrange⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 : ℕ) ↦ ℝ) ∞))
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
    hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
have 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 : ℕ) ↦ ℝ) ∞))
Tactic: rcases eq_toGHSpace_iff.1 hq with ⟨Ψ, ⟨Ψisom, Ψrange⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 : ℕ) ↦ ℝ) ∞))
⊢ diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
have rcases : ∀ (xX : X),
  Membership.mem (γ := Set X) univ xX →
    diam (range Φ ∪ range Ψ) ≤ 2 * diam.{u} (α := X) univ + 1 + 2 * diam.{v} (α := Y) univ
Tactic: rcases exists_mem_of_nonempty X with ⟨xX, _⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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
⊢ ∃ y ∈ range Ψ, dist (Φ xX) y < diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
have rw : ∃ y ∈ (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), dist (Φ xX) y < diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
Tactic: rw [Ψrange]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
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
⊢ ∃ y ∈ (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), dist (Φ xX) y < diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ
have this : Φ xX ∈ (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Tactic: have : Φ xX ∈ (p : Set _) := Φrange ▸ (mem_range_self _)