awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
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 y : (↑(s p) : Type)
i : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x) : ℕ)
hip : i < N p
hiq : i < N q
i' : i = (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ x)) : ℕ)
j : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) y) : ℕ)
hjp : j < N p
hjq : j < N q
j' : j = (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ y)) : ℕ)
this_1 :
  (F p).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x)
      ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) y) =
    ⌊ε⁻¹ * dist x y⌋
Ap :
  (F p).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (⟨i, hip⟩ : Fin ((F p).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)))
      (⟨j, hjp⟩ : Fin ((F p).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ))) =
    ⌊ε⁻¹ * dist x y⌋
this :
  (F q).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)
      ((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ x))
      ((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ y)) =
    ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq :
  (F q).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (⟨i, hiq⟩ : Fin ((F q).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)))
      (⟨j, hjq⟩ : Fin ((F q).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ))) =
    ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε
have this₁ : (F p).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (⟨i, hip⟩ : Fin ((F p).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)))
    (⟨j, hjp⟩ : Fin ((F p).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ))) =
  (F q).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) ⟨i, hiq⟩ ⟨j, hjq⟩
Tactic: have : (F p).2 ⟨i, hip⟩ ⟨j, hjp⟩ = (F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩ := by
        have hpq' : (F p).snd ≍ (F q).snd := (Sigma.mk.inj_iff.1 hpq).2
        rw [Fin.heq_fun₂_iff Npq Npq] at hpq'
        rw [← hpq']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
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 y : (↑(s p) : Type)
i : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x) : ℕ)
hip : i < N p
hiq : i < N q
i' : i = (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ x)) : ℕ)
j : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) y) : ℕ)
hjp : j < N p
hjq : j < N q
j' : j = (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ y)) : ℕ)
this_1 :
  (F p).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x)
      ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) y) =
    ⌊ε⁻¹ * dist x y⌋
Ap :
  (F p).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (⟨i, hip⟩ : Fin ((F p).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)))
      (⟨j, hjp⟩ : Fin ((F p).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ))) =
    ⌊ε⁻¹ * dist x y⌋
this_2 :
  (F q).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)
      ((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ x))
      ((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ y)) =
    ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq :
  (F q).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (⟨i, hiq⟩ : Fin ((F q).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)))
      (⟨j, hjq⟩ : Fin ((F q).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ))) =
    ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
this :
  (F p).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (⟨i, hip⟩ : Fin ((F p).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)))
      (⟨j, hjp⟩ : Fin ((F p).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ))) =
    (F q).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) ⟨i, hiq⟩ ⟨j, hjq⟩
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε
have this₁ : ⌊ε⁻¹ * dist x y⌋ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Tactic: rw [Ap, Aq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 y : (↑(s p) : Type)
i : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x) : ℕ)
hip : i < N p
hiq : i < N q
i' : i = (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ x)) : ℕ)
j : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) y) : ℕ)
hjp : j < N p
hjq : j < N q
j' : j = (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ y)) : ℕ)
this_1 :
  (F p).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x)
      ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) y) =
    ⌊ε⁻¹ * dist x y⌋
Ap :
  (F p).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (⟨i, hip⟩ : Fin ((F p).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)))
      (⟨j, hjp⟩ : Fin ((F p).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ))) =
    ⌊ε⁻¹ * dist x y⌋
this_2 :
  (F q).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)
      ((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ x))
      ((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ y)) =
    ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq :
  (F q).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (⟨i, hiq⟩ : Fin ((F q).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)))
      (⟨j, hjq⟩ : Fin ((F q).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ))) =
    ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
this : ⌊ε⁻¹ * dist x y⌋ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
⊢ ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)| = |ε⁻¹ * (dist x y - dist (Ψ x) (Ψ y))|
have rw : ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)| = |ε⁻¹| * |dist x y - dist (Ψ x) (Ψ y)|
Tactic: rw [abs_mul, abs_of_nonneg (inv_pos.2 εpos).le]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 y : (↑(s p) : Type)
i : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x) : ℕ)
hip : i < N p
hiq : i < N q
i' : i = (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ x)) : ℕ)
j : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) y) : ℕ)
hjp : j < N p
hjq : j < N q
j' : j = (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ y)) : ℕ)
this_1 :
  (F p).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x)
      ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) y) =
    ⌊ε⁻¹ * dist x y⌋
Ap :
  (F p).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (⟨i, hip⟩ : Fin ((F p).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)))
      (⟨j, hjp⟩ : Fin ((F p).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ))) =
    ⌊ε⁻¹ * dist x y⌋
this_2 :
  (F q).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)
      ((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ x))
      ((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ y)) =
    ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq :
  (F q).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (⟨i, hiq⟩ : Fin ((F q).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)))
      (⟨j, hjq⟩ : Fin ((F q).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ))) =
    ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
this : ⌊ε⁻¹ * dist x y⌋ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
rw : ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)| = |ε⁻¹| * |dist x y - dist (Ψ x) (Ψ y)|
⊢ ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)| = |ε⁻¹ * (dist x y - dist (Ψ x) (Ψ y))|
have rw₁ : ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)| = ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)|
Tactic: rw [abs_mul, abs_of_nonneg (inv_pos.2 εpos).le]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 y : (↑(s p) : Type)
i : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x) : ℕ)
hip : i < N p
hiq : i < N q
i' : i = (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ x)) : ℕ)
j : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) y) : ℕ)
hjp : j < N p
hjq : j < N q
j' : j = (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ y)) : ℕ)
this_1 :
  (F p).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x)
      ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) y) =
    ⌊ε⁻¹ * dist x y⌋
