awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : Eq (α := Y → GlueSpace hΦ hΨ) (toGlueL hΦ hΨ ∘ optimalGHInjr X Y) (toGlueR hΦ hΨ ∘ optimalGHInjl Y Z)
⊢ Bornology.IsBounded (α := GlueSpace hΦ hΨ) (range (toGlueL hΦ hΨ ∘ optimalGHInjr X Y))

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

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

Tactic:
simp only [← range_comp, Comm]

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

Tactic:
rw [hausdorffDist_image (toGlueL_isometry hΦ hΨ),
          hausdorffDist_image (toGlueR_isometry hΦ hΨ)]

Premises used: Metric.toGlueL_isometry, Metric.hausdorffDist_image, Metric.toGlueR_isometry
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y z : GHSpace
X : Type := x.Rep
Y : Type := y.Rep
Z : Type := z.Rep
γ1 : Type := OptimalGHCoupling X Y
γ2 : Type := OptimalGHCoupling Y Z
Φ : Y → γ1 := optimalGHInjr X Y
hΦ : Isometry Φ
Ψ : Y → γ2 := optimalGHInjl Y Z
hΨ : Isometry Ψ
Comm : Eq (α := Y → GlueSpace hΦ hΨ) (toGlueL hΦ hΨ ∘ optimalGHInjr X Y) (toGlueR hΦ hΨ ∘ optimalGHInjl Y Z)
rw :
  ghDist X Y + hausdorffDist (α := OptimalGHCoupling Y Z) (range (optimalGHInjl Y Z)) (range (optimalGHInjr Y Z)) =
    dist (toGHSpace X) (toGHSpace Y) + dist (toGHSpace Y) (toGHSpace Z)
rw₁ : ghDist X Y + ghDist Y Z = dist (toGHSpace X) (toGHSpace Y) + dist (toGHSpace Y) (toGHSpace Z)
rw₂ :
  dist (toGHSpace X) (toGHSpace Y) + ghDist Y Z = dist (toGHSpace X) (toGHSpace Y) + dist (toGHSpace Y) (toGHSpace Z)
rw₃ rw₄ :
  dist (toGHSpace X) (toGHSpace Y) + dist (toGHSpace Y) (toGHSpace Z) =
    dist (toGHSpace X) (toGHSpace Y) + dist (toGHSpace Y) (toGHSpace Z)
⊢ hausdorffDist (α := OptimalGHCoupling X Y) (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) +
      hausdorffDist (α := OptimalGHCoupling Y Z) (range (optimalGHInjl Y Z)) (range (optimalGHInjr Y Z)) =
    dist (toGHSpace X) (toGHSpace Y) + dist (toGHSpace Y) (toGHSpace Z)

Tactic:
rw [hausdorffDist_optimal, hausdorffDist_optimal, ghDist, ghDist]

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

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

Premises used: GromovHausdorff.GHSpace.toGHSpace_rep
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
rcases :
  ∀ (Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) (Φisom : Isometry Φ)
    (Ψisom : Isometry Ψ) (DΦΨ : ghDist x.Rep y.Rep = hausdorffDist (range Φ) (range Ψ)), x = y
⊢ x = y

Tactic:
rcases ghDist_eq_hausdorffDist x.Rep y.Rep with ⟨Φ, Ψ, Φisom, Ψisom, DΦΨ⟩

Premises used: GromovHausdorff.ghDist_eq_hausdorffDist, GromovHausdorff.GHSpace.Rep
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : ghDist x.Rep y.Rep = hausdorffDist (range Φ) (range Ψ)
⊢ 0 = hausdorffDist (range Φ) (range Ψ)

Tactic:
rw [← dist_ghDist, hxy] at DΦΨ

Premises used: GromovHausdorff.dist_ghDist
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
⊢ IsCompact (range Φ)

Tactic:
have hΦ : IsCompact (range Φ) := isCompact_range Φisom.continuous
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
hΦ : IsCompact (range Φ)
⊢ IsCompact (range Ψ)

