awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y : (n : ℕ) × X n
m : ℕ := max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m
rw :
  dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) =
    inductiveLimitDist (X := X) f y x
rw₁ :
  dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
⊢ inductiveLimitDist (X := X) f x y = inductiveLimitDist (X := X) f y x
have rw₂ : dist (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
    (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n))) =
  dist (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
    (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
Tactic: rw [inductiveLimitDist_eq_dist I x y m hx hy, inductiveLimitDist_eq_dist I y x m hy hx,
      dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
m : ℕ := max (max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))) (z.fst (β := fun (n : ℕ) ↦ X n))
⊢ inductiveLimitDist (X := X) f x z ≤ inductiveLimitDist (X := X) f x y + inductiveLimitDist (X := X) f y z
have hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
Tactic: have hx : x.1 ≤ m := le_trans (le_max_left _ _) (le_max_left _ _)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
m : ℕ := max (max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))) (z.fst (β := fun (n : ℕ) ↦ X n))
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
⊢ inductiveLimitDist (X := X) f x z ≤ inductiveLimitDist (X := X) f x y + inductiveLimitDist (X := X) f y z
have hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m
Tactic: have hy : y.1 ≤ m := le_trans (le_max_right _ _) (le_max_left _ _)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (hypothesis)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
m : ℕ := max (max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))) (z.fst (β := fun (n : ℕ) ↦ X n))
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m
⊢ inductiveLimitDist (X := X) f x z ≤ inductiveLimitDist (X := X) f x y + inductiveLimitDist (X := X) f y z
have hz : z.fst (β := fun (n : ℕ) ↦ X n) ≤ m
Tactic: have hz : z.1 ≤ m := le_max_right _ _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
m : ℕ := max (max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))) (z.fst (β := fun (n : ℕ) ↦ X n))
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hz : z.fst (β := fun (n : ℕ) ↦ X n) ≤ m
⊢ dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) +
      dist (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hz (fun {k : ℕ} ↦ f k) (z.snd (β := fun (n : ℕ) ↦ X n))) =
    inductiveLimitDist (X := X) f x y + inductiveLimitDist (X := X) f y z
have rw : dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) +
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hz (fun {k : ℕ} ↦ f k) (z.snd (β := fun (n : ℕ) ↦ X n))) =
  dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) +
    inductiveLimitDist (X := X) f y z
Tactic: rw [inductiveLimitDist_eq_dist I x y m hx hy, inductiveLimitDist_eq_dist I y z m hy hz]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
m : ℕ := max (max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))) (z.fst (β := fun (n : ℕ) ↦ X n))
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hz : z.fst (β := fun (n : ℕ) ↦ X n) ≤ m
rw :
  dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) +
      dist (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hz (fun {k : ℕ} ↦ f k) (z.snd (β := fun (n : ℕ) ↦ X n))) =
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) +
      inductiveLimitDist (X := X) f y z
⊢ dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) +
      dist (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
        (leRecOn (C := fun (x : ℕ) ↦ X x) hz (fun {k : ℕ} ↦ f k) (z.snd (β := fun (n : ℕ) ↦ X n))) =
    inductiveLimitDist (X := X) f x y + inductiveLimitDist (X := X) f y z
have rw₁ : dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) +
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hz (fun {k : ℕ} ↦ f k) (z.snd (β := fun (n : ℕ) ↦ X n))) =
  dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) +
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hz (fun {k : ℕ} ↦ f k) (z.snd (β := fun (n : ℕ) ↦ X n)))
Tactic: rw [inductiveLimitDist_eq_dist I x y m hx hy, inductiveLimitDist_eq_dist I y z m hy hz]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
x y z : (n : ℕ) × X n
m : ℕ := max (max (x.fst (β := fun (n : ℕ) ↦ X n)) (y.fst (β := fun (n : ℕ) ↦ X n))) (z.fst (β := fun (n : ℕ) ↦ X n))
hx : x.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hy : y.fst (β := fun (n : ℕ) ↦ X n) ≤ m
hz : z.fst (β := fun (n : ℕ) ↦ X n) ≤ m
⊢ inductiveLimitDist (X := X) f x z ≤ inductiveLimitDist (X := X) f x y + inductiveLimitDist (X := X) f y z
have inductiveLimitDist : dist (leRecOn (C := fun (x : ℕ) ↦ X x) hx (fun {k : ℕ} ↦ f k) (x.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n))) +
    dist (leRecOn (C := fun (x : ℕ) ↦ X x) hy (fun {k : ℕ} ↦ f k) (y.snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) hz (fun {k : ℕ} ↦ f k) (z.snd (β := fun (n : ℕ) ↦ X n))) =
  inductiveLimitDist (X := X) f x y + inductiveLimitDist (X := X) f y z
