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
inhabited_h_1 : Inhabited X
inhabited_h : Inhabited Y
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
            diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ →
          hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
          hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ ghDist X Y
have refine_1 : Set.Nonempty (α := ℝ)
  ((fun (p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) × NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦
      hausdorffDist (↑p.1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑p.2 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) ''
    SProd.sprod (α := Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) (β :=
      Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)))
      {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = toGHSpace X}
      {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = toGHSpace Y})
Tactic: apply le_csInf
-- 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
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
            diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ →
          hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
          hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
refine_1 :
  Set.Nonempty (α := ℝ)
    ((fun (p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) × NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦
        hausdorffDist (↑p.1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑p.2 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) ''
      SProd.sprod (α := Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) (β :=
        Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)))
        {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = toGHSpace X}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = toGHSpace Y})
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ ghDist X Y
have refine_1₁ : ∀ (b : ℝ),
  Membership.mem (γ := Set ℝ)
      ((fun (p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) × NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦
          hausdorffDist (↑p.1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑p.2 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) ''
        SProd.sprod (α := Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) (β :=
          Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)))
          {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = toGHSpace X}
          {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = toGHSpace Y})
      b →
    hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ b
Tactic: apply le_csInf
-- 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
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
            diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ →
          hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
          hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ Set.Nonempty (α := ℝ)
    ((fun (p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) × NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦
        hausdorffDist (↑p.1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑p.2 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) ''
      SProd.sprod (α := Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) (β :=
        Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)))
        {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = toGHSpace X}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = toGHSpace Y})
have refine_1 : Set.Nonempty (α := NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
  {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = toGHSpace X}
Tactic: refine (Set.Nonempty.prod ?_ ?_).image _
-- 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
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) <
            diam.{u} (α := X) univ + 1 + diam.{v} (α := Y) univ →
          hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
          hausdorffDist (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑q : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
refine_1 :
  Set.Nonempty (α := NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
    {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = toGHSpace X}
⊢ Set.Nonempty (α := ℝ)
    ((fun (p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) × NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦
        hausdorffDist (↑p.1 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑p.2 : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) ''
      SProd.sprod (α := Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) (β :=
        Set (NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)))
        {a : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦a⟧ = toGHSpace X}
        {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = toGHSpace Y})
have refine_1₁ : Set.Nonempty (α := NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
  {b : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) | ⟦b⟧ = toGHSpace Y}
Tactic: refine (Set.Nonempty.prod ?_ ?_).image _
-- 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
F : OptimalGHCoupling X Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjr X Y
⊢ ∃ (Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ)
have refine_1 : Isometry Φ
Tactic: refine ⟨Φ, Ψ, ?_, ?_, ?_⟩
-- 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
F : OptimalGHCoupling X Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjr X Y
refine_1 : Isometry Φ
⊢ ∃ (Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ)
have refine_2 : Isometry Ψ
Tactic: refine ⟨Φ, Ψ, ?_, ?_, ?_⟩
-- 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
F : OptimalGHCoupling X Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := F ∘ optimalGHInjr X Y
refine_1 : Isometry Φ
refine_2 : Isometry Ψ
⊢ ∃ (Φ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (Ψ : Y → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)),
    Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ)
have refine_3 : ghDist X Y = hausdorffDist (range Φ) (range Ψ)
Tactic: refine ⟨Φ, Ψ, ?_, ?_, ?_⟩
-- 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
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
⊢ ghDist X Y = hausdorffDist (range Φ) (range Ψ)
have refine_3 : hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) =
  hausdorffDist (F '' range (optimalGHInjl X Y)) (F '' range (optimalGHInjr X Y))
Tactic: rw [← image_univ, ← image_univ, image_comp F, image_univ, image_comp F (optimalGHInjr X Y),
      image_univ, ← hausdorffDist_optimal]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
x : GHSpace
⊢ dist x x = 0
have rcases : ∀ (y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (hy : ⟦y⟧ = x), dist x x = 0
Tactic: rcases exists_rep x with ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
x : GHSpace
y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : ⟦y⟧ = x
⊢ dist x x = 0
have refine_1 : dist x x ≤ 0
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
x : GHSpace
y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : ⟦y⟧ = x
refine_1 : dist x x ≤ 0
⊢ dist x x = 0
have refine_2 : 0 ≤ dist x x
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
x : GHSpace
y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : ⟦y⟧ = x
⊢ dist x x ≤ 0
have 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})
Tactic: apply csInf_le
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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})
⊢ dist x x ≤ 0
have 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
Tactic: apply csInf_le
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
x : GHSpace
y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : ⟦y⟧ = x
⊢ 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
have 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
Tactic: simp only [mem_image, mem_prod, mem_setOf_eq, Prod.exists]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
x : GHSpace
y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : ⟦y⟧ = x
⊢ ∃ (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
have refine_1 : (⟦y⟧ = x ∧ ⟦y⟧ = x) ∧ hausdorffDist (↑y : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (↑y : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = 0
Tactic: exists y, y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
x : GHSpace
y : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
hy : ⟦y⟧ = x
⊢ 0 ≤ dist x x
have 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})
Tactic: apply le_csInf
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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})
⊢ 0 ≤ dist x x
have 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
Tactic: apply le_csInf
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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})
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
Goal:
x y : GHSpace
⊢ dist x y = dist y x
have 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})
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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
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
⊢ dist x z ≤ dist x y + dist y z
have hΦ : Isometry Φ
Tactic: have hΦ : Isometry Φ := isometry_optimalGHInjr X Y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
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
⊢ dist x z ≤ dist x y + dist y z
have hΨ : Isometry Ψ
Tactic: have hΨ : Isometry Ψ := isometry_optimalGHInjl Y Z
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
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 Ψ
⊢ dist x z ≤ dist x y + dist y z
have Comm : 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Ψ
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 x z = dist (toGHSpace X) (toGHSpace Z)
have rw : dist x z = dist x (toGHSpace Z)
Tactic: rw [x.toGHSpace_rep, z.toGHSpace_rep]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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)
⊢ dist x z = dist (toGHSpace X) (toGHSpace Z)
have rw₁ : dist x z = dist x z
Tactic: rw [x.toGHSpace_rep, z.toGHSpace_rep]