Tactic:
have hΨ : IsCompact (range Ψ) := isCompact_range Ψisom.continuous
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
hΦ : IsCompact (range Φ)
hΨ : IsCompact (range Ψ)
apply : IsClosed (range Φ)
apply₁ : IsClosed (range Ψ)
apply₂ : hausdorffEDist (range Φ) (range Ψ) ≠ ∞
⊢ range Φ = range Ψ

Tactic:
apply (IsClosed.hausdorffDist_zero_iff_eq _ _ _).1 DΦΨ.symm

Premises used: IsClosed.hausdorffDist_zero_iff_eq, Iff.mp, Eq.symm
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
hΦ : IsCompact (range Φ)
hΨ : IsCompact (range Ψ)
⊢ IsClosed (range Φ)

Tactic:
hΦ.isClosed

Premises used: IsCompact.isClosed
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
hΦ : IsCompact (range Φ)
hΨ : IsCompact (range Ψ)
⊢ IsClosed (range Φ)

Tactic:
exact hΦ.isClosed

Premises used: IsCompact.isClosed
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
hΦ : IsCompact (range Φ)
hΨ : IsCompact (range Ψ)
⊢ IsClosed (range Ψ)

Tactic:
hΨ.isClosed

Premises used: IsCompact.isClosed
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
hΦ : IsCompact (range Φ)
hΨ : IsCompact (range Ψ)
⊢ IsClosed (range Ψ)

Tactic:
exact hΨ.isClosed

Premises used: IsCompact.isClosed
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
hΦ : IsCompact (range Φ)
hΨ : IsCompact (range Ψ)
⊢ hausdorffEDist (range Φ) (range Ψ) ≠ ∞

Tactic:
hausdorffEDist_ne_top_of_nonempty_of_bounded (range_nonempty _) (range_nonempty _)
          hΦ.isBounded hΨ.isBounded

Premises used: IsCompact.isBounded, Metric.hausdorffEDist_ne_top_of_nonempty_of_bounded, Set.range_nonempty
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
hΦ : IsCompact (range Φ)
hΨ : IsCompact (range Ψ)
⊢ hausdorffEDist (range Φ) (range Ψ) ≠ ∞

Tactic:
exact hausdorffEDist_ne_top_of_nonempty_of_bounded (range_nonempty _) (range_nonempty _)
          hΦ.isBounded hΨ.isBounded

Premises used: IsCompact.isBounded, Metric.hausdorffEDist_ne_top_of_nonempty_of_bounded, Set.range_nonempty
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
⊢ range Φ = range Ψ

Tactic:
have : range Φ = range Ψ := by
      have hΦ : IsCompact (range Φ) := isCompact_range Φisom.continuous
      have hΨ : IsCompact (range Ψ) := isCompact_range Ψisom.continuous
      apply (IsClosed.hausdorffDist_zero_iff_eq _ _ _).1 DΦΨ.symm
      · exact hΦ.isClosed
      · exact hΨ.isClosed
      · exact hausdorffEDist_ne_top_of_nonempty_of_bounded (range_nonempty _) (range_nonempty _)
          hΦ.isBounded hΨ.isBounded
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
this : range Φ = range Ψ
rw rw₁ : ((↑(range Ψ) : Type) ≃ᵢ y.Rep) = ((↑(range Ψ) : Type) ≃ᵢ y.Rep)
⊢ ((↑(range Ψ) : Type) ≃ᵢ y.Rep) = ((↑(range Φ) : Type) ≃ᵢ y.Rep)

Tactic:
rw [this]
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
this : range Φ = range Ψ
⊢ ((↑(range Ψ) : Type) ≃ᵢ y.Rep) = ((↑(range Φ) : Type) ≃ᵢ y.Rep)

Tactic:
have T : (range Ψ ≃ᵢ y.Rep) = (range Φ ≃ᵢ y.Rep) := by rw [this]
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
this : range Φ = range Ψ
T : ((↑(range Ψ) : Type) ≃ᵢ y.Rep) = ((↑(range Φ) : Type) ≃ᵢ y.Rep)
have : ∀ (eΨ : (↑(range Φ) : Type) ≃ᵢ y.Rep), x = y
⊢ x = y