Tactic: calc
      inductiveLimitDist f x z = dist (leRecOn hx (f _) x.2 : X m) (leRecOn hz (f _) z.2 : X m) :=
        inductiveLimitDist_eq_dist I x z m hx hz
      _ ≤ dist (leRecOn hx (f _) x.2 : X m) (leRecOn hy (f _) y.2 : X m) +
            dist (leRecOn hy (f _) y.2 : X m) (leRecOn hz (f _) z.2 : X m) :=
        (dist_triangle _ _ _)
      _ = inductiveLimitDist f x y + inductiveLimitDist f y z := by
        rw [inductiveLimitDist_eq_dist I x y m hx hy, inductiveLimitDist_eq_dist I y z m hy hz]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x y : X n
⊢ dist (toInductiveLimit (X := X) I n x) (toInductiveLimit (X := X) I n y) = dist x y
have change : inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x) (Sigma.mk (β := fun (n : ℕ) ↦ X n) n y) = dist x y
Tactic: change inductiveLimitDist f ⟨n, x⟩ ⟨n, y⟩ = dist x y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x y : X n
⊢ inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x) (Sigma.mk (β := fun (n : ℕ) ↦ X n) n y) =
    dist x y
have rw : dist
    (leRecOn (C := fun (x : ℕ) ↦ X x) sorry (fun {k : ℕ} ↦ f k)
      ((Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).snd (β := fun (n : ℕ) ↦ X n)))
    (leRecOn (C := fun (x : ℕ) ↦ X x) sorry (fun {k : ℕ} ↦ f k)
      ((Sigma.mk (β := fun (n : ℕ) ↦ X n) n y).snd (β := fun (n : ℕ) ↦ X n))) =
  dist x y
Tactic: rw [inductiveLimitDist_eq_dist I ⟨n, x⟩ ⟨n, y⟩ n (le_refl n) (le_refl n), leRecOn_self,
      leRecOn_self]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x y : X n
rw :
  dist
      (leRecOn (C := fun (x : ℕ) ↦ X x) ⋯ (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) ⋯ (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) n y).snd (β := fun (n : ℕ) ↦ X n))) =
    dist x y
⊢ inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x) (Sigma.mk (β := fun (n : ℕ) ↦ X n) n y) =
    dist x y
have rw₁ : dist ((Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).snd (β := fun (n : ℕ) ↦ X n))
    (leRecOn (C := fun (x : ℕ) ↦ X x) sorry (fun {k : ℕ} ↦ f k)
      ((Sigma.mk (β := fun (n : ℕ) ↦ X n) n y).snd (β := fun (n : ℕ) ↦ X n))) =
  dist x y
Tactic: rw [inductiveLimitDist_eq_dist I ⟨n, x⟩ ⟨n, y⟩ n (le_refl n) (le_refl n), leRecOn_self,
      leRecOn_self]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
x y : X n
rw :
  dist
      (leRecOn (C := fun (x : ℕ) ↦ X x) ⋯ (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).snd (β := fun (n : ℕ) ↦ X n)))
      (leRecOn (C := fun (x : ℕ) ↦ X x) ⋯ (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) n y).snd (β := fun (n : ℕ) ↦ X n))) =
    dist x y
rw₁ :
  dist ((Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).snd (β := fun (n : ℕ) ↦ X n))
      (leRecOn (C := fun (x : ℕ) ↦ X x) ⋯ (fun {k : ℕ} ↦ f k)
        ((Sigma.mk (β := fun (n : ℕ) ↦ X n) n y).snd (β := fun (n : ℕ) ↦ X n))) =
    dist x y
⊢ inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x) (Sigma.mk (β := fun (n : ℕ) ↦ X n) n y) =
    dist x y
