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
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
h :
  (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
    p (NonemptyCompacts.kuratowskiEmbedding X)
refine_1 :
  ∀ (e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥p),
    ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))

Tactic:
rcases Setoid.symm h with ⟨e⟩

Premises used: Setoid.symm
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
h :
  (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
    p (NonemptyCompacts.kuratowskiEmbedding X)
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥p
refine_1 :
  ∀ (f : X ≃ᵢ ↥p), ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))

Tactic:
have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange.trans e
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
h :
  (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
    p (NonemptyCompacts.kuratowskiEmbedding X)
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥p
f : X ≃ᵢ ↥p
right :
  (range fun (x : X) ↦ (↑((f : (a : X) → ↥p) x) : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))

Tactic:
use fun x => f x, isometry_subtype_coe.comp f.isometry

Premises used: Isometry.comp, isometry_subtype_coe, DFunLike.coe, IsometryEquiv.isometry
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
h :
  (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
    p (NonemptyCompacts.kuratowskiEmbedding X)
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥p
f : X ≃ᵢ ↥p
right :
  image (α := ↥p) (Subtype.val (p := fun (x : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦ x ∈ p))
      (range (ι := X) (⇑f : (a : X) → ↥p)) =
    (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
right₁ :
  image (α := ↥p) (Subtype.val (p := fun (x : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦ x ∈ p)) univ =
    (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
right₂ :
  range (ι := ↥p) (Subtype.val (p := fun (x : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦ x ∈ p)) =
    (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
right₃ right₄ : (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ (range fun (x : X) ↦ (↑((f : (a : X) → ↥p) x) : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))

Tactic:
rw [range_comp', f.range_eq_univ, Set.image_univ, Subtype.range_coe]

Premises used: IsometryEquiv.range_eq_univ, Set.image_univ, Subtype.range_coe, Set.range_comp'
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
isomΨ : Isometry Ψ
rangeΨ : range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
refine_2 :
  ∀ (f : (↑(range Ψ) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type)),
    (IsometryRel.setoid :
        NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
      p (NonemptyCompacts.kuratowskiEmbedding X)
⊢ (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
    p (NonemptyCompacts.kuratowskiEmbedding X)

Tactic:
have f :=
      ((kuratowskiEmbedding.isometry X).isometryEquivOnRange.symm.trans
          isomΨ.isometryEquivOnRange).symm
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
isomΨ : Isometry Ψ
rangeΨ : range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
f : (↑(range Ψ) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type)
rw :
  ((↑(↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) : Type) ≃ᵢ
      ↥{ carrier := range (kuratowskiEmbedding X), isCompact' := ⋯, nonempty' := ⋯ :
          NonemptyCompacts ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) }) =
    (↥p ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type))
⊢ ((↑(range Ψ) : Type) ≃ᵢ
      ↥{ carrier := range (kuratowskiEmbedding X), isCompact' := ⋯, nonempty' := ⋯ :
          NonemptyCompacts ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) }) =
    (↥p ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type))

Tactic:
rw [rangeΨ]
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
isomΨ : Isometry Ψ
rangeΨ : range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
f : (↑(range Ψ) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type)
⊢ ((↑(↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) : Type) ≃ᵢ
      ↥{ carrier := range (kuratowskiEmbedding X), isCompact' := ⋯, nonempty' := ⋯ :
          NonemptyCompacts ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) }) =
    (↥p ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type))

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
isomΨ : Isometry Ψ
rangeΨ : range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
f : (↑(range Ψ) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type)
⊢ ((↑(range Ψ) : Type) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding X)) = (↥p ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type))

Tactic:
have E : (range Ψ ≃ᵢ NonemptyCompacts.kuratowskiEmbedding X)
        = (p ≃ᵢ range (kuratowskiEmbedding X)) := by
      dsimp only [NonemptyCompacts.kuratowskiEmbedding]; rw [rangeΨ]; rfl
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
isomΨ : Isometry Ψ
rangeΨ : range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
f : (↑(range Ψ) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type)
E :
  ((↑(range Ψ) : Type) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding X)) = (↥p ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type))
⊢ (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
    p (NonemptyCompacts.kuratowskiEmbedding X)

Tactic:
⟨cast E f⟩

Premises used: cast, Nonempty.intro, _private.0.GromovHausdorff.IsometryRel
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
isomΨ : Isometry Ψ
rangeΨ : range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
f : (↑(range Ψ) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type)
E :
  ((↑(range Ψ) : Type) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding X)) = (↥p ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type))
⊢ (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
    p (NonemptyCompacts.kuratowskiEmbedding X)

Tactic:
exact ⟨cast E f⟩
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
⊢ ⟦p⟧ = toGHSpace ↥p

Tactic:
eq_toGHSpace_iff.2 ⟨fun x => x, isometry_subtype_coe, Subtype.range_coe⟩

Premises used: Iff.mpr, Subtype.range_coe, And.intro, Exists.intro, isometry_subtype_coe, Subtype.val, GromovHausdorff.eq_toGHSpace_iff
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
p : GHSpace
⊢ CompactSpace p.Rep

Tactic:
inferInstanceAs <| CompactSpace p.out

Premises used: _private.0.GromovHausdorff.rep_gHSpace_compactSpace._proof_1
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
p : GHSpace
⊢ Nonempty p.Rep

Tactic:
inferInstanceAs <| Nonempty p.out

Premises used: _private.0.GromovHausdorff.rep_gHSpace_nonempty._proof_1
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
p : GHSpace
rw :
  ⟦Quot.out (r :=
        (⇑IsometryRel.setoid :
          NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop))
        p⟧ =
    p
⊢ toGHSpace
      ↥(Quot.out (r :=
          (⇑IsometryRel.setoid :
            NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop))
          p) =
    p

Tactic:
rw [← eq_toGHSpace]

Premises used: GromovHausdorff.eq_toGHSpace
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
p : GHSpace
⊢ ⟦Quot.out (r :=
        (⇑IsometryRel.setoid :
          NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop))
        p⟧ =
    p

Tactic:
Quot.out_eq p

Premises used: Quot.out_eq, GromovHausdorff.GHSpace, Quotient
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
p : GHSpace
⊢ ⟦Quot.out (r :=
        (⇑IsometryRel.setoid :
          NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop))
        p⟧ =
    p

Tactic:
exact Quot.out_eq p

Premises used: Quot.out_eq
-- 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
rw :
  (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
      (NonemptyCompacts.kuratowskiEmbedding X) (NonemptyCompacts.kuratowskiEmbedding Y) →
    Nonempty (X ≃ᵢ Y)
⊢ ⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧ → Nonempty (X ≃ᵢ Y)

Tactic:
rw [Quotient.eq]

Premises used: Quotient.eq
-- 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
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)
⊢ (↥{ carrier := range (kuratowskiEmbedding X), isCompact' := ⋯, nonempty' := ⋯ :
          NonemptyCompacts ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) } ≃ᵢ
      ↥{ carrier := range (kuratowskiEmbedding Y), isCompact' := ⋯, nonempty' := ⋯ :
          NonemptyCompacts ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) }) =
    ((↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type))