Tactic:
have eΨ := cast T Ψisom.isometryEquivOnRange.symm
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
this : range Φ = range Ψ
T : ((↑(range Ψ) : Type) ≃ᵢ y.Rep) = ((↑(range Φ) : Type) ≃ᵢ y.Rep)
eΨ : (↑(range Φ) : Type) ≃ᵢ y.Rep
have : ∀ (e : x.Rep ≃ᵢ y.Rep), x = y
⊢ x = y

Tactic:
have e := Φisom.isometryEquivOnRange.trans eΨ
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
this : range Φ = range Ψ
T : ((↑(range Ψ) : Type) ≃ᵢ y.Rep) = ((↑(range Φ) : Type) ≃ᵢ y.Rep)
eΨ : (↑(range Φ) : Type) ≃ᵢ y.Rep
e : x.Rep ≃ᵢ y.Rep
rw : Nonempty (x.Rep ≃ᵢ y.Rep)
⊢ x = y

Tactic:
rw [← x.toGHSpace_rep, ← y.toGHSpace_rep, toGHSpace_eq_toGHSpace_iff_isometryEquiv]

Premises used: GromovHausdorff.toGHSpace_eq_toGHSpace_iff_isometryEquiv, GromovHausdorff.GHSpace.toGHSpace_rep
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
this : range Φ = range Ψ
T : ((↑(range Ψ) : Type) ≃ᵢ y.Rep) = ((↑(range Φ) : Type) ≃ᵢ y.Rep)
eΨ : (↑(range Φ) : Type) ≃ᵢ y.Rep
e : x.Rep ≃ᵢ y.Rep
⊢ Nonempty (x.Rep ≃ᵢ y.Rep)

Tactic:
⟨e⟩

Premises used: Nonempty.intro
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
x y : GHSpace
hxy : dist x y = 0
Φ : x.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : y.Rep → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Φisom : Isometry Φ
Ψisom : Isometry Ψ
DΦΨ : 0 = hausdorffDist (range Φ) (range Ψ)
this : range Φ = range Ψ
T : ((↑(range Ψ) : Type) ≃ᵢ y.Rep) = ((↑(range Φ) : Type) ≃ᵢ y.Rep)
eΨ : (↑(range Φ) : Type) ≃ᵢ y.Rep
e : x.Rep ≃ᵢ y.Rep
⊢ Nonempty (x.Rep ≃ᵢ y.Rep)

Tactic:
exact ⟨e⟩
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
p q : NonemptyCompacts X
⊢ Isometry.{u, u} (α := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))

Tactic:
have ha : Isometry ((↑) : p → X) := isometry_subtype_coe
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry.{u, u} (α := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
⊢ Isometry.{u, u} (α := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q))

Tactic:
have hb : Isometry ((↑) : q → X) := isometry_subtype_coe
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry.{u, u} (α := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
hb : Isometry.{u, u} (α := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q))
⊢ dist p q = hausdorffDist (↑p : Set X) (↑q : Set X)

Tactic:
have A : dist p q = hausdorffDist (p : Set X) q := rfl
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry.{u, u} (α := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
hb : Isometry.{u, u} (α := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q))
A : dist p q = hausdorffDist (↑p : Set X) (↑q : Set X)
⊢ (↑p : Set X) = range (ι := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))

Tactic:
have I : ↑p = range ((↑) : p → X) := Subtype.range_coe_subtype.symm
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry.{u, u} (α := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
hb : Isometry.{u, u} (α := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q))
A : dist p q = hausdorffDist (↑p : Set X) (↑q : Set X)
I : (↑p : Set X) = range (ι := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
⊢ (↑q : Set X) = range (ι := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q))

