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
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
⊢ (range fun (x : X) ↦ (↑((f : (a : X) → ↥p) x) : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
have right : image (α := ↥p) (Subtype.val (p := fun (x : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦ x ∈ p)) (range (ι := X) (⇑f : (a : X) → ↥p)) =
  (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Tactic: rw [range_comp', f.range_eq_univ, Set.image_univ, Subtype.range_coe]
-- 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
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 : ℕ) ↦ ℝ) ∞))
⊢ (range fun (x : X) ↦ (↑((f : (a : X) → ↥p) x) : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
have right₁ : image (α := ↥p) (Subtype.val (p := fun (x : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦ x ∈ p)) univ =
  (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Tactic: rw [range_comp', f.range_eq_univ, Set.image_univ, Subtype.range_coe]
-- 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
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 : ℕ) ↦ ℝ) ∞))
⊢ (range fun (x : X) ↦ (↑((f : (a : X) → ↥p) x) : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
have right₂ : range (ι := ↥p) (Subtype.val (p := fun (x : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) ↦ x ∈ p)) = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Tactic: rw [range_comp', f.range_eq_univ, Set.image_univ, Subtype.range_coe]
-- 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
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 : ℕ) ↦ ℝ) ∞))
⊢ (range fun (x : X) ↦ (↑((f : (a : X) → ↥p) x) : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
have right₃ : (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Tactic: rw [range_comp', f.range_eq_univ, Set.image_univ, Subtype.range_coe]
-- 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
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
isomΨ : Isometry Ψ
rangeΨ : range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
    p (NonemptyCompacts.kuratowskiEmbedding X)
have refine_2 : ∀ (f : (↑(range Ψ) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type)),
  (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
-- 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
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) ≃ᵢ
      ↥{ carrier := range (kuratowskiEmbedding X), isCompact' := ⋯, nonempty' := ⋯ :
          NonemptyCompacts ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) }) =
    (↥p ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type))
have rw : ((↑(↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)) : Type) ≃ᵢ
    ↥{ carrier := range (kuratowskiEmbedding X), isCompact' := sorry, nonempty' := sorry :
        NonemptyCompacts ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) }) =
  (↥p ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type))
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
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)
⊢ (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
    p (NonemptyCompacts.kuratowskiEmbedding X)
have E : ((↑(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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
p : GHSpace
⊢ toGHSpace
      ↥(Quot.out (r :=
          (⇑IsometryRel.setoid :
            NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop))
          p) =
    p
have rw : ⟦Quot.out (r :=
      (⇑IsometryRel.setoid :
        NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop))
      p⟧ =
  p
Tactic: rw [← eq_toGHSpace]
-- 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
⊢ ⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧ → Nonempty (X ≃ᵢ Y)
have rw : (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
    (NonemptyCompacts.kuratowskiEmbedding X) (NonemptyCompacts.kuratowskiEmbedding Y) →
  Nonempty (X ≃ᵢ Y)
Tactic: rw [Quotient.eq]
-- 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
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)
⊢ Nonempty (X ≃ᵢ Y)
have I : (↥(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
-- 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
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)
I :
  (↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥(NonemptyCompacts.kuratowskiEmbedding Y)) =
    ((↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type))
⊢ Nonempty (X ≃ᵢ Y)
have have : ∀ (f : X ≃ᵢ (↑(range (kuratowskiEmbedding X)) : Type)), Nonempty (X ≃ᵢ Y)
Tactic: have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange
-- 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
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)
⊢ Nonempty (X ≃ᵢ Y)
have have : ∀ (g : (↑(range (kuratowskiEmbedding Y)) : Type) ≃ᵢ Y), Nonempty (X ≃ᵢ Y)
Tactic: have g := (kuratowskiEmbedding.isometry Y).isometryEquivOnRange.symm
-- 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
e : X ≃ᵢ Y
⊢ ⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧
have have : ∀ (f : (↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ X),
  ⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧
Tactic: have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange.symm
-- 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
e : X ≃ᵢ Y
f : (↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ X
⊢ ⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧
have have : ∀ (g : Y ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type)),
  ⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧
Tactic: have g := (kuratowskiEmbedding.isometry Y).isometryEquivOnRange
-- 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
e : X ≃ᵢ Y
f : (↑(range (kuratowskiEmbedding X)) : Type) ≃ᵢ X
g : Y ≃ᵢ (↑(range (kuratowskiEmbedding Y)) : Type)
⊢ ⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧
have I : ((↑(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
-- 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
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))
⊢ ⟦NonemptyCompacts.kuratowskiEmbedding X⟧ = ⟦NonemptyCompacts.kuratowskiEmbedding Y⟧
have rw : (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
  (NonemptyCompacts.kuratowskiEmbedding X) (NonemptyCompacts.kuratowskiEmbedding Y)
Tactic: rw [Quotient.eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
p q : GHSpace
⊢ dist p q = ghDist p.Rep q.Rep
have rw : dist p q = dist (toGHSpace p.Rep) (toGHSpace q.Rep)
Tactic: rw [ghDist, p.toGHSpace_rep, q.toGHSpace_rep]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
p q : GHSpace
rw : dist p q = dist (toGHSpace p.Rep) (toGHSpace q.Rep)
⊢ dist p q = ghDist p.Rep q.Rep
have rw₁ : dist p q = dist p (toGHSpace q.Rep)
Tactic: rw [ghDist, p.toGHSpace_rep, q.toGHSpace_rep]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
p q : GHSpace
rw : dist p q = dist (toGHSpace p.Rep) (toGHSpace q.Rep)
rw₁ : dist p q = dist p (toGHSpace q.Rep)
⊢ dist p q = ghDist p.Rep q.Rep
have rw₂ : dist p q = dist p q
Tactic: rw [ghDist, p.toGHSpace_rep, q.toGHSpace_rep]
-- 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 Ψ
⊢ ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
have rcases : ∀ (xX : X), Membership.mem (γ := Set X) univ xX → ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
Tactic: rcases exists_mem_of_nonempty X with ⟨xX, _⟩
-- 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) ⋯
⊢ ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
have IΦ' : Isometry Φ'
Tactic: have IΦ' : Isometry Φ' := fun x y => ha x y
-- 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 Φ'
⊢ ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
have IΨ' : Isometry Ψ'
Tactic: have IΨ' : Isometry Ψ' := fun x y => hb x y
-- 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 Ψ'
⊢ ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
have this : IsCompact s
Tactic: have : IsCompact s := (isCompact_range ha.continuous).union (isCompact_range hb.continuous)
-- 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 : IsCompact s
⊢ ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
have this₁ : CompactSpace.{w} (↑s : Type w)
Tactic: have : CompactSpace s := ⟨isCompact_iff_isCompact_univ.1 ‹IsCompact s›⟩
-- 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 : CompactSpace.{w} (↑s : Type w)
⊢ ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
have ΦΦ' : Φ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Φ'
Tactic: have ΦΦ' : Φ = Subtype.val ∘ Φ' := rfl
-- 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 : CompactSpace.{w} (↑s : Type w)
ΦΦ' : Φ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Φ'
⊢ ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
have ΨΨ' : Ψ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Ψ'
Tactic: have ΨΨ' : Ψ = Subtype.val ∘ Ψ' := rfl
-- 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 : CompactSpace.{w} (↑s : Type w)
ΦΦ' : Φ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Φ'
ΨΨ' : Ψ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Ψ'
⊢ hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
have rw : hausdorffDist (Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' range Φ')
    (Subtype.val (p := fun (x : γ) ↦ x ∈ s) '' range Ψ') =
  hausdorffDist (range Φ') (range Ψ')
Tactic: rw [ΦΦ', ΨΨ', range_comp, range_comp]
-- 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 : CompactSpace.{w} (↑s : Type w)
ΦΦ' : Φ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Φ'
ΨΨ' : Ψ = Subtype.val (p := fun (x : γ) ↦ x ∈ s) ∘ Ψ'
⊢ ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
have this₁ : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
Tactic: have : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ') := by
    rw [ΦΦ', ΨΨ', range_comp, range_comp]
    exact hausdorffDist_image isometry_subtype_coe
-- 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 : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
⊢ ghDist X Y ≤ hausdorffDist (range Φ) (range Ψ)
have rw : ghDist X Y ≤ hausdorffDist (range Φ') (range Ψ')
Tactic: rw [this]
-- 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 : hausdorffDist (range Φ) (range Ψ) = hausdorffDist (range Φ') (range Ψ')
F : (↑s : Type w) → ↥(lp (fun (x : ℕ) ↦ ℝ) ∞) := kuratowskiEmbedding (↑s : Type w)
⊢ ghDist X Y ≤ hausdorffDist (range Φ') (range Ψ')
have this₁ : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ')
Tactic: have : hausdorffDist (F '' range Φ') (F '' range Ψ') = hausdorffDist (range Φ') (range Ψ') :=
    hausdorffDist_image (kuratowskiEmbedding.isometry _)