awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
have this₁ : 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]⟩
-- 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
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) ≤ ε₁
⊢ 0 ≤ ε₂ / 2 + δ
have linarith : ε₂ / 2 + δ < 0 → 2 / 2 = 1
Tactic: linarith
-- 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
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
⊢ 0 ≤ ε₂ / 2 + δ
have linarith₁ : ε₂ / 2 + δ < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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
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
⊢ 0 ≤ ε₂ / 2 + δ
have linarith₂ : ε₂ / 2 + δ < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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
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
⊢ 0 ≤ ε₂ / 2 + δ
have linarith₃ : ε₂ / 2 + δ < 0 → 2 * (0 - δ) + (0 - ε₂) + (1 * ε₂ + 2 * δ - HMul.hMul (α := ℝ) 2 0) = 0
Tactic: linarith
-- 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
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 + δ
have refine_1 : ∀ x_1 ∈ Fl '' s, ∃ y ∈ Fr '' range Φ, dist x_1 y ≤ ε₂ / 2 + δ
Tactic: refine hausdorffDist_le_of_mem_dist (by linarith) ?_ ?_
-- 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
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 + δ
⊢ hausdorffDist (Fl '' s) (Fr '' range Φ) ≤ ε₂ / 2 + δ
have refine_2 : ∀ x_1 ∈ Fr '' range Φ, ∃ y ∈ Fl '' s, dist x_1 y ≤ ε₂ / 2 + δ
Tactic: refine hausdorffDist_le_of_mem_dist (by linarith) ?_ ?_
-- 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
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
⊢ ∃ y ∈ Fr '' range Φ, dist x' y ≤ ε₂ / 2 + δ
have refine_1 : ∀ (x_1 : X) (x_in_s : x_1 ∈ s) (xx' : Fl x_1 = x'), ∃ y ∈ Fr '' range Φ, dist x' y ≤ ε₂ / 2 + δ
Tactic: rcases (Set.mem_image _ _ _).1 hx' with ⟨x, ⟨x_in_s, xx'⟩⟩
-- 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
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'
⊢ ∃ y ∈ Fr '' range Φ, dist x' y ≤ ε₂ / 2 + δ
have refine_1 : ∃ y ∈ Fr '' range Φ, dist (Fl x) y ≤ ε₂ / 2 + δ
Tactic: rw [← xx']
-- 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
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'
⊢ ∃ y ∈ Fr '' range Φ, dist (Fl x) y ≤ ε₂ / 2 + δ
have right : dist (Fl x) (Fr (Φ (Subtype.mk (p := fun (x : X) ↦ x ∈ s) x x_in_s))) ≤ ε₂ / 2 + δ
Tactic: use Fr (Φ ⟨x, x_in_s⟩), mem_image_of_mem Fr (mem_range_self _)
-- 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
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 ∈ Fl '' s, dist x' y ≤ ε₂ / 2 + δ
have refine_2 : ∀ (y : Y) (y_in_s' : y ∈ range Φ) (yx' : Fr y = x'), ∃ y ∈ Fl '' s, dist x' y ≤ ε₂ / 2 + δ
Tactic: rcases (Set.mem_image _ _ _).1 hx' with ⟨y, ⟨y_in_s', yx'⟩⟩
-- 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
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'
⊢ ∃ y ∈ Fl '' s, dist x' y ≤ ε₂ / 2 + δ
have refine_2 : ∀ (x_1 : (↑s : Type u)) (xy : Φ x_1 = y), ∃ y ∈ Fl '' s, dist x' y ≤ ε₂ / 2 + δ
Tactic: rcases mem_range.1 y_in_s' with ⟨x, xy⟩
-- 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
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
⊢ ∃ y ∈ Fl '' s, dist x' y ≤ ε₂ / 2 + δ
have right : dist x' (Fl (↑x : X)) ≤ ε₂ / 2 + δ
Tactic: use Fl x, mem_image_of_mem _ x.2
-- 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
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 x' (Fl (↑x : X)) ≤ ε₂ / 2 + δ
have right : dist (Fl (↑x : X)) (Fr (Φ x)) ≤ ε₂ / 2 + δ
Tactic: rw [← yx', ← xy, dist_comm]
-- 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
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) ≤ ε₁
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ
have this₁ : 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)