Ap :
  (F p).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (⟨i, hip⟩ : Fin ((F p).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)))
      (⟨j, hjp⟩ : Fin ((F p).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ))) =
    ⌊ε⁻¹ * dist x y⌋
this_2 :
  (F q).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)
      ((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ x))
      ((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ y)) =
    ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq :
  (F q).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (⟨i, hiq⟩ : Fin ((F q).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)))
      (⟨j, hjq⟩ : Fin ((F q).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ))) =
    ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
this : ⌊ε⁻¹ * dist x y⌋ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
⊢ |ε⁻¹ * (dist x y - dist (Ψ x) (Ψ y))| = |ε⁻¹ * dist x y - ε⁻¹ * dist (Ψ x) (Ψ y)|
have e_a : ε⁻¹ * (dist x y - dist (Ψ x) (Ψ y)) = ε⁻¹ * dist x y - ε⁻¹ * dist (Ψ x) (Ψ y)
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (hypothesis)
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 y : (↑(s p) : Type)
i : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x) : ℕ)
hip : i < N p
hiq : i < N q
i' : i = (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ x)) : ℕ)
j : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) y) : ℕ)
hjp : j < N p
hjq : j < N q
j' : j = (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ y)) : ℕ)
this_1 :
  (F p).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x)
      ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) y) =
    ⌊ε⁻¹ * dist x y⌋
Ap :
  (F p).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (⟨i, hip⟩ : Fin ((F p).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)))
      (⟨j, hjp⟩ : Fin ((F p).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ))) =
    ⌊ε⁻¹ * dist x y⌋
this_2 :
  (F q).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)
      ((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ x))
      ((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ y)) =
    ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq :
  (F q).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (⟨i, hiq⟩ : Fin ((F q).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)))
      (⟨j, hjq⟩ : Fin ((F q).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ))) =
    ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
this : ⌊ε⁻¹ * dist x y⌋ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε
have I : ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)| ≤ 1
Tactic: have I :=
        calc
          ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)| = |ε⁻¹ * (dist x y - dist (Ψ x) (Ψ y))| := by
            rw [abs_mul, abs_of_nonneg (inv_pos.2 εpos).le]
          _ = |ε⁻¹ * dist x y - ε⁻¹ * dist (Ψ x) (Ψ y)| := by congr; ring
          _ ≤ 1 := le_of_lt (abs_sub_lt_one_of_floor_eq_floor this)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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 y : (↑(s p) : Type)
i : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x) : ℕ)
hip : i < N p
hiq : i < N q
i' : i = (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ x)) : ℕ)
j : ℕ := (↑((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) y) : ℕ)
hjp : j < N p
hjq : j < N q
j' : j = (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ y)) : ℕ)
this_1 :
  (F p).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) x)
      ((E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) y) =
    ⌊ε⁻¹ * dist x y⌋
Ap :
  (F p).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (⟨i, hip⟩ : Fin ((F p).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)))
      (⟨j, hjp⟩ : Fin ((F p).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ))) =
    ⌊ε⁻¹ * dist x y⌋
this_2 :
  (F q).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)
      ((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ x))
      ((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ y)) =
    ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Aq :
  (F q).snd (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ) (⟨i, hiq⟩ : Fin ((F q).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ)))
      (⟨j, hjq⟩ : Fin ((F q).fst (β := fun (n : ℕ) ↦ Fin n → Fin n → ℤ))) =
    ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
this : ⌊ε⁻¹ * dist x y⌋ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
I : ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)| ≤ 1
⊢ ε * (ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)|) ≤ ε * 1
have ha : 0 ≤ ε
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
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)
main : ghDist p.Rep q.Rep ≤ ε + ε / 2 + ε
⊢ dist p q ≤ δ
have dist : ε + ε / 2 + ε = δ
Tactic: calc
    dist p q = ghDist p.Rep q.Rep := dist_ghDist p q
    _ ≤ ε + ε / 2 + ε := main
    _ = δ := by ring
-- 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))
⊢ TotallyBounded t
have refine : ∀ (δ : ℝ) (δpos : δ > 0),
  ∃ (β : Type) (x : Fintype β) (F : (↑t : Type) → β),
    ∀ (x y : (↑t : Type)), F x = F y → dist (↑x : GHSpace) (↑y : GHSpace) < δ
Tactic: refine Metric.totallyBounded_of_finite_discretization fun δ δpos => ?_
-- 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 * δ
⊢ ∃ (β : Type) (x : Fintype β) (F : (↑t : Type) → β),
    ∀ (x y : (↑t : Type)), F x = F y → dist (↑x : GHSpace) (↑y : GHSpace) < δ
have εpos : 0 < ε
Tactic: have εpos : 0 < ε := mul_pos (by simp) δpos
-- 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 < ε
⊢ ∃ (β : Type) (x : Fintype β) (F : (↑t : Type) → β),
    ∀ (x y : (↑t : Type)), F x = F y → dist (↑x : GHSpace) (↑y : GHSpace) < δ
have rcases : ∀ (n : ℕ) (hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε),
  ∃ (β : Type) (x : Fintype β) (F : (↑t : Type) → β),
    ∀ (x y : (↑t : Type)), F x = F y → dist (↑x : GHSpace) (↑y : GHSpace) < δ
Tactic: rcases Metric.tendsto_atTop.1 ulim ε εpos with ⟨n, hn⟩
-- 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 n ≤ ε
have this : dist (u n) 0 < ε
Tactic: have := hn n le_rfl