awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
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 : q.Rep
this : Membership.mem (γ := Set q.Rep) (⋃ y ∈ s q, ball y (u n)) x
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y (u n)
i : ℕ := (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) : ℕ)
hi : (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) : ℕ) < N q := ⋯
ihi_eq :
  (⟨i, hi⟩ : Fin (N q)) = (E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)
hiq : i < N q
hip : i < N p
z : (↑(s p) : Type) := ((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) ⟨i, hip⟩
⊢ dist x (Φ z) ≤ ε
have C1 : (E p : (a : (↑(s p) : Type)) → Fin (N p)) z = (⟨i, hip⟩ : Fin (N p))
Tactic: have C1 : (E p) z = ⟨i, hip⟩ := (E p).apply_symm_apply ⟨i, hip⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
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 : q.Rep
this : Membership.mem (γ := Set q.Rep) (⋃ y ∈ s q, ball y (u n)) x
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y (u n)
i : ℕ := (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) : ℕ)
hi : (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) : ℕ) < N q := ⋯
ihi_eq :
  (⟨i, hi⟩ : Fin (N q)) = (E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)
hiq : i < N q
hip : i < N p
z : (↑(s p) : Type) := ((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) ⟨i, hip⟩
C1 : (E p : (a : (↑(s p) : Type)) → Fin (N p)) z = (⟨i, hip⟩ : Fin (N p))
⊢ dist x (Φ z) ≤ ε
have C2 : Fin.cast Npq (⟨i, hip⟩ : Fin (N p)) = ⟨i, hi⟩
Tactic: have C2 : Fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩ := rfl
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
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 : q.Rep
this : Membership.mem (γ := Set q.Rep) (⋃ y ∈ s q, ball y (u n)) x
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y (u n)
i : ℕ := (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) : ℕ)
hi : (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) : ℕ) < N q := ⋯
ihi_eq :
  (⟨i, hi⟩ : Fin (N q)) = (E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)
hiq : i < N q
hip : i < N p
z : (↑(s p) : Type) := ((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) ⟨i, hip⟩
C1 : (E p : (a : (↑(s p) : Type)) → Fin (N p)) z = (⟨i, hip⟩ : Fin (N p))
C2 : Fin.cast Npq (⟨i, hip⟩ : Fin (N p)) = ⟨i, hi⟩
⊢ dist x (Φ z) ≤ ε
have C3 : ((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) ⟨i, hi⟩ = Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys
Tactic: have C3 : (E q).symm ⟨i, hi⟩ = ⟨y, ys⟩ := by
        rw [ihi_eq]; exact (E q).symm_apply_apply ⟨y, ys⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 : q.Rep
this : Membership.mem (γ := Set q.Rep) (⋃ y ∈ s q, ball y (u n)) x
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y (u n)
i : ℕ := (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) : ℕ)
hi : (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) : ℕ) < N q := ⋯
ihi_eq :
  (⟨i, hi⟩ : Fin (N q)) = (E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)
hiq : i < N q
hip : i < N p
z : (↑(s p) : Type) := ((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) ⟨i, hip⟩
C1 : (E p : (a : (↑(s p) : Type)) → Fin (N p)) z = (⟨i, hip⟩ : Fin (N p))
C2 : Fin.cast Npq (⟨i, hip⟩ : Fin (N p)) = ⟨i, hi⟩
C3 : ((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) ⟨i, hi⟩ = Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys
⊢ (↑(((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (N p)) z))) :
      q.Rep) =
    y
have rw : (↑(((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) (Fin.cast Npq ⟨i, hip⟩)) : q.Rep) = y
Tactic: rw [C1, C2, C3]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 : q.Rep
this : Membership.mem (γ := Set q.Rep) (⋃ y ∈ s q, ball y (u n)) x
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y (u n)
i : ℕ := (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) : ℕ)
hi : (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) : ℕ) < N q := ⋯
ihi_eq :
  (⟨i, hi⟩ : Fin (N q)) = (E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)