Tactic:
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
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)
⊢ (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)) =
    ((↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type))

Tactic:
have I :
      (NonemptyCompacts.kuratowskiEmbedding X ≃ᵢ NonemptyCompacts.kuratowskiEmbedding Y) =
        (range (kuratowskiEmbedding X) ≃ᵢ range (kuratowskiEmbedding Y)) := by
      dsimp only [NonemptyCompacts.kuratowskiEmbedding]; 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
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)
I :
  (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)) =
    ((↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type))
have : ∀ (f : X ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type)), Nonempty (X ≃ᵢ Y)
⊢ Nonempty (X ≃ᵢ Y)

Tactic:
have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange
-- 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
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)
I :
  (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)) =
    ((↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type))
f : X ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type)
have : ∀ (g : (↑(range (kuratowskiEmbedding Y)) : Type) ≃ᵢ Y), Nonempty (X ≃ᵢ Y)
⊢ Nonempty (X ≃ᵢ Y)

Tactic:
have g := (kuratowskiEmbedding.isometry Y).isometryEquivOnRange.symm
-- 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
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)
I :
  (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)) =
    ((↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type))
f : X ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type)
g : (↑(range (kuratowskiEmbedding Y)) : Type) ≃ᵢ Y
⊢ Nonempty (X ≃ᵢ Y)

Tactic:
⟨f.trans <| (cast I e).trans g⟩

Premises used: cast, Nonempty.intro, IsometryEquiv.trans
-- 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
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)
I :
  (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)) =
    ((↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type))
