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_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 : Membership.mem (γ := Set Y) univ x
rcases : ∀ (y : (↑s : Type u)) (Dy : dist x (Φ y) ≤ ε₃), ∃ y ∈ range Φ, dist x y ≤ ε₃
⊢ ∃ y ∈ range Φ, dist x y ≤ ε₃

Tactic:
rcases hs' x with ⟨y, Dy⟩
-- 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 : Membership.mem (γ := Set Y) univ x
y : (↑s : Type u)
Dy : dist x (Φ y) ≤ ε₃
⊢ ∃ y ∈ range Φ, dist x y ≤ ε₃

Tactic:
⟨Φ y, mem_range_self _, Dy⟩

Premises used: Set.mem_range_self, And.intro, Exists.intro
-- 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 : Membership.mem (γ := Set Y) univ x
y : (↑s : Type u)
Dy : dist x (Φ y) ≤ ε₃
⊢ ∃ y ∈ range Φ, dist x y ≤ ε₃

Tactic:
exact ⟨Φ y, mem_range_self _, Dy⟩
-- 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 + δ
⊢ hausdorffDist (Fr '' range Φ) (range Fr) ≤ ε₃

Tactic:
have : hausdorffDist (Fr '' range Φ) (range Fr) ≤ ε₃ := by
    rw [← @image_univ _ _ Fr, hausdorffDist_image Ir]
    rcases exists_mem_of_nonempty Y with ⟨xY, _⟩
    rcases hs' xY with ⟨xs', Dxs'⟩
    have : 0 ≤ ε₃ := le_trans dist_nonneg Dxs'
    refine hausdorffDist_le_of_mem_dist this
      (fun x _ => ⟨x, mem_univ _, by simpa only [dist_self]⟩)
      fun x _ => ?_
    rcases hs' x with ⟨y, Dy⟩
    exact ⟨Φ y, mem_range_self _, Dy⟩
-- 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 + δ
this : hausdorffDist (Fr '' range Φ) (range Fr) ≤ ε₃
linarith : ε₁ + ε₂ / 2 + ε₃ + δ < ghDist X Y → 2 / 2 = 1
linarith₁ : ε₁ + ε₂ / 2 + ε₃ + δ < ghDist X Y → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : ε₁ + ε₂ / 2 + ε₃ + δ < ghDist X Y → GT.gt (α := ℝ) 2 0
linarith₃ : ε₁ + ε₂ / 2 + ε₃ + δ < ghDist X Y → 2 / 2 = 1
linarith₄ : ε₁ + ε₂ / 2 + ε₃ + δ < ghDist X Y → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : ε₁ + ε₂ / 2 + ε₃ + δ < ghDist X Y → GT.gt (α := ℝ) 2 0
linarith₆ :
  ε₁ + ε₂ / 2 + ε₃ + δ < ghDist X Y →
    2 * (ghDist X Y - hausdorffDist (range Fl) (range Fr)) +
                  2 *
                    (hausdorffDist (range Fl) (range Fr) -
                      (hausdorffDist (range Fl) (Fl '' s) + hausdorffDist (Fl '' s) (range Fr))) +
                2 *
                  (hausdorffDist (Fl '' s) (range Fr) -
                    (hausdorffDist (Fl '' s) (Fr '' range Φ) + hausdorffDist (Fr '' range Φ) (range Fr))) +
              2 * (hausdorffDist (range Fl) (Fl '' s) - ε₁) +
            (2 * hausdorffDist (Fl '' s) (Fr '' range Φ) - (1 * ε₂ + 2 * δ)) +
          2 * (hausdorffDist (Fr '' range Φ) (range Fr) - ε₃) +
        (2 * ε₁ + 1 * ε₂ + 2 * ε₃ + 2 * δ - 2 * ghDist X Y) =
      0
linarith₇ linarith₈ linarith₉ linarith₁₀ linarith₁₁ : ε₁ + ε₂ / 2 + ε₃ + δ < ghDist X Y → GT.gt (α := ℝ) 2 0
⊢ ghDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ + δ

Tactic:
linarith
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
⊢ SecondCountableTopology GHSpace

Tactic:
secondCountable_of_countable_discretization fun δ δpos => ?_

