awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam (α := p.Rep) univ ≤ C
hcov :
  ∀ p ∈ t,
    ∀ (n : ℕ),
      ∃ (s : Set p.Rep), #(↑s : Type) ≤ (↑(K n) : Cardinal.{0}) ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s, ball x (u n))
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : (p : GHSpace) → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (N p)
hs : ∀ p ∈ t, Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x (u n))
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) ⟨N p, ⋯⟩
      fun (a b : Fin (↑(⟨N p, ⋯⟩ : Fin (K n).succ) : ℕ)) ↦
      ⟨min M
          ⌊ε⁻¹ *
              dist (α := (↑(s p) : Type)) (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) a : (↑(s p) : Type))
                (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋₊,
        ⋯⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq :
  Eq (α := (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) p pt))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) q qt))
Npq : N p = N q
Ψ : (↑(s p) : Type) → (↑(s q) : Type) :=
  fun (x : (↑(s p) : Type)) ↦
    ((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (N p)) x))
Φ : (↑(s p) : Type) → q.Rep := fun (x : (↑(s p) : Type)) ↦ (↑(Ψ x) : q.Rep)
x y : (↑(s p) : Type)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (N p)) x) : ℕ)
hip : i < N p
hiq : i < N q
i' : i = (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Ψ x)) : ℕ)
j : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (N p)) y) : ℕ)
hjp : j < N p
hjq : j < N q
j' : j = (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Ψ y)) : ℕ)
Ap :
  (↑((F p).snd (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)
          (⟨i, hip⟩ : Fin (↑((F p).fst (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)) : ℕ))
          (⟨j, hjp⟩ :
            Fin (↑((F p).fst (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)) : ℕ))) :
      ℕ) =
    ⌊ε⁻¹ * dist x y⌋₊
⊢ diam (α := q.Rep) univ ≤ C

Tactic:
exact hdiam q qt
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam (α := p.Rep) univ ≤ C
hcov :
  ∀ p ∈ t,
    ∀ (n : ℕ),
      ∃ (s : Set p.Rep), #(↑s : Type) ≤ (↑(K n) : Cardinal.{0}) ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s, ball x (u n))
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : (p : GHSpace) → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (N p)
hs : ∀ p ∈ t, Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x (u n))
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) ⟨N p, ⋯⟩
      fun (a b : Fin (↑(⟨N p, ⋯⟩ : Fin (K n).succ) : ℕ)) ↦
      ⟨min M
          ⌊ε⁻¹ *
              dist (α := (↑(s p) : Type)) (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) a : (↑(s p) : Type))
                (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋₊,
        ⋯⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq :
  Eq (α := (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) p pt))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) q qt))
Npq : N p = N q
Ψ : (↑(s p) : Type) → (↑(s q) : Type) :=
  fun (x : (↑(s p) : Type)) ↦
    ((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (N p)) x))
Φ : (↑(s p) : Type) → q.Rep := fun (x : (↑(s p) : Type)) ↦ (↑(Ψ x) : q.Rep)
x y : (↑(s p) : Type)
this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (N p)) x) : ℕ)
hip : i < N p
hiq : i < N q
i' : i = (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Ψ x)) : ℕ)
j : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (N p)) y) : ℕ)
hjp : j < N p
hjq : j < N q
j' : j = (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Ψ y)) : ℕ)
Ap :
  (↑((F p).snd (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)
          (⟨i, hip⟩ : Fin (↑((F p).fst (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)) : ℕ))
          (⟨j, hjp⟩ :
            Fin (↑((F p).fst (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)) : ℕ))) :
      ℕ) =
    ⌊ε⁻¹ * dist x y⌋₊
Aq :
  (↑((F q).snd (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)
          (⟨i, hiq⟩ : Fin (↑((F q).fst (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)) : ℕ))
          (⟨j, hjq⟩ :
            Fin (↑((F q).fst (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)) : ℕ))) :
      ℕ) =
    ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊
⊢ (F p).snd (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) ≍
    (F q).snd (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)

Tactic:
have hpq' : (F p).snd ≍ (F q).snd := (Sigma.mk.inj_iff.1 hpq).2
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam (α := p.Rep) univ ≤ C
hcov :
  ∀ p ∈ t,
    ∀ (n : ℕ),
      ∃ (s : Set p.Rep), #(↑s : Type) ≤ (↑(K n) : Cardinal.{0}) ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s, ball x (u n))
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : (p : GHSpace) → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (N p)
hs : ∀ p ∈ t, Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x (u n))
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) ⟨N p, ⋯⟩
      fun (a b : Fin (↑(⟨N p, ⋯⟩ : Fin (K n).succ) : ℕ)) ↦
      ⟨min M
          ⌊ε⁻¹ *
              dist (α := (↑(s p) : Type)) (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) a : (↑(s p) : Type))
                (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋₊,
        ⋯⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq :
  Eq (α := (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) p pt))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) q qt))
