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 : 0 ≤ ε₂
p q : (↑s : Type u)
linarith : 2 * (ε₂ / 2 + δ) < ε₂ → 2 / 2 = 1
linarith₁ linarith₂ : 2 * (ε₂ / 2 + δ) < ε₂ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₃ : 2 * (ε₂ / 2 + δ) < ε₂ → GT.gt (α := ℝ) 2 0
linarith₄ : 2 * (ε₂ / 2 + δ) < ε₂ → 4 * (0 - δ) + (HMul.hMul (α := ℝ) 1 2 * (1 * ε₂ + 2 * δ) - 2 * ε₂) = 0
linarith₅ : 2 * (ε₂ / 2 + δ) < ε₂ → GT.gt (α := ℝ) 4 0
⊢ ε₂ ≤ 2 * (ε₂ / 2 + δ)

Tactic:
linarith
-- 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 : 0 ≤ ε₂
⊢ ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)

Tactic:
have : ∀ p q : s, |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ) := fun p q =>
    calc
      |dist p q - dist (Φ p) (Φ q)| ≤ ε₂ := H p q
      _ ≤ 2 * (ε₂ / 2 + δ) := by linarith
-- 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 : ∀ (p q : (↑s : Type u)), |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ)
linarith : ε₂ / 2 + δ ≤ 0 → 2 / 2 = 1
linarith₁ : ε₂ / 2 + δ ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ε₂ / 2 + δ ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₃ : ε₂ / 2 + δ ≤ 0 → 2 * (0 - δ) + (0 - ε₂) + (1 * ε₂ + 2 * δ - HMul.hMul (α := ℝ) 2 0) = 0
linarith₄ : ε₂ / 2 + δ ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < ε₂ / 2 + δ

Tactic:
linarith
-- 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 : ∀ (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
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
⊢ Isometry Fl

Tactic:
have Il : Isometry Fl := Isometry.of_dist_eq fun x y => 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
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 : ∀ (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
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
⊢ Isometry Fr

Tactic:
have Ir : Isometry Fr := Isometry.of_dist_eq fun x y => 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
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 : ∀ (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
Fl : (val : X) → X ⊕ Y := inl
Fr : (val : Y) → X ⊕ Y := inr
Il : Isometry Fl
Ir : Isometry Fr
⊢ ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)

Tactic:
have : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr) := ghDist_le_hausdorffDist Il Ir
-- 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 : ghDist X Y ≤ hausdorffDist (range Fl) (range Fr)
⊢ hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)

Tactic:
have :
    hausdorffDist (range Fl) (range Fr) ≤
      hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr) :=
    have B : IsBounded (range Fl) := (isCompact_range Il.continuous).isBounded
    hausdorffDist_triangle
      (hausdorffEDist_ne_top_of_nonempty_of_bounded (range_nonempty _) (sne.image _) B
        (B.subset (image_subset_range _ _)))
-- 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 : hausdorffDist (range Fl) (range Fr) ≤ hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr)
⊢ hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)

Tactic:
have :
    hausdorffDist (Fl '' s) (range Fr) ≤
      hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr) :=
    have B : IsBounded (range Fr) := (isCompact_range Ir.continuous).isBounded
    hausdorffDist_triangle'
      (hausdorffEDist_ne_top_of_nonempty_of_bounded ((range_nonempty _).image _) (range_nonempty _)
        (B.subset (image_subset_range _ _)) B)
-- 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 :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
rw : hausdorffDist univ s ≤ ε₁
⊢ hausdorffDist (range Fl) (Fl '' s) ≤ ε₁

Tactic:
rw [← image_univ, hausdorffDist_image Il]

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 :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
⊢ 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 : 0 ≤ ε₁
x : X
h_2 : x ∈ s
⊢ 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 : 0 ≤ ε₁
⊢ hausdorffDist univ s ≤ ε₁

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

Premises used: Metric.hausdorffDist_le_of_mem_dist, And.intro, Exists.intro, Set.mem_univ
-- 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 :
  hausdorffDist (Fl '' s) (range Fr) ≤
    hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr)
⊢ hausdorffDist (range Fl) (Fl '' s) ≤ ε₁

Tactic:
have : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁ := by
    rw [← image_univ, hausdorffDist_image Il]
    have : 0 ≤ ε₁ := le_trans dist_nonneg Dxs
    refine hausdorffDist_le_of_mem_dist this (fun x _ => hs x) fun x _ =>
      ⟨x, mem_univ _, by simpa only [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 : hausdorffDist (range Fl) (Fl '' s) ≤ ε₁
linarith : ε₂ / 2 + δ < 0 → 2 / 2 = 1
linarith₁ : ε₂ / 2 + δ < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ε₂ / 2 + δ < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : ε₂ / 2 + δ < 0 → 2 * (0 - δ) + (0 - ε₂) + (1 * ε₂ + 2 * δ - HMul.hMul (α := ℝ) 2 0) = 0
linarith₄ : ε₂ / 2 + δ < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ ε₂ / 2 + δ

Tactic:
linarith
-- 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) ≤ ε₁
refine_1 : ∀ x_1 ∈ Fl '' s, ∃ y ∈ Fr '' range Φ, dist x_1 y ≤ ε₂ / 2 + δ
refine_2 : ∀ x_1 ∈ Fr '' range Φ, ∃ y ∈ Fl '' s, dist x_1 y ≤ ε₂ / 2 + δ
⊢ hausdorffDist (Fl '' s) (Fr '' range Φ) ≤ ε₂ / 2 + δ

Tactic:
refine hausdorffDist_le_of_mem_dist (by linarith) ?_ ?_

Premises used: Metric.hausdorffDist_le_of_mem_dist
-- 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' ∈ Fl '' s
refine_1 : ∀ (x_1 : X) (x_in_s : x_1 ∈ s) (xx' : Fl x_1 = x'), ∃ y ∈ Fr '' range Φ, dist x' y ≤ ε₂ / 2 + δ
⊢ ∃ y ∈ Fr '' range Φ, dist x' y ≤ ε₂ / 2 + δ

Tactic:
rcases (Set.mem_image _ _ _).1 hx' with ⟨x, ⟨x_in_s, xx'⟩⟩

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_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'
refine_1 : ∃ y ∈ Fr '' range Φ, dist (Fl x) y ≤ ε₂ / 2 + δ
⊢ ∃ y ∈ Fr '' range Φ, dist x' y ≤ ε₂ / 2 + δ

Tactic:
rw [← xx']
-- 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'
right : dist (Fl x) (Fr (Φ (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x x_in_s))) ≤ ε₂ / 2 + δ
⊢ ∃ y ∈ Fr '' range Φ, dist (Fl x) y ≤ ε₂ / 2 + δ

Tactic:
use Fr (Φ ⟨x, x_in_s⟩), mem_image_of_mem Fr (mem_range_self _)

Premises used: Set.mem_range_self, Subtype.mk, Set.mem_image_of_mem