Premises used: Metric.secondCountable_of_countable_discretization
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
refine :
  ∀ (δ : ℝ) (δpos : δ > 0),
    ∃ (β : Type) (x : Encodable β) (F : GHSpace → β), ∀ (x y : GHSpace), F x = F y → dist x y ≤ δ
⊢ SecondCountableTopology GHSpace

Tactic:
refine secondCountable_of_countable_discretization fun δ δpos => ?_

Premises used: Metric.secondCountable_of_countable_discretization
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
⊢ 0 < 2 / 5

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
⊢ 0 < ε

Tactic:
have εpos : 0 < ε := mul_pos (by simp) δpos
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
p : GHSpace
⊢ ∃ (s : Set p.Rep), s.Finite ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s, ball x ε)

Tactic:
simpa only [subset_univ, true_and] using
      finite_cover_balls_of_compact (X := p.Rep) isCompact_univ εpos

Premises used: Set.subset_univ, finite_cover_balls_of_compact, isCompact_univ, true_and
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
⊢ ∀ (p : GHSpace), ∃ (s : Set p.Rep), s.Finite ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s, ball x ε)

Tactic:
have (p : GHSpace) : ∃ s : Set p.Rep, s.Finite ∧ univ ⊆ ⋃ x ∈ s, ball x ε := by
    simpa only [subset_univ, true_and] using
      finite_cover_balls_of_compact (X := p.Rep) isCompact_univ εpos
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
this : ∀ (p : GHSpace), ∃ (s : Set p.Rep), s.Finite ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s, ball x ε)
choose :
  ∀ (s : (p : GHSpace) → Set p.Rep)
    (hs : ∀ (p : GHSpace), (s p).Finite ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x ε)),
    ∃ (β : Type) (x : Encodable β) (F : GHSpace → β), ∀ (x y : GHSpace), F x = F y → dist x y ≤ δ
⊢ ∃ (β : Type) (x : Encodable β) (F : GHSpace → β), ∀ (x y : GHSpace), F x = F y → dist x y ≤ δ