Tactic:
have J : ↑q = range ((↑) : q → X) := Subtype.range_coe_subtype.symm
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry.{u, u} (α := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
hb : Isometry.{u, u} (α := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q))
A : dist p q = hausdorffDist (↑p : Set X) (↑q : Set X)
I : (↑p : Set X) = range (ι := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
J : (↑q : Set X) = range (ι := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q))
rw :
  dist p.toGHSpace q.toGHSpace ≤
    hausdorffDist.{u} (α := X) (range (ι := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p)))
      (range (ι := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q)))
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q

Tactic:
rw [A, I, J]
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry.{u, u} (α := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
hb : Isometry.{u, u} (α := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q))
A : dist p q = hausdorffDist (↑p : Set X) (↑q : Set X)
I : (↑p : Set X) = range (ι := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
J : (↑q : Set X) = range (ι := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q))
⊢ dist p.toGHSpace q.toGHSpace ≤
    hausdorffDist.{u} (α := X) (range (ι := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p)))
      (range (ι := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q)))

Tactic:
ghDist_le_hausdorffDist ha hb

Premises used: GromovHausdorff.ghDist, setOf, GromovHausdorff.ghDist_le_hausdorffDist, TopologicalSpace.NonemptyCompacts.toGHSpace
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry.{u, u} (α := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
hb : Isometry.{u, u} (α := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q))
A : dist p q = hausdorffDist (↑p : Set X) (↑q : Set X)
I : (↑p : Set X) = range (ι := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p))
J : (↑q : Set X) = range (ι := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q))
⊢ dist p.toGHSpace q.toGHSpace ≤
    hausdorffDist.{u} (α := X) (range (ι := ↥p) (Subtype.val (p := fun (x : X) ↦ x ∈ p)))
      (range (ι := ↥q) (Subtype.val (p := fun (x : X) ↦ x ∈ q)))

Tactic:
exact ghDist_le_hausdorffDist ha hb

Premises used: GromovHausdorff.ghDist_le_hausdorffDist
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
⊢ LipschitzWith.{u, 0} (α := NonemptyCompacts X) 1 NonemptyCompacts.toGHSpace

Tactic:
LipschitzWith.mk_one ghDist_le_nonemptyCompacts_dist

Premises used: LipschitzWith.mk_one, GromovHausdorff.ghDist_le_nonemptyCompacts_dist
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
⊢ Continuous.{u, 0} (X := NonemptyCompacts X) NonemptyCompacts.toGHSpace

Tactic:
toGHSpace_lipschitz.continuous

Premises used: LipschitzWith.continuous, GromovHausdorff.toGHSpace_lipschitz
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃

Tactic:
le_of_forall_pos_le_add fun δ δ0 => ?_

Premises used: le_of_forall_pos_le_add
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
refine : ∀ (δ : ℝ) (δ0 : 0 < δ), ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃

Tactic:
refine le_of_forall_pos_le_add fun δ δ0 => ?_

Premises used: le_of_forall_pos_le_add
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
rcases : ∀ (xX : X), Membership.mem (γ := Set X) univ xX → ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ

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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
rcases : ∀ (xs : X) (hxs : xs ∈ s) (Dxs : dist xX xs ≤ ε₁), ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ

Tactic:
rcases hs xX with ⟨xs, hxs, Dxs⟩
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
⊢ s.Nonempty

Tactic:
have sne : s.Nonempty := ⟨xs, hxs⟩
-- 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
s : Set X
Φ : (↑s : Type u) → Y
ε₁ ε₂ ε₃ : ℝ
hs : ∀ (x : X), ∃ y ∈ s, dist x y ≤ ε₁
hs' : ∀ (x : Y), ∃ (y : (↑s : Type u)), dist x (Φ y) ≤ ε₃
H : ∀ (x y : (↑s : Type u)), |dist x y - dist (Φ x) (Φ y)| ≤ ε₂
δ : ℝ
δ0 : 0 < δ
xX : X
h : Membership.mem (γ := Set X) univ xX
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
⊢ 0 ≤ ε₂

Tactic:
have : 0 ≤ ε₂ := le_trans (abs_nonneg _) (H ⟨xs, hxs⟩ ⟨xs, hxs⟩)