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 : q.Rep
this : Membership.mem (γ := Set q.Rep) (⋃ y ∈ s q, ball y ε) x
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y ε
i : ℕ :=
  (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type)))
        (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) :
    ℕ)
hi : (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type)))
        (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) :
    ℕ) <
  Nat.card (↑(s q) : Type) :=
  ⋯
ihi_eq :
  (⟨i, hi⟩ : Fin (N q)) =
    (E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (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 (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) ⟨i, hip⟩
C1 : (E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) z = (⟨i, hip⟩ : Fin (Nat.card (↑(s p) : Type)))
C2 : Fin.cast Npq (⟨i, hip⟩ : Fin (N p)) = ⟨i, hi⟩
⊢ dist x (Φ z) ≤ ε
have C3 : ((E q).symm : (a : Fin (Nat.card (↑(s q) : Type))) → (↑(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:
δ : ℝ
δ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
this : Membership.mem (γ := Set q.Rep) (⋃ y ∈ s q, ball y ε) x
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y ε
i : ℕ :=
  (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type)))
        (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) :
    ℕ)
hi : (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type)))
        (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) :
    ℕ) <
  Nat.card (↑(s q) : Type) :=
  ⋯
ihi_eq :
  (⟨i, hi⟩ : Fin (N q)) =
    (E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (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 (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) ⟨i, hip⟩
C1 : (E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) z = (⟨i, hip⟩ : Fin (Nat.card (↑(s p) : Type)))
C2 : Fin.cast Npq (⟨i, hip⟩ : Fin (N p)) = ⟨i, hi⟩
C3 :
  ((E q).symm : (a : Fin (Nat.card (↑(s q) : Type))) → (↑(s q) : Type)) ⟨i, hi⟩ =
    Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys
⊢ (↑(((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))) z))) :
      q.Rep) =
    y
have rw : (↑(((E q).symm : (a : Fin (Nat.card (↑(s q) : Type))) → (↑(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:
δ : ℝ
δ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
this : Membership.mem (γ := Set q.Rep) (⋃ y ∈ s q, ball y ε) x
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y ε
i : ℕ :=
  (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type)))
        (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) :
    ℕ)
hi : (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type)))
        (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) :
    ℕ) <
  Nat.card (↑(s q) : Type) :=
  ⋯
ihi_eq :
  (⟨i, hi⟩ : Fin (N q)) =
    (E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (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 (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) ⟨i, hip⟩
C1 : (E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) z = (⟨i, hip⟩ : Fin (Nat.card (↑(s p) : Type)))
C2 : Fin.cast Npq (⟨i, hip⟩ : Fin (N p)) = ⟨i, hi⟩
C3 :
  ((E q).symm : (a : Fin (Nat.card (↑(s q) : Type))) → (↑(s q) : Type)) ⟨i, hi⟩ =
    Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys
rw : (↑(((E q).symm : (a : Fin (Nat.card (↑(s q) : Type))) → (↑(s q) : Type)) (Fin.cast Npq ⟨i, hip⟩)) : q.Rep) = y
⊢ (↑(((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))) z))) :
      q.Rep) =
    y
have rw₁ : (↑(((E q).symm : (a : Fin (Nat.card (↑(s q) : Type))) → (↑(s q) : Type)) ⟨i, hi⟩) : q.Rep) = y
Tactic: rw [C1, C2, C3]
-- 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 : q.Rep
this : Membership.mem (γ := Set q.Rep) (⋃ y ∈ s q, ball y ε) x
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y ε
i : ℕ :=
  (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type)))
        (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) :
    ℕ)
hi : (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type)))
        (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) :
    ℕ) <
  Nat.card (↑(s q) : Type) :=
  ⋯