have rw₂ : dist ((Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).snd (β := fun (n : ℕ) ↦ X n))
    ((Sigma.mk (β := fun (n : ℕ) ↦ X n) n y).snd (β := fun (n : ℕ) ↦ X n)) =
  dist x y
Tactic: rw [inductiveLimitDist_eq_dist I ⟨n, x⟩ ⟨n, y⟩ n (le_refl n) (le_refl n), leRecOn_self,
      leRecOn_self]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric (X := X) I
x : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace
⊢ toInductiveLimit (X := X) I n.succ ∘ f n = toInductiveLimit (X := X) I n
have h₁ : ∀ (x : X n), (toInductiveLimit (X := X) I n.succ ∘ f n) x = toInductiveLimit (X := X) I n x
Tactic: funext x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric (X := X) I
x_1 : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace
x : X n
⊢ Eq (α := InductiveLimit (X := X) I) (Quotient.mk'' (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x)))
    (Quotient.mk'' (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x))
have h₁ : dist (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x)) (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x) = 0
Tactic: refine SeparationQuotient.mk_eq_mk.2 (Metric.inseparable_iff.2 ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric (X := X) I
x_1 : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace
x : X n
⊢ dist (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x)) (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x) = 0
have h₁ : inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x))
    (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x) =
  0
Tactic: change inductiveLimitDist f ⟨n.succ, f n x⟩ ⟨n, x⟩ = 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric (X := X) I
x_1 : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace
x : X n
⊢ inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x))
      (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x) =
    0
have h₁ : (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).fst (β := fun (n : ℕ) ↦ X n) ≤
  (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).fst (β := fun (n : ℕ) ↦ X n)
Tactic: rw [inductiveLimitDist_eq_dist I ⟨n.succ, f n x⟩ ⟨n, x⟩ n.succ, leRecOn_self,
    leRecOn_succ, leRecOn_self, dist_self]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric (X := X) I
x_1 : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace
x : X n
h₁ :
  (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).fst (β := fun (n : ℕ) ↦ X n) ≤
    (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).fst (β := fun (n : ℕ) ↦ X n)
⊢ inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x))
      (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x) =
    0
have h₂ : (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x)).fst (β := fun (n : ℕ) ↦ X n) ≤
  (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x)).fst (β := fun (n : ℕ) ↦ X n)
Tactic: rw [inductiveLimitDist_eq_dist I ⟨n.succ, f n x⟩ ⟨n, x⟩ n.succ, leRecOn_self,
    leRecOn_succ, leRecOn_self, dist_self]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
n : ℕ
h : PseudoMetricSpace ((n : ℕ) × X n) := inductivePremetric (X := X) I
x_1 : TopologicalSpace ((n : ℕ) × X n) := UniformSpace.toTopologicalSpace
x : X n
h₁ :
  (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).fst (β := fun (n : ℕ) ↦ X n) ≤
    (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).fst (β := fun (n : ℕ) ↦ X n)
h₂ :
  (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x)).fst (β := fun (n : ℕ) ↦ X n) ≤
    (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x)).fst (β := fun (n : ℕ) ↦ X n)
⊢ inductiveLimitDist (X := X) f (Sigma.mk (β := fun (n : ℕ) ↦ X n) n.succ (f n x))
      (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x) =
    0
have h₃ : (Sigma.mk (β := fun (n : ℕ) ↦ X n) n x).fst (β := fun (n : ℕ) ↦ X n) ≤ n.succ
Tactic: rw [inductiveLimitDist_eq_dist I ⟨n.succ, f n x⟩ ⟨n, x⟩ n.succ, leRecOn_self,
    leRecOn_succ, leRecOn_self, dist_self]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