f : X ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type)
g : (↑(range (kuratowskiEmbedding Y)) : Type) ≃ᵢ Y
⊢ Nonempty (X ≃ᵢ Y)

Tactic:
exact ⟨f.trans <| (cast I e).trans g⟩
-- 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
e : X ≃ᵢ Y
have :
  ∀ (f : (↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ X),
    ⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧
⊢ ⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧

Tactic:
have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange.symm
-- 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
e : X ≃ᵢ Y
f : (↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ X
have :
  ∀ (g : Y ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type)),
    ⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧
⊢ ⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧

Tactic:
have g := (kuratowskiEmbedding.isometry Y).isometryEquivOnRange
-- 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
e : X ≃ᵢ Y
f : (↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ X
g : Y ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type)
⊢ ((↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type)) =
    (↥{ carrier := range (kuratowskiEmbedding X), isCompact' := ⋯, nonempty' := ⋯ :
          NonemptyCompacts ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) } ≃ᵢ
      ↥{ carrier := range (kuratowskiEmbedding Y), isCompact' := ⋯, nonempty' := ⋯ :
          NonemptyCompacts ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) })

Tactic:
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
e : X ≃ᵢ Y
f : (↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ X
g : Y ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type)
⊢ ((↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type)) =
    (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y))

Tactic:
have I :
      (range (kuratowskiEmbedding X) ≃ᵢ range (kuratowskiEmbedding Y)) =
        (NonemptyCompacts.kuratowskiEmbedding X ≃ᵢ NonemptyCompacts.kuratowskiEmbedding Y) := by
      dsimp only [NonemptyCompacts.kuratowskiEmbedding]; 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
e : X ≃ᵢ Y
f : (↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ X
g : Y ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type)
I :
  ((↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type)) =
    (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y))
rw :
  (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
    (NonemptyCompacts.kuratowskiEmbedding X) (NonemptyCompacts.kuratowskiEmbedding Y)
⊢ ⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧

Tactic:
rw [Quotient.eq]

Premises used: Quotient.eq
-- 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
e : X ≃ᵢ Y
f : (↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ X
g : Y ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type)
I :
  ((↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type)) =
    (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y))
⊢ (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
    (NonemptyCompacts.kuratowskiEmbedding X) (NonemptyCompacts.kuratowskiEmbedding Y)

Tactic:
⟨cast I ((f.trans e).trans g)⟩

Premises used: cast, Nonempty.intro, IsometryEquiv.trans, _private.0.GromovHausdorff.IsometryRel
-- 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
e : X ≃ᵢ Y
f : (↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ X
g : Y ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type)
I :
  ((↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type)) =
    (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y))
⊢ (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
    (NonemptyCompacts.kuratowskiEmbedding X) (NonemptyCompacts.kuratowskiEmbedding Y)

Tactic:
exact ⟨cast I ((f.trans e).trans g)⟩
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
p q : GHSpace
rw : dist p q = dist (toGHSpace p.Rep) (toGHSpace q.Rep)
rw₁ : dist p q = dist p (toGHSpace q.Rep)
rw₂ rw₃ : dist p q = dist p q
⊢ dist p q = ghDist p.Rep q.Rep

Tactic:
rw [ghDist, p.toGHSpace_rep, q.toGHSpace_rep]

Premises used: GromovHausdorff.ghDist, GromovHausdorff.GHSpace.toGHSpace_rep
-- 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 Ψ
rcases : ∀ (xX : X), Membership.mem (γ := Set X) univ xX → ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
⊢ ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)

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
γ : 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) ⋯
⊢ Isometry Φ'

Tactic:
have IΦ' : Isometry Φ' := fun x y => ha x y
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
γ : 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 Φ'
⊢ Isometry Ψ'

Tactic:
have IΨ' : Isometry Ψ' := fun x y => hb x y
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
Y : Type v
inst_3 : MetricSpace Y
inst_4 : CompactSpace Y
inst_5 : Nonempty Y
γ : 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 Ψ'
⊢ IsCompact s

Tactic:
have : IsCompact s := (isCompact_range ha.continuous).union (isCompact_range hb.continuous)
-- 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 : IsCompact s
⊢ CompactSpace.{w} (↑s : Type w)

Tactic:
have : CompactSpace s := ⟨isCompact_iff_isCompact_univ.1 ‹IsCompact s›⟩
-- 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) ∘ Φ'

Tactic:
have ΦΦ' : Φ = Subtype.val ∘ Φ' := rfl