Npq : N p = N q
Ψ : (↑(s p) : Type) → (↑(s q) : Type) :=
  fun (x : (↑(s p) : Type)) ↦
    ((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (N p)) x))
Φ : (↑(s p) : Type) → q.Rep := fun (x : (↑(s p) : Type)) ↦ (↑(Ψ x) : q.Rep)
x y : (↑(s p) : Type)
this_1 : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (N p)) x) : ℕ)
hip : i < N p
hiq : i < N q
i' : i = (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Ψ x)) : ℕ)
j : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (N p)) y) : ℕ)
hjp : j < N p
hjq : j < N q
j' : j = (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Ψ y)) : ℕ)
Ap :
  (↑((F p).snd (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)
          (⟨i, hip⟩ : Fin (↑((F p).fst (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)) : ℕ))
          (⟨j, hjp⟩ :
            Fin (↑((F p).fst (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)) : ℕ))) :
      ℕ) =
    ⌊ε⁻¹ * dist x y⌋₊
Aq :
  (↑((F q).snd (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)
          (⟨i, hiq⟩ : Fin (↑((F q).fst (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)) : ℕ))
          (⟨j, hjq⟩ :
            Fin (↑((F q).fst (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)) : ℕ))) :
      ℕ) =
    ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊
this : ⌊ε⁻¹ * dist x y⌋₊ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊
⊢ 0 ≤ ⌊ε⁻¹ * dist x y⌋

Tactic:
have D : 0 ≤ ⌊ε⁻¹ * dist x y⌋ :=
          floor_nonneg.2 (mul_nonneg (le_of_lt (inv_pos.2 εpos)) dist_nonneg)
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam (α := p.Rep) univ ≤ C
hcov :
  ∀ p ∈ t,
    ∀ (n : ℕ),
      ∃ (s : Set p.Rep), #(↑s : Type) ≤ (↑(K n) : Cardinal.{0}) ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s, ball x (u n))
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : (p : GHSpace) → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (N p)
hs : ∀ p ∈ t, Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x (u n))
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) ⟨N p, ⋯⟩
      fun (a b : Fin (↑(⟨N p, ⋯⟩ : Fin (K n).succ) : ℕ)) ↦
      ⟨min M
          ⌊ε⁻¹ *
              dist (α := (↑(s p) : Type)) (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) a : (↑(s p) : Type))
                (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋₊,
        ⋯⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq :
  Eq (α := (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) p pt))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) q qt))
Npq : N p = N q
Ψ : (↑(s p) : Type) → (↑(s q) : Type) :=
  fun (x : (↑(s p) : Type)) ↦
    ((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (N p)) x))
Φ : (↑(s p) : Type) → q.Rep := fun (x : (↑(s p) : Type)) ↦ (↑(Ψ x) : q.Rep)
x y : (↑(s p) : Type)
this_1 : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (N p)) x) : ℕ)
hip : i < N p
hiq : i < N q
i' : i = (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Ψ x)) : ℕ)
j : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (N p)) y) : ℕ)
hjp : j < N p
hjq : j < N q
j' : j = (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Ψ y)) : ℕ)
Ap :
  (↑((F p).snd (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)
          (⟨i, hip⟩ : Fin (↑((F p).fst (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)) : ℕ))
          (⟨j, hjp⟩ :
            Fin (↑((F p).fst (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)) : ℕ))) :
      ℕ) =
    ⌊ε⁻¹ * dist x y⌋₊
Aq :
  (↑((F q).snd (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)
          (⟨i, hiq⟩ : Fin (↑((F q).fst (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)) : ℕ))
          (⟨j, hjq⟩ :
            Fin (↑((F q).fst (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ)) : ℕ))) :
      ℕ) =
    ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊
this : ⌊ε⁻¹ * dist x y⌋₊ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊
D : 0 ≤ ⌊ε⁻¹ * dist x y⌋
⊢ 0 ≤ ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋

Tactic:
have D' : 0 ≤ ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋ :=
          floor_nonneg.2 (mul_nonneg (le_of_lt (inv_pos.2 εpos)) dist_nonneg)
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam (α := p.Rep) univ ≤ C
hcov :
  ∀ p ∈ t,
    ∀ (n : ℕ),
      ∃ (s : Set p.Rep), #(↑s : Type) ≤ (↑(K n) : Cardinal.{0}) ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s, ball x (u n))
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : (p : GHSpace) → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (N p)
hs : ∀ p ∈ t, Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x (u n))
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) ⟨N p, ⋯⟩
      fun (a b : Fin (↑(⟨N p, ⋯⟩ : Fin (K n).succ) : ℕ)) ↦
      ⟨min M
          ⌊ε⁻¹ *
              dist (α := (↑(s p) : Type)) (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) a : (↑(s p) : Type))
                (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋₊,
        ⋯⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq :
  Eq (α := (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) p pt))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) q qt))