Tactic:
choose s hs using this
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x ε)
N : (p : GHSpace) → ℕ := fun (p : GHSpace) ↦ Nat.card (↑(s p) : Type)
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (Nat.card (↑(s p) : Type)) :=
  fun (p : GHSpace) ↦ Finite.equivFin (↑(s p) : Type)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (N p) fun (a b : Fin (N p)) ↦
      ⌊ε⁻¹ *
          dist (α := (↑(s p) : Type))
            (((E p).symm : (a : Fin (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) a : (↑(s p) : Type))
            (((E p).symm : (a : Fin (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋
⊢ ∃ (β : Type) (x : Encodable β) (F : GHSpace → β), ∀ (x y : GHSpace), F x = F y → dist x y ≤ δ

Tactic:
⟨Σ n, Fin n → Fin n → ℤ, inferInstance, F, fun p q hpq => ?_⟩

Premises used: inferInstance, Exists.intro, Sigma
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x ε)
N : (p : GHSpace) → ℕ := fun (p : GHSpace) ↦ Nat.card (↑(s p) : Type)
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (Nat.card (↑(s p) : Type)) :=
  fun (p : GHSpace) ↦ Finite.equivFin (↑(s p) : Type)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (N p) fun (a b : Fin (N p)) ↦
      ⌊ε⁻¹ *
          dist (α := (↑(s p) : Type))
            (((E p).symm : (a : Fin (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) a : (↑(s p) : Type))
            (((E p).symm : (a : Fin (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋
refine : ∀ (p q : GHSpace) (hpq : F p = F q), dist p q ≤ δ
⊢ ∃ (β : Type) (x : Encodable β) (F : GHSpace → β), ∀ (x y : GHSpace), F x = F y → dist x y ≤ δ

Tactic:
refine ⟨Σ n, Fin n → Fin n → ℤ, inferInstance, F, fun p q hpq => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x ε)
N : (p : GHSpace) → ℕ := fun (p : GHSpace) ↦ Nat.card (↑(s p) : Type)
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (Nat.card (↑(s p) : Type)) :=
  fun (p : GHSpace) ↦ Finite.equivFin (↑(s p) : Type)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (N p) fun (a b : Fin (N p)) ↦
      ⌊ε⁻¹ *
          dist (α := (↑(s p) : Type))
            (((E p).symm : (a : Fin (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) a : (↑(s p) : Type))
            (((E p).symm : (a : Fin (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋
p q : GHSpace
hpq : F p = F q
⊢ N p = N q

Tactic:
have Npq : N p = N q := (Sigma.mk.inj_iff.1 hpq).1
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x ε)
N : (p : GHSpace) → ℕ := fun (p : GHSpace) ↦ Nat.card (↑(s p) : Type)
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (Nat.card (↑(s p) : Type)) :=
  fun (p : GHSpace) ↦ Finite.equivFin (↑(s p) : Type)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (N p) fun (a b : Fin (N p)) ↦
      ⌊ε⁻¹ *
          dist (α := (↑(s p) : Type))
            (((E p).symm : (a : Fin (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) a : (↑(s p) : Type))
            (((E p).symm : (a : Fin (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : (↑(s p) : Type) → (↑(s q) : Type) :=
  fun (x : (↑(s p) : Type)) ↦
    ((E q).symm : (a : Fin (Nat.card (↑(s q) : Type))) → (↑(s q) : Type))
      (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x))
Φ : (↑(s p) : Type) → q.Rep := fun (x : (↑(s p) : Type)) ↦ (↑(Ψ x) : q.Rep)
refine_1 : ∀ (x : p.Rep), ∃ y ∈ s p, dist x y ≤ ε
refine_2 : ∀ (x : q.Rep), ∃ (y : (↑(s p) : Type)), dist x (Φ y) ≤ ε
refine_3 : ∀ (x y : (↑(s p) : Type)), |dist x y - dist (Φ x) (Φ y)| ≤ ε
⊢ ghDist p.Rep q.Rep ≤ ε + ε / 2 + ε

Tactic:
refine ghDist_le_of_approx_subsets Φ ?_ ?_ ?_

Premises used: GromovHausdorff.ghDist_le_of_approx_subsets
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x ε)
N : (p : GHSpace) → ℕ := fun (p : GHSpace) ↦ Nat.card (↑(s p) : Type)
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (Nat.card (↑(s p) : Type)) :=
  fun (p : GHSpace) ↦ Finite.equivFin (↑(s p) : Type)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (N p) fun (a b : Fin (N p)) ↦
      ⌊ε⁻¹ *
          dist (α := (↑(s p) : Type))
            (((E p).symm : (a : Fin (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) a : (↑(s p) : Type))
            (((E p).symm : (a : Fin (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : (↑(s p) : Type) → (↑(s q) : Type) :=
  fun (x : (↑(s p) : Type)) ↦
    ((E q).symm : (a : Fin (Nat.card (↑(s q) : Type))) → (↑(s q) : Type))
      (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x))
Φ : (↑(s p) : Type) → q.Rep := fun (x : (↑(s p) : Type)) ↦ (↑(Ψ x) : q.Rep)
x : p.Rep
⊢ Membership.mem (γ := Set p.Rep) (⋃ y ∈ s p, ball y ε) x

Tactic:
have : x ∈ ⋃ y ∈ s p, ball y ε := (hs p).2 (mem_univ _)
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x ε)
N : (p : GHSpace) → ℕ := fun (p : GHSpace) ↦ Nat.card (↑(s p) : Type)
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (Nat.card (↑(s p) : Type)) :=
  fun (p : GHSpace) ↦ Finite.equivFin (↑(s p) : Type)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (N p) fun (a b : Fin (N p)) ↦
      ⌊ε⁻¹ *
          dist (α := (↑(s p) : Type))
            (((E p).symm : (a : Fin (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) a : (↑(s p) : Type))
            (((E p).symm : (a : Fin (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : (↑(s p) : Type) → (↑(s q) : Type) :=
  fun (x : (↑(s p) : Type)) ↦
    ((E q).symm : (a : Fin (Nat.card (↑(s q) : Type))) → (↑(s q) : Type))
      (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x))
Φ : (↑(s p) : Type) → q.Rep := fun (x : (↑(s p) : Type)) ↦ (↑(Ψ x) : q.Rep)
x : p.Rep
this : Membership.mem (γ := Set p.Rep) (⋃ y ∈ s p, ball y ε) x
refine_1 : ∀ (y : p.Rep) (ys : y ∈ s p) (hy : x ∈ ball y ε), ∃ y ∈ s p, dist x y ≤ ε
⊢ ∃ y ∈ s p, dist x y ≤ ε

Tactic:
obtain ⟨y, ys, hy⟩ := mem_iUnion₂.1 this

Premises used: Set.mem_iUnion₂, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x ε)
N : (p : GHSpace) → ℕ := fun (p : GHSpace) ↦ Nat.card (↑(s p) : Type)
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (Nat.card (↑(s p) : Type)) :=
  fun (p : GHSpace) ↦ Finite.equivFin (↑(s p) : Type)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (N p) fun (a b : Fin (N p)) ↦
      ⌊ε⁻¹ *
          dist (α := (↑(s p) : Type))
            (((E p).symm : (a : Fin (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) a : (↑(s p) : Type))
            (((E p).symm : (a : Fin (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : (↑(s p) : Type) → (↑(s q) : Type) :=
  fun (x : (↑(s p) : Type)) ↦
    ((E q).symm : (a : Fin (Nat.card (↑(s q) : Type))) → (↑(s q) : Type))
      (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x))
Φ : (↑(s p) : Type) → q.Rep := fun (x : (↑(s p) : Type)) ↦ (↑(Ψ x) : q.Rep)
x : p.Rep
this : Membership.mem (γ := Set p.Rep) (⋃ y ∈ s p, ball y ε) x
y : p.Rep
ys : y ∈ s p
hy : x ∈ ball y ε
⊢ ∃ y ∈ s p, dist x y ≤ ε

Tactic:
⟨y, ys, hy.le⟩

Premises used: LT.lt.le, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x ε)
N : (p : GHSpace) → ℕ := fun (p : GHSpace) ↦ Nat.card (↑(s p) : Type)
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (Nat.card (↑(s p) : Type)) :=
  fun (p : GHSpace) ↦ Finite.equivFin (↑(s p) : Type)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (N p) fun (a b : Fin (N p)) ↦
      ⌊ε⁻¹ *
          dist (α := (↑(s p) : Type))
            (((E p).symm : (a : Fin (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) a : (↑(s p) : Type))
            (((E p).symm : (a : Fin (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : (↑(s p) : Type) → (↑(s q) : Type) :=
  fun (x : (↑(s p) : Type)) ↦
    ((E q).symm : (a : Fin (Nat.card (↑(s q) : Type))) → (↑(s q) : Type))
      (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x))
Φ : (↑(s p) : Type) → q.Rep := fun (x : (↑(s p) : Type)) ↦ (↑(Ψ x) : q.Rep)
x : p.Rep
this : Membership.mem (γ := Set p.Rep) (⋃ y ∈ s p, ball y ε) x
y : p.Rep
ys : y ∈ s p
hy : x ∈ ball y ε
⊢ ∃ y ∈ s p, dist x y ≤ ε

Tactic:
exact ⟨y, ys, hy.le⟩
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
δ : ℝ
δpos : δ > 0
ε : ℝ := 2 / 5 * δ
εpos : 0 < ε
s : (p : GHSpace) → Set p.Rep
hs : ∀ (p : GHSpace), (s p).Finite ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x ε)
N : (p : GHSpace) → ℕ := fun (p : GHSpace) ↦ Nat.card (↑(s p) : Type)
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (Nat.card (↑(s p) : Type)) :=
  fun (p : GHSpace) ↦ Finite.equivFin (↑(s p) : Type)
F : GHSpace → (n : ℕ) × (Fin n → Fin n → ℤ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (N p) fun (a b : Fin (N p)) ↦
      ⌊ε⁻¹ *
          dist (α := (↑(s p) : Type))
            (((E p).symm : (a : Fin (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) a : (↑(s p) : Type))
            (((E p).symm : (a : Fin (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋
p q : GHSpace
hpq : F p = F q
Npq : N p = N q
Ψ : (↑(s p) : Type) → (↑(s q) : Type) :=
  fun (x : (↑(s p) : Type)) ↦
    ((E q).symm : (a : Fin (Nat.card (↑(s q) : Type))) → (↑(s q) : Type))
      (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x))
Φ : (↑(s p) : Type) → q.Rep := fun (x : (↑(s p) : Type)) ↦ (↑(Ψ x) : q.Rep)
x : q.Rep
⊢ Membership.mem (γ := Set q.Rep) (⋃ y ∈ s q, ball y ε) x

Tactic:
have : x ∈ ⋃ y ∈ s q, ball y ε := (hs q).2 (mem_univ _)