ihi_eq :
  (⟨i, hi⟩ : Fin (N q)) =
    (E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (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 (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) ⟨i, hip⟩
C1 : (E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) z = (⟨i, hip⟩ : Fin (Nat.card (↑(s p) : Type)))
C2 : Fin.cast Npq (⟨i, hip⟩ : Fin (N p)) = ⟨i, hi⟩
C3 :
  ((E q).symm : (a : Fin (Nat.card (↑(s q) : Type))) → (↑(s q) : Type)) ⟨i, hi⟩ =
    Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys
rw : (↑(((E q).symm : (a : Fin (Nat.card (↑(s q) : Type))) → (↑(s q) : Type)) (Fin.cast Npq ⟨i, hip⟩)) : q.Rep) = y
rw₁ : (↑(((E q).symm : (a : Fin (Nat.card (↑(s q) : Type))) → (↑(s q) : Type)) ⟨i, hi⟩) : q.Rep) = y
⊢ (↑(((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))) 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:
δ : ℝ
δ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
this : Membership.mem (γ := Set q.Rep) (⋃ y ∈ s q, ball y ε) x
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y ε
i : ℕ :=
  (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type)))
        (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) :
    ℕ)
hi : (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type)))
        (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) :
    ℕ) <
  Nat.card (↑(s q) : Type) :=
  ⋯
ihi_eq :
  (⟨i, hi⟩ : Fin (N q)) =
    (E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (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 (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) ⟨i, hip⟩
C1 : (E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) z = (⟨i, hip⟩ : Fin (Nat.card (↑(s p) : Type)))
C2 : Fin.cast Npq (⟨i, hip⟩ : Fin (N p)) = ⟨i, hi⟩
C3 :
  ((E q).symm : (a : Fin (Nat.card (↑(s q) : Type))) → (↑(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:
δ : ℝ
δ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
this_1 : Membership.mem (γ := Set q.Rep) (⋃ y ∈ s q, ball y ε) x
y : q.Rep
ys : y ∈ s q
hy : x ∈ ball y ε
i : ℕ :=
  (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type)))
        (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) :
    ℕ)
hi : (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type)))
        (Subtype.mk (p := fun (x : q.Rep) ↦ x ∈ s q) y ys)) :
    ℕ) <
  Nat.card (↑(s q) : Type) :=
  ⋯
ihi_eq :
  (⟨i, hi⟩ : Fin (N q)) =
    (E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (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 (Nat.card (↑(s p) : Type))) → (↑(s p) : Type)) ⟨i, hip⟩
C1 : (E p : (a : (↑(s p) : Type)) → Fin (Nat.card (↑(s p) : Type))) z = (⟨i, hip⟩ : Fin (Nat.card (↑(s p) : Type)))
C2 : Fin.cast Npq (⟨i, hip⟩ : Fin (N p)) = ⟨i, hi⟩
C3 :
  ((E q).symm : (a : Fin (Nat.card (↑(s q) : Type))) → (↑(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:
δ : ℝ
δ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) : ℕ)
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε
have hip : i < N p
Tactic: have hip : i < N p := ((E p) x).2
-- 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
⊢ i < N q
have rwa : ∀ (hip : i < N q), i < N q
Tactic: rwa [Npq] at hip
Cleared hypotheses: hip
-- 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
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε
have hiq : i < N q
Tactic: have hiq : i < N q := by rwa [Npq] at hip
-- 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
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε
have i' : i = (↑((E q : (a : (↑(s q) : Type)) → Fin (Nat.card (↑(s q) : Type))) (Ψ x)) : ℕ)
Tactic: have i' : i = (E q) (Ψ x) := by simp only [i, Ψ, Equiv.apply_symm_apply, Fin.val_cast]
-- 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) : ℕ)
⊢ |dist x y - dist (Φ x) (Φ y)| ≤ ε
have hjp : j < N p
Tactic: have hjp : j < N p := ((E p) y).2
-- 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
⊢ j < N q
have rwa : ∀ (hjp : j < N q), j < N q
Tactic: rwa [Npq] at hjp
Cleared hypotheses: hjp