Npq : N p = N q
Ψ : (↑(s p) : Type) → (↑(s q) : Type) :=
  fun (x : (↑(s p) : Type)) ↦
    ((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (N p)) x))
Φ : (↑(s p) : Type) → q.Rep := fun (x : (↑(s p) : Type)) ↦ (↑(Ψ x) : q.Rep)
main : ghDist p.Rep q.Rep ≤ ε + ε / 2 + ε
⊢ dist p q = ghDist p.Rep q.Rep

Tactic:
dist_ghDist p q

Premises used: GromovHausdorff.dist_ghDist
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam (α := p.Rep) univ ≤ C
hcov :
  ∀ p ∈ t,
    ∀ (n : ℕ),
      ∃ (s : Set p.Rep), #(↑s : Type) ≤ (↑(K n) : Cardinal.{0}) ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s, ball x (u n))
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : (p : GHSpace) → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (N p)
hs : ∀ p ∈ t, Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x (u n))
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) ⟨N p, ⋯⟩
      fun (a b : Fin (↑(⟨N p, ⋯⟩ : Fin (K n).succ) : ℕ)) ↦
      ⟨min M
          ⌊ε⁻¹ *
              dist (α := (↑(s p) : Type)) (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) a : (↑(s p) : Type))
                (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋₊,
        ⋯⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq :
  Eq (α := (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) p pt))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) q qt))
Npq : N p = N q
Ψ : (↑(s p) : Type) → (↑(s q) : Type) :=
  fun (x : (↑(s p) : Type)) ↦
    ((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (N p)) x))
Φ : (↑(s p) : Type) → q.Rep := fun (x : (↑(s p) : Type)) ↦ (↑(Ψ x) : q.Rep)
main : ghDist p.Rep q.Rep ≤ ε + ε / 2 + ε
⊢ ghDist p.Rep q.Rep ≤ ε + ε / 2 + ε

Tactic:
main
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam (α := p.Rep) univ ≤ C
hcov :
  ∀ p ∈ t,
    ∀ (n : ℕ),
      ∃ (s : Set p.Rep), #(↑s : Type) ≤ (↑(K n) : Cardinal.{0}) ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s, ball x (u n))
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : (p : GHSpace) → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (N p)
hs : ∀ p ∈ t, Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x (u n))
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) ⟨N p, ⋯⟩
      fun (a b : Fin (↑(⟨N p, ⋯⟩ : Fin (K n).succ) : ℕ)) ↦
      ⟨min M
          ⌊ε⁻¹ *
              dist (α := (↑(s p) : Type)) (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) a : (↑(s p) : Type))
                (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋₊,
        ⋯⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq :
  Eq (α := (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) p pt))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) q qt))
Npq : N p = N q
Ψ : (↑(s p) : Type) → (↑(s q) : Type) :=
  fun (x : (↑(s p) : Type)) ↦
    ((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (N p)) x))
Φ : (↑(s p) : Type) → q.Rep := fun (x : (↑(s p) : Type)) ↦ (↑(Ψ x) : q.Rep)
main : ghDist p.Rep q.Rep ≤ ε + ε / 2 + ε
simp : 5⁻¹ * δ + 5⁻¹ * δ / 2 + 5⁻¹ * δ = δ / 2
⊢ ε + ε / 2 + ε = δ / 2

Tactic:
simp only [ε, one_div]

Premises used: one_div
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam (α := p.Rep) univ ≤ C
hcov :
  ∀ p ∈ t,
    ∀ (n : ℕ),
      ∃ (s : Set p.Rep), #(↑s : Type) ≤ (↑(K n) : Cardinal.{0}) ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s, ball x (u n))
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : (p : GHSpace) → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (N p)
hs : ∀ p ∈ t, Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x (u n))
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) ⟨N p, ⋯⟩
      fun (a b : Fin (↑(⟨N p, ⋯⟩ : Fin (K n).succ) : ℕ)) ↦
      ⟨min M
          ⌊ε⁻¹ *
              dist (α := (↑(s p) : Type)) (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) a : (↑(s p) : Type))
                (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋₊,
        ⋯⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq :
  Eq (α := (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) p pt))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) q qt))
Npq : N p = N q
Ψ : (↑(s p) : Type) → (↑(s q) : Type) :=
  fun (x : (↑(s p) : Type)) ↦
    ((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (N p)) x))
Φ : (↑(s p) : Type) → q.Rep := fun (x : (↑(s p) : Type)) ↦ (↑(Ψ x) : q.Rep)
main : ghDist p.Rep q.Rep ≤ ε + ε / 2 + ε
⊢ 5⁻¹ * δ + 5⁻¹ * δ / 2 + 5⁻¹ * δ = δ / 2