hiq : i < N q
hip : i < N p
z : (↑(s p) : Type) := ((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) ⟨i, hip⟩
C1 : (E p : (a : (↑(s p) : Type)) → Fin (N p)) z = (⟨i, hip⟩ : Fin (N p))
C2 : Fin.cast Npq (⟨i, hip⟩ : Fin (N p)) = ⟨i, hi⟩
C3 : ((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) ⟨i, hi⟩ = Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys
rw : (↑(((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) (Fin.cast Npq ⟨i, hip⟩)) : q.Rep) = y
⊢ (↑(((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (N p)) z))) :
      q.Rep) =
    y
have rw₁ : (↑(((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) ⟨i, hi⟩) : q.Rep) = y
Tactic: rw [C1, C2, C3]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 : q.Rep
this : Membership.mem (γ := Set q.Rep) (⋃ y ∈ s q, ball y (u n)) x
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y (u n)
i : ℕ := (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) : ℕ)
hi : (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) : ℕ) < N q := ⋯
ihi_eq :
  (⟨i, hi⟩ : Fin (N q)) = (E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)
hiq : i < N q
hip : i < N p
z : (↑(s p) : Type) := ((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) ⟨i, hip⟩
C1 : (E p : (a : (↑(s p) : Type)) → Fin (N p)) z = (⟨i, hip⟩ : Fin (N p))
C2 : Fin.cast Npq (⟨i, hip⟩ : Fin (N p)) = ⟨i, hi⟩
C3 : ((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) ⟨i, hi⟩ = Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys
rw : (↑(((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) (Fin.cast Npq ⟨i, hip⟩)) : q.Rep) = y
rw₁ : (↑(((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) ⟨i, hi⟩) : q.Rep) = y
⊢ (↑(((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) (Fin.cast Npq ((E p : (a : (↑(s p) : Type)) → Fin (N p)) z))) :
      q.Rep) =
    y
have rw₂ : (↑(Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys) : q.Rep) = y
Tactic: rw [C1, C2, C3]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
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 : q.Rep
this : Membership.mem (γ := Set q.Rep) (⋃ y ∈ s q, ball y (u n)) x
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y (u n)
i : ℕ := (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) : ℕ)
hi : (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) : ℕ) < N q := ⋯
ihi_eq :
  (⟨i, hi⟩ : Fin (N q)) = (E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)
hiq : i < N q
hip : i < N p
z : (↑(s p) : Type) := ((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) ⟨i, hip⟩
C1 : (E p : (a : (↑(s p) : Type)) → Fin (N p)) z = (⟨i, hip⟩ : Fin (N p))
C2 : Fin.cast Npq (⟨i, hip⟩ : Fin (N p)) = ⟨i, hi⟩
C3 : ((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) ⟨i, hi⟩ = Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys
⊢ dist x (Φ z) ≤ ε
have this₁ : Φ z = y
Tactic: have : Φ z = y := by simp only [Ψ, Φ]; rw [C1, C2, C3]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 : q.Rep
this_1 : Membership.mem (γ := Set q.Rep) (⋃ y ∈ s q, ball y (u n)) x
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y (u n)
i : ℕ := (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) : ℕ)
hi : (↑((E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) : ℕ) < N q := ⋯
ihi_eq :
  (⟨i, hi⟩ : Fin (N q)) = (E q : (a : (↑(s q) : Type)) → Fin (N q)) (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)
hiq : i < N q
hip : i < N p
z : (↑(s p) : Type) := ((E p).symm : (a : Fin (N p)) → (↑(s p) : Type)) ⟨i, hip⟩
C1 : (E p : (a : (↑(s p) : Type)) → Fin (N p)) z = (⟨i, hip⟩ : Fin (N p))
C2 : Fin.cast Npq (⟨i, hip⟩ : Fin (N p)) = ⟨i, hi⟩
C3 : ((E q).symm : (a : Fin (N q)) → (↑(s q) : Type)) ⟨i, hi⟩ = Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys
this : Φ z = y
⊢ dist x (Φ z) ≤ ε
have h : dist x y ≤ ε
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
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)
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε
have this : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
Tactic: have : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y) := rfl