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
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) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x_1 : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this_3 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this_4 : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this_5 :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
x' : X ⊕ Y
hx' : x' ∈ Fl '' s
x : X
x_in_s : x ∈ s
xx' : Fl x = x'
⊢ dist (Fl x) (Fr (Φ (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x x_in_s))) ≤ ε₂ / 2 + δ

Tactic:
le_of_eq (glueDist_glued_points (fun x : s => (x : X)) Φ (ε₂ / 2 + δ) ⟨x, x_in_s⟩)

Premises used: Metric.glueDist_glued_points, HDiv.hDiv, Subtype.mk, HAdd.hAdd, le_of_eq, OfNat.ofNat, Subtype.val
-- 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) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x_1 : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this_3 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this_4 : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this_5 :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
x' : X ⊕ Y
hx' : x' ∈ Fl '' s
x : X
x_in_s : x ∈ s
xx' : Fl x = x'
⊢ dist (Fl x) (Fr (Φ (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x x_in_s))) ≤ ε₂ / 2 + δ

Tactic:
exact le_of_eq (glueDist_glued_points (fun x : s => (x : X)) Φ (ε₂ / 2 + δ) ⟨x, x_in_s⟩)

Premises used: Metric.glueDist_glued_points, HDiv.hDiv, Subtype.mk, HAdd.hAdd, le_of_eq, OfNat.ofNat, Subtype.val
-- 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) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this_3 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this_4 : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this_5 :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
x' : X ⊕ Y
hx' : x' ∈ Fr '' range Φ
refine_2 : ∀ (y : Y) (y_in_s' : y ∈ range Φ) (yx' : Fr y = x'), ∃ y ∈ Fl '' s, dist x' y ≤ ε₂ / 2 + δ
⊢ ∃ y ∈ Fl '' s, dist x' y ≤ ε₂ / 2 + δ

Tactic:
rcases (Set.mem_image _ _ _).1 hx' with ⟨y, ⟨y_in_s', yx'⟩⟩

Premises used: Set.mem_image, Iff.mp
-- 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) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this_3 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this_4 : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this_5 :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
x' : X ⊕ Y
hx' : x' ∈ Fr '' range Φ
y : Y
y_in_s' : y ∈ range Φ
yx' : Fr y = x'
refine_2 : ∀ (x_1 : (↑s : Type u)) (xy : Φ x_1 = y), ∃ y ∈ Fl '' s, dist x' y ≤ ε₂ / 2 + δ
⊢ ∃ y ∈ Fl '' s, dist x' y ≤ ε₂ / 2 + δ

Tactic:
rcases mem_range.1 y_in_s' with ⟨x, xy⟩

Premises used: Set.mem_range, Iff.mp
-- 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) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x_1 : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this_3 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this_4 : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this_5 :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
x' : X ⊕ Y
hx' : x' ∈ Fr '' range Φ
y : Y
y_in_s' : y ∈ range Φ
yx' : Fr y = x'
x : (↑s : Type u)
xy : Φ x = y
right : dist x' (Fl (↑x : X)) ≤ ε₂ / 2 + δ
⊢ ∃ y ∈ Fl '' s, dist x' y ≤ ε₂ / 2 + δ

Tactic:
use Fl x, mem_image_of_mem _ x.2

Premises used: Set.mem_image_of_mem, Subtype.val, Subtype.property
-- 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) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x_1 : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this_3 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this_4 : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this_5 :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
x' : X ⊕ Y
hx' : x' ∈ Fr '' range Φ
y : Y
y_in_s' : y ∈ range Φ
yx' : Fr y = x'
x : (↑s : Type u)
xy : Φ x = y
right : dist (Fl (↑x : X)) (Fr (Φ x)) ≤ ε₂ / 2 + δ
⊢ dist x' (Fl (↑x : X)) ≤ ε₂ / 2 + δ

Tactic:
rw [← yx', ← xy, dist_comm]

Premises used: dist_comm
-- 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) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x_1 : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this_3 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this_4 : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this_5 :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
x' : X ⊕ Y
hx' : x' ∈ Fr '' range Φ
y : Y
y_in_s' : y ∈ range Φ
yx' : Fr y = x'
x : (↑s : Type u)
xy : Φ x = y
⊢ dist (Fl (↑x : X)) (Fr (Φ x)) ≤ ε₂ / 2 + δ

Tactic:
le_of_eq (glueDist_glued_points (Z := s) Subtype.val Φ (ε₂ / 2 + δ) x)

Premises used: Metric.glueDist_glued_points, HDiv.hDiv, HAdd.hAdd, le_of_eq, OfNat.ofNat, Subtype.val
-- 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) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x_1 : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this_3 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this_4 : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this_5 :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
x' : X ⊕ Y
hx' : x' ∈ Fr '' range Φ
y : Y
y_in_s' : y ∈ range Φ
yx' : Fr y = x'
x : (↑s : Type u)
xy : Φ x = y
⊢ dist (Fl (↑x : X)) (Fr (Φ x)) ≤ ε₂ / 2 + δ

Tactic:
exact le_of_eq (glueDist_glued_points (Z := s) Subtype.val Φ (ε₂ / 2 + δ) x)

Premises used: Metric.glueDist_glued_points, HDiv.hDiv, HAdd.hAdd, le_of_eq, OfNat.ofNat, Subtype.val
-- 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) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this_3 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this_4 : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this_5 :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
⊢ hausdorffDist (Fl '' s) (Fr '' range Φ) ≤ ε₂ / 2 + δ