⊢ Dense.{u} (X := InductiveLimit (X := X) I) (⋃ (i : ℕ), range (toInductiveLimit (X := X) I i))
have refine : Subset.{u} (α := Set (InductiveLimit (X := X) I)) univ (⋃ (i : ℕ), range (toInductiveLimit (X := X) I i))
Tactic: refine dense_univ.mono ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
hs : ∀ (n : ℕ), TopologicalSpace.SeparableSpace.{u} (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
⊢ TopologicalSpace.SeparableSpace.{u} (InductiveLimit (X := X) I)
have choose : ∀ (hsX : (n : ℕ) → Set (X n)) (hcX : ∀ (n : ℕ), (hsX n).Countable) (hdX : ∀ (n : ℕ), Dense (hsX n)),
  TopologicalSpace.SeparableSpace.{u} (InductiveLimit (X := X) I)
Tactic: choose hsX hcX hdX using (fun n ↦ TopologicalSpace.exists_countable_dense (X n))
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
hs : ∀ (n : ℕ), TopologicalSpace.SeparableSpace.{u} (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
hsX : (n : ℕ) → Set (X n)
hcX : ∀ (n : ℕ), (hsX n).Countable
hdX : ∀ (n : ℕ), Dense (hsX n)
s : Set (InductiveLimit (X := X) I) := ⋃ (i : ℕ), toInductiveLimit (X := X) I i '' hsX i
⊢ TopologicalSpace.SeparableSpace.{u} (InductiveLimit (X := X) I)
have refine : Dense s
Tactic: refine ⟨s, countable_iUnion (fun n => (hcX n).image _), ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Gluing (goal)
Goal:
X : ℕ → Type u
inst : (n : ℕ) → MetricSpace (X n)
hs : ∀ (n : ℕ), TopologicalSpace.SeparableSpace.{u} (X n)
f : (n : ℕ) → X n → X (n + 1)
I : ∀ (n : ℕ), Isometry (f n)
hsX : (n : ℕ) → Set (X n)
hcX : ∀ (n : ℕ), (hsX n).Countable
hdX : ∀ (n : ℕ), Dense (hsX n)
s : Set (InductiveLimit (X := X) I) := ⋃ (i : ℕ), toInductiveLimit (X := X) I i '' hsX i
⊢ Dense s
have refine : ∀ (i : ℕ), range (toInductiveLimit (X := X) I i) ⊆ closure s
Tactic: refine .of_closure <| (dense_iUnion_range_toInductiveLimit I).mono <| iUnion_subset fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
⊢ ⟦p⟧ = toGHSpace X ↔ ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
have simp : (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop) p
    (NonemptyCompacts.kuratowskiEmbedding X) ↔
  ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Tactic: simp only [toGHSpace, Quotient.eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
⊢ (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
      p (NonemptyCompacts.kuratowskiEmbedding X) ↔
    ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
have refine_1 : ∀
  (h :
    (IsometryRel.setoid :
        NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
      p (NonemptyCompacts.kuratowskiEmbedding X)),
  ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
refine_1 :
  ∀
    (h :
      (IsometryRel.setoid :
          NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
        p (NonemptyCompacts.kuratowskiEmbedding X)),
    ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
⊢ (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
      p (NonemptyCompacts.kuratowskiEmbedding X) ↔
    ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
have refine_2 : (∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) →
  (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
    p (NonemptyCompacts.kuratowskiEmbedding X)
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
h :
  (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
    p (NonemptyCompacts.kuratowskiEmbedding X)
⊢ ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
have refine_1 : ∀ (e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥p),
  ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Tactic: rcases Setoid.symm h with ⟨e⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
h :
  (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
    p (NonemptyCompacts.kuratowskiEmbedding X)
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥p
⊢ ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
have refine_1 : ∀ (f : X ≃ᵢ ↥p), ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Tactic: have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange.trans e
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.GromovHausdorff (goal)
Goal:
X : Type u
inst : MetricSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty X
p : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)
h :
  (IsometryRel.setoid : NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → NonemptyCompacts ↥(lp (fun (n : ℕ) ↦ ℝ) ∞) → Prop)
    p (NonemptyCompacts.kuratowskiEmbedding X)
e : ↥(NonemptyCompacts.kuratowskiEmbedding X) ≃ᵢ ↥p
f : X ≃ᵢ ↥p
⊢ ∃ (Ψ : X → ↥(lp (fun (n : ℕ) ↦ ℝ) ∞)), Isometry Ψ ∧ range Ψ = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
have right : (range fun (x : X) ↦ (↑((f : (a : X) → ↥p) x) : ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))) = (↑p : Set ↥(lp (fun (n : ℕ) ↦ ℝ) ∞))
Tactic: use fun x => f x, isometry_subtype_coe.comp f.isometry