Tactic:
ring
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam (α := p.Rep) univ ≤ C
hcov :
  ∀ p ∈ t,
    ∀ (n : ℕ),
      ∃ (s : Set p.Rep), #(↑s : Type) ≤ (↑(K n) : Cardinal.{0}) ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s, ball x (u n))
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : (p : GHSpace) → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (N p)
hs : ∀ p ∈ t, Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x (u n))
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) ⟨N p, ⋯⟩
      fun (a b : Fin (↑(⟨N p, ⋯⟩ : Fin (K n).succ) : ℕ)) ↦
      ⟨min M
          ⌊ε⁻¹ *
              dist (α := (↑(s p) : Type)) (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) a : (↑(s p) : Type))
                (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋₊,
        ⋯⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq :
  Eq (α := (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) p pt))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) q qt))
Npq : N p = N q
Ψ : (↑(s p) : Type) → (↑(s q) : Type) :=
  fun (x : (↑(s p) : Type)) ↦
    ((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (N p)) x))
Φ : (↑(s p) : Type) → q.Rep := fun (x : (↑(s p) : Type)) ↦ (↑(Ψ x) : q.Rep)
main : ghDist p.Rep q.Rep ≤ ε + ε / 2 + ε
⊢ δ / 2 < δ

Tactic:
half_lt_self δpos

Premises used: half_lt_self
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam (α := p.Rep) univ ≤ C
hcov :
  ∀ p ∈ t,
    ∀ (n : ℕ),
      ∃ (s : Set p.Rep), #(↑s : Type) ≤ (↑(K n) : Cardinal.{0}) ∧ Subset (α := Set p.Rep) univ (⋃ x ∈ s, ball x (u n))
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, Dist.dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : (p : GHSpace) → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → (↑(s p) : Type) ≃ Fin (N p)
hs : ∀ p ∈ t, Subset (α := Set p.Rep) univ (⋃ x ∈ s p, ball x (u n))
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) :=
  fun (p : GHSpace) ↦
    Sigma.mk (β := fun (k : Fin (K n).succ) ↦ Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ) ⟨N p, ⋯⟩
      fun (a b : Fin (↑(⟨N p, ⋯⟩ : Fin (K n).succ) : ℕ)) ↦
      ⟨min M
          ⌊ε⁻¹ *
              Dist.dist (α := (↑(s p) : Type)) (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) a : (↑(s p) : Type))
                (((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) b : (↑(s p) : Type))⌋₊,
        ⋯⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq :
  Eq (α := (k : Fin (K n).succ) × (Fin (↑k : ℕ) → Fin (↑k : ℕ) → Fin M.succ))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) p pt))
    ((fun (p : (↑t : Type)) ↦ F (↑p : GHSpace)) (Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) q qt))
Npq : N p = N q
Ψ : (↑(s p) : Type) → (↑(s q) : Type) :=
  fun (x : (↑(s p) : Type)) ↦
    ((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (N p)) x))
Φ : (↑(s p) : Type) → q.Rep := fun (x : (↑(s p) : Type)) ↦ (↑(Ψ x) : q.Rep)
main : ghDist p.Rep q.Rep ≤ ε + ε / 2 + ε
dist : ε + ε / 2 + ε = δ / 2
⊢ Dist.dist (↑(Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) p pt) : GHSpace)
      (↑(Subtype.mk (p := fun (x : GHSpace) ↦ x ∈ t) q qt) : GHSpace) <
    δ

Tactic:
calc
    dist p q = ghDist p.Rep q.Rep := dist_ghDist p q
    _ ≤ ε + ε / 2 + ε := main
    _ = δ / 2 := by simp only [ε, one_div]; ring
    _ < δ := half_lt_self δpos

Premises used: half_lt_self, GromovHausdorff.ghDist, GromovHausdorff.dist_ghDist, Dist.dist, GromovHausdorff.GHSpace.Rep
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : ℕ → Type
inst : (n : ℕ) → MetricSpace (X n)
inst_1 : ∀ (n : ℕ), CompactSpace (X n)
inst_2 : ∀ (n : ℕ), Nonempty (X n)
A : Type
inst_3 : MetricSpace A
⊢ MetricSpace A

Tactic:
infer_instance
-- Module: Mathlib.Topology.MetricSpace.GromovHausdorff
Goal:
X : ℕ → Type
inst : (n : ℕ) → MetricSpace (X n)
inst_1 : ∀ (n : ℕ), CompactSpace (X n)
inst_2 : ∀ (n : ℕ), Nonempty (X n)
n_1 n : ℕ
Y : AuxGluingStruct (X n)
⊢ MetricSpace (GlueSpace (Y := OptimalGHCoupling (X n) (X (n + 1))) ⋯ ⋯)

Tactic:
infer_instance