Tactic:
have : hausdorffDist (Fl '' s) (Fr '' range Φ) ≤ ε₂ / 2 + δ := by
    refine hausdorffDist_le_of_mem_dist (by linarith) ?_ ?_
    · intro x' hx'
      rcases (Set.mem_image _ _ _).1 hx' with ⟨x, ⟨x_in_s, xx'⟩⟩
      rw [← xx']
      use Fr (Φ ⟨x, x_in_s⟩), mem_image_of_mem Fr (mem_range_self _)
      exact le_of_eq (glueDist_glued_points (fun x : s => (x : X)) Φ (ε₂ / 2 + δ) ⟨x, x_in_s⟩)
    · intro x' hx'
      rcases (Set.mem_image _ _ _).1 hx' with ⟨y, ⟨y_in_s', yx'⟩⟩
      rcases mem_range.1 y_in_s' with ⟨x, xy⟩
      use Fl x, mem_image_of_mem _ x.2
      rw [← yx', ← xy, dist_comm]
      exact le_of_eq (glueDist_glued_points (Z := s) Subtype.val Φ (ε₂ / 2 + δ) x)
-- 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) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this_3 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this_4 : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this_5 :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this_6 : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
this : hausdorffDist (Fl '' s) (Fr '' range Φ) ≤ ε₂ / 2 + δ
rw : hausdorffDist (range Φ) univ ≤ ε₃
⊢ hausdorffDist (Fr '' range Φ) (range Fr) ≤ ε₃

Tactic:
rw [← @image_univ _ _ Fr, hausdorffDist_image Ir]

Premises used: Set.image_univ, Metric.hausdorffDist_image
-- 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) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this_3 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this_4 : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this_5 :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this_6 : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
this : hausdorffDist (Fl '' s) (Fr '' range Φ) ≤ ε₂ / 2 + δ
rcases : ∀ (xY : Y), Membership.mem (γ := Set Y) univ xY → hausdorffDist (range Φ) univ ≤ ε₃
⊢ hausdorffDist (range Φ) univ ≤ ε₃

Tactic:
rcases exists_mem_of_nonempty Y with ⟨xY, _⟩

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
xs : X
hxs : xs ∈ s
Dxs : dist xX xs ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this_3 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this_4 : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this_5 :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this_6 : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
this : hausdorffDist (Fl '' s) (Fr '' range Φ) ≤ ε₂ / 2 + δ
xY : Y
h_2 : Membership.mem (γ := Set Y) univ xY
rcases : ∀ (xs' : (↑s : Type u)) (Dxs' : dist xY (Φ xs') ≤ ε₃), hausdorffDist (range Φ) univ ≤ ε₃
⊢ hausdorffDist (range Φ) univ ≤ ε₃

Tactic:
rcases hs' xY with ⟨xs', 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 ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this_3 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this_4 : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this_5 :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this_6 : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
this : hausdorffDist (Fl '' s) (Fr '' range Φ) ≤ ε₂ / 2 + δ
xY : Y
h_2 : Membership.mem (γ := Set Y) univ xY
xs' : (↑s : Type u)
Dxs' : dist xY (Φ xs') ≤ ε₃
⊢ 0 ≤ ε₃

Tactic:
have : 0 ≤ ε₃ := le_trans dist_nonneg 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 ≤ ε₁
sne : s.Nonempty
h_1 : Nonempty.{u + 1} (↑s : Type u) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x_1 : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this_3 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this_4 : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this_5 :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this_6 : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
this_7 : hausdorffDist (Fl '' s) (Fr '' range Φ) ≤ ε₂ / 2 + δ
xY : Y
h_2 : Membership.mem (γ := Set Y) univ xY
xs' : (↑s : Type u)
Dxs' : dist xY (Φ xs') ≤ ε₃
this : 0 ≤ ε₃
x : Y
h_3 : x ∈ range Φ
⊢ dist x x ≤ ε₃

Tactic:
simpa only [dist_self]

Premises used: dist_self
-- 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) := ⋯
this_1 : 0 ≤ ε₂
this_2 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
x : MetricSpace (X ⊕ Y) :=
  glueMetricApprox (fun (x : (↑s : Type u)) ↦ (↑x : X)) (fun (x : (↑s : Type u)) ↦ Φ x) (ε₂ / 2 + δ) ⋯ this_2
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
this_3 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
this_4 : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
this_5 :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
this_6 : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
this_7 : hausdorffDist (Fl '' s) (Fr '' range Φ) ≤ ε₂ / 2 + δ
xY : Y
h_2 : Membership.mem (γ := Set Y) univ xY
xs' : (↑s : Type u)
Dxs' : dist xY (Φ xs') ≤ ε₃
this : 0 ≤ ε₃
refine : ∀ (x : Y), Membership.mem (γ := Set Y) univ x → ∃ y ∈ range Φ, dist x y ≤ ε₃
⊢ hausdorffDist (range Φ) univ ≤ ε₃

Tactic:
refine hausdorffDist_le_of_mem_dist this
      (fun x _ => ⟨x, mem_univ _, by simpa only [dist_self]⟩)
      fun x _ => ?_

Premises used: Metric.hausdorffDist_le_of_mem_dist, And.intro, Exists.intro, Set.mem_univ