awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y ∈ s, edist x y < δ / 2
F : (x : α) → α := fun (x : α) ↦ ⋯.choose (p := fun (y : α) ↦ y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this_1 : TotallyBounded (↑t : Set α)
a : Set α
af : a.Finite
ta : (↑t : Set α) ⊆ ⋃ y ∈ a, eball y (δ / 2)
b : Set α := F '' a
this_2 : b.Finite
tb : ∀ x ∈ t, ∃ y ∈ b, edist x y < δ
c : Set α := {y : α | y ∈ b ∧ ∃ x ∈ t, edist x y < δ}
this : c.Finite
x : α
hx : x ∈ t
y : α
yv : y ∈ b
Dxy : edist x y < δ
⊢ ∃ y ∈ c, edist x y ≤ δ
have this₁ : y ∈ c
Tactic: have : y ∈ c := by simpa [c, -mem_image] using ⟨yv, ⟨x, hx, Dxy⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y ∈ s, edist x y < δ / 2
F : (x : α) → α := fun (x : α) ↦ ⋯.choose (p := fun (y : α) ↦ y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this_1 : TotallyBounded (↑t : Set α)
a : Set α
af : a.Finite
ta : (↑t : Set α) ⊆ ⋃ y ∈ a, eball y (δ / 2)
b : Set α := F '' a
this_2 : b.Finite
tb : ∀ x ∈ t, ∃ y ∈ b, edist x y < δ
c : Set α := {y : α | y ∈ b ∧ ∃ x ∈ t, edist x y < δ}
this : c.Finite
⊢ ∃ y ∈ v, edist t y < ε
have tc : ∀ x ∈ t, ∃ y ∈ c, edist x y ≤ δ
Tactic: have tc : ∀ x ∈ t, ∃ y ∈ c, edist x y ≤ δ := by
        intro x hx
        rcases tb x hx with ⟨y, yv, Dxy⟩
        have : y ∈ c := by simpa [c, -mem_image] using ⟨yv, ⟨x, hx, Dxy⟩⟩
        exact ⟨y, this, le_of_lt Dxy⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y ∈ s, edist x y < δ / 2
F : (x : α) → α := fun (x : α) ↦ ⋯.choose (p := fun (y : α) ↦ y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this_1 : TotallyBounded (↑t : Set α)
a : Set α
af : a.Finite
ta : (↑t : Set α) ⊆ ⋃ y ∈ a, eball y (δ / 2)
b : Set α := F '' a
this_2 : b.Finite
tb : ∀ x ∈ t, ∃ y ∈ b, edist x y < δ
c : Set α := {y : α | y ∈ b ∧ ∃ x ∈ t, edist x y < δ}
this : c.Finite
tc : ∀ x ∈ t, ∃ y ∈ c, edist x y ≤ δ
y : α
left : y ∈ b
x : α
xt : x ∈ t
Dyx : edist x y < δ
⊢ ∃ x ∈ t, edist y x ≤ δ
have this₁ : edist y x ≤ δ
Tactic: have : edist y x ≤ δ :=
          calc
            edist y x = edist x y := edist_comm _ _
            _ ≤ δ := le_of_lt Dyx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y ∈ s, edist x y < δ / 2
F : (x : α) → α := fun (x : α) ↦ ⋯.choose (p := fun (y : α) ↦ y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this_1 : TotallyBounded (↑t : Set α)
a : Set α
af : a.Finite
ta : (↑t : Set α) ⊆ ⋃ y ∈ a, eball y (δ / 2)
b : Set α := F '' a
this_2 : b.Finite
tb : ∀ x ∈ t, ∃ y ∈ b, edist x y < δ
c : Set α := {y : α | y ∈ b ∧ ∃ x ∈ t, edist x y < δ}
this : c.Finite
tc : ∀ x ∈ t, ∃ y ∈ c, edist x y ≤ δ
⊢ ∃ y ∈ v, edist t y < ε
have ct : ∀ y ∈ c, ∃ x ∈ t, edist y x ≤ δ
Tactic: have ct : ∀ y ∈ c, ∃ x ∈ t, edist y x ≤ δ := by
        rintro y ⟨_, x, xt, Dyx⟩
        have : edist y x ≤ δ :=
          calc
            edist y x = edist x y := edist_comm _ _
            _ ≤ δ := le_of_lt Dyx
        exact ⟨x, xt, this⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y ∈ s, edist x y < δ / 2
F : (x : α) → α := fun (x : α) ↦ ⋯.choose (p := fun (y : α) ↦ y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this_1 : TotallyBounded (↑t : Set α)
a : Set α
af : a.Finite
ta : (↑t : Set α) ⊆ ⋃ y ∈ a, eball y (δ / 2)
b : Set α := F '' a
this_2 : b.Finite
tb : ∀ x ∈ t, ∃ y ∈ b, edist x y < δ
c : Set α := {y : α | y ∈ b ∧ ∃ x ∈ t, edist x y < δ}
this : c.Finite
tc : ∀ x ∈ t, ∃ y ∈ c, edist x y ≤ δ
ct : ∀ y ∈ c, ∃ x ∈ t, edist y x ≤ δ
⊢ ∃ y ∈ v, edist t y < ε
have this₁ : hausdorffEDist (↑t : Set α) c ≤ δ
Tactic: have : hausdorffEDist (t : Set α) c ≤ δ := hausdorffEDist_le_of_mem_edist tc ct
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y ∈ s, edist x y < δ / 2
F : (x : α) → α := fun (x : α) ↦ ⋯.choose (p := fun (y : α) ↦ y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this_1 : TotallyBounded (↑t : Set α)
a : Set α
af : a.Finite
ta : (↑t : Set α) ⊆ ⋃ y ∈ a, eball y (δ / 2)
b : Set α := F '' a
this_2 : b.Finite
tb : ∀ x ∈ t, ∃ y ∈ b, edist x y < δ
c : Set α := {y : α | y ∈ b ∧ ∃ x ∈ t, edist x y < δ}
this_3 : c.Finite
tc : ∀ x ∈ t, ∃ y ∈ c, edist x y ≤ δ
ct : ∀ y ∈ c, ∃ x ∈ t, edist y x ≤ δ
this : hausdorffEDist (↑t : Set α) c ≤ δ
⊢ ∃ y ∈ v, edist t y < ε
have Dtc : hausdorffEDist (↑t : Set α) c < ε
Tactic: have Dtc : hausdorffEDist (t : Set α) c < ε := this.trans_lt δlt
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y ∈ s, edist x y < δ / 2
F : (x : α) → α := fun (x : α) ↦ ⋯.choose (p := fun (y : α) ↦ y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this_1 : TotallyBounded (↑t : Set α)
a : Set α
af : a.Finite
ta : (↑t : Set α) ⊆ ⋃ y ∈ a, eball y (δ / 2)
b : Set α := F '' a
this_2 : b.Finite
tb : ∀ x ∈ t, ∃ y ∈ b, edist x y < δ
c : Set α := {y : α | y ∈ b ∧ ∃ x ∈ t, edist x y < δ}
this_3 : c.Finite
tc : ∀ x ∈ t, ∃ y ∈ c, edist x y ≤ δ
ct : ∀ y ∈ c, ∃ x ∈ t, edist y x ≤ δ
this : hausdorffEDist (↑t : Set α) c ≤ δ
Dtc : hausdorffEDist (↑t : Set α) c < ε
⊢ ∃ y ∈ v, edist t y < ε
have hc : c.Nonempty
Tactic: have hc : c.Nonempty := nonempty_of_hausdorffEDist_ne_top t.nonempty (ne_top_of_lt Dtc)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y ∈ s, edist x y < δ / 2
F : (x : α) → α := fun (x : α) ↦ ⋯.choose (p := fun (y : α) ↦ y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this_1 : TotallyBounded (↑t : Set α)
a : Set α
af : a.Finite
ta : (↑t : Set α) ⊆ ⋃ y ∈ a, eball y (δ / 2)
b : Set α := F '' a
this_2 : b.Finite
tb : ∀ x ∈ t, ∃ y ∈ b, edist x y < δ
c : Set α := {y : α | y ∈ b ∧ ∃ x ∈ t, edist x y < δ}
this_3 : c.Finite
tc : ∀ x ∈ t, ∃ y ∈ c, edist x y ≤ δ
ct : ∀ y ∈ c, ∃ x ∈ t, edist y x ≤ δ
this : hausdorffEDist (↑t : Set α) c ≤ δ
Dtc : hausdorffEDist (↑t : Set α) c < ε
hc : c.Nonempty
d : NonemptyCompacts α := { carrier := c, isCompact' := ⋯, nonempty' := hc }
x : α
hx : x ∈ c
⊢ x ∈ s
have rcases : ∀ y ∈ a, ∀ (yx : F y = x), x ∈ s
Tactic: rcases (mem_image _ _ _).1 hx.1 with ⟨y, ⟨_, yx⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y ∈ s, edist x y < δ / 2
F : (x : α) → α := fun (x : α) ↦ ⋯.choose (p := fun (y : α) ↦ y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this_1 : TotallyBounded (↑t : Set α)
a : Set α
af : a.Finite
ta : (↑t : Set α) ⊆ ⋃ y ∈ a, eball y (δ / 2)
b : Set α := F '' a
this_2 : b.Finite
tb : ∀ x ∈ t, ∃ y ∈ b, edist x y < δ
c : Set α := {y : α | y ∈ b ∧ ∃ x ∈ t, edist x y < δ}
this_3 : c.Finite
tc : ∀ x ∈ t, ∃ y ∈ c, edist x y ≤ δ
ct : ∀ y ∈ c, ∃ x ∈ t, edist y x ≤ δ
this : hausdorffEDist (↑t : Set α) c ≤ δ
Dtc : hausdorffEDist (↑t : Set α) c < ε
hc : c.Nonempty
d : NonemptyCompacts α := { carrier := c, isCompact' := ⋯, nonempty' := hc }
x : α
hx : x ∈ c
y : α
left : y ∈ a
yx : F y = x
⊢ x ∈ s
have rw : F y ∈ s
Tactic: rw [← yx]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y ∈ s, edist x y < δ / 2
F : (x : α) → α := fun (x : α) ↦ ⋯.choose (p := fun (y : α) ↦ y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this_1 : TotallyBounded (↑t : Set α)
a : Set α
af : a.Finite
ta : (↑t : Set α) ⊆ ⋃ y ∈ a, eball y (δ / 2)
b : Set α := F '' a
this_2 : b.Finite
tb : ∀ x ∈ t, ∃ y ∈ b, edist x y < δ
c : Set α := {y : α | y ∈ b ∧ ∃ x ∈ t, edist x y < δ}
this_3 : c.Finite
tc : ∀ x ∈ t, ∃ y ∈ c, edist x y ≤ δ
ct : ∀ y ∈ c, ∃ x ∈ t, edist y x ≤ δ
this : hausdorffEDist (↑t : Set α) c ≤ δ
Dtc : hausdorffEDist (↑t : Set α) c < ε
hc : c.Nonempty
d : NonemptyCompacts α := { carrier := c, isCompact' := ⋯, nonempty' := hc }
⊢ ∃ y ∈ v, edist t y < ε
have this₁ : c ⊆ s
Tactic: have : c ⊆ s := by
        intro x hx
        rcases (mem_image _ _ _).1 hx.1 with ⟨y, ⟨_, yx⟩⟩
        rw [← yx]
        exact (Fspec y).1
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
s_1 : Set α
inst_2 : SecondCountableTopology α
s : Set α
cs : s.Countable
s_dense : Dense s
v0 : Set (Set α) := {t : Set α | t.Finite ∧ t ⊆ s}
v : Set (NonemptyCompacts α) := {t : NonemptyCompacts α | (↑t : Set α) ∈ v0}
t : NonemptyCompacts α
ε : ℝ≥0∞
εpos : ε > 0
δ : ℝ≥0∞
δpos : 0 < δ
δlt : δ < ε
δpos' : 0 < δ / 2
Exy : ∀ (x : α), ∃ y ∈ s, edist x y < δ / 2
F : (x : α) → α := fun (x : α) ↦ ⋯.choose (p := fun (y : α) ↦ y ∈ s ∧ edist x y < δ / 2)
Fspec : ∀ (x : α), F x ∈ s ∧ edist x (F x) < δ / 2
this_1 : TotallyBounded (↑t : Set α)
a : Set α
af : a.Finite
ta : (↑t : Set α) ⊆ ⋃ y ∈ a, eball y (δ / 2)
b : Set α := F '' a
this_2 : b.Finite
tb : ∀ x ∈ t, ∃ y ∈ b, edist x y < δ
c : Set α := {y : α | y ∈ b ∧ ∃ x ∈ t, edist x y < δ}
this_3 : c.Finite
tc : ∀ x ∈ t, ∃ y ∈ c, edist x y ≤ δ
ct : ∀ y ∈ c, ∃ x ∈ t, edist y x ≤ δ
this_4 : hausdorffEDist (↑t : Set α) c ≤ δ
Dtc : hausdorffEDist (↑t : Set α) c < ε
hc : c.Nonempty
d : NonemptyCompacts α := { carrier := c, isCompact' := ⋯, nonempty' := hc }
this : c ⊆ s
⊢ ∃ y ∈ v, edist t y < ε
have this₁ : d ∈ v
Tactic: have : d ∈ v := ⟨‹c.Finite›, this⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
Goal:
α : Type u_1
inst : MetricSpace α
x : α
s t : NonemptyCompacts α
⊢ infDist x (↑s : Set α) ≤ infDist x (↑t : Set α) + dist s t
have rw : infDist x (↑s : Set α) ≤ infDist x (↑t : Set α) + dist t s
Tactic: rw [dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Closeds (goal)
Goal:
α : Type u_1
inst : MetricSpace α
⊢ LipschitzWith (β := ℝ) 2 fun (p : α × NonemptyCompacts α) ↦ infDist p.1 (↑p.2 : Set α)
have rw : LipschitzWith (β := ℝ) (HAdd.hAdd (α := NNReal) 1 1) fun (p : α × NonemptyCompacts α) ↦ infDist p.1 (↑p.2 : Set α)
Tactic: rw [← one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : Completion α
⊢ dist x x = 0
have refine_1 : IsClosed.{u} (X := Completion α) {a : Completion α | dist a a = 0}
Tactic: refine induction_on x ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : Completion α
refine_1 : IsClosed.{u} (X := Completion α) {a : Completion α | dist a a = 0}
⊢ dist x x = 0
have refine_2 : ∀ (a : α), dist (α := Completion α) (↑a : Completion α) (↑a : Completion α) = 0
Tactic: refine induction_on x ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : Completion α
⊢ IsClosed.{u} (X := Completion α) {a : Completion α | dist a a = 0}
have refine_1 : Continuous (Y := ℝ) fun (a : Completion α) ↦ dist a a
Tactic: refine isClosed_eq ?_ continuous_const
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : Completion α
a : α
⊢ dist (α := Completion α) (↑a : Completion α) (↑a : Completion α) = 0
have refine_2 : dist a a = 0
Tactic: rw [Completion.dist_eq, dist_self]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : Completion α
a : α
refine_2 : dist a a = 0
⊢ dist (α := Completion α) (↑a : Completion α) (↑a : Completion α) = 0
have refine_2₁ : Eq (α := ℝ) 0 0
Tactic: rw [Completion.dist_eq, dist_self]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : Completion α
⊢ dist x y = dist y x
have refine_1 : IsClosed.{u} (X := Completion α × Completion α) {x : Completion α × Completion α | dist x.1 x.2 = dist x.2 x.1}
Tactic: refine induction_on₂ x y ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : Completion α
refine_1 :
  IsClosed.{u} (X := Completion α × Completion α) {x : Completion α × Completion α | dist x.1 x.2 = dist x.2 x.1}
⊢ dist x y = dist y x
have refine_2 : ∀ (a b : α),
  dist (α := Completion α) (↑a : Completion α) (↑b : Completion α) =
    dist (α := Completion α) (↑b : Completion α) (↑a : Completion α)
Tactic: refine induction_on₂ x y ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : Completion α
a b : α
⊢ dist (α := Completion α) (↑a : Completion α) (↑b : Completion α) =
    dist (α := Completion α) (↑b : Completion α) (↑a : Completion α)
have refine_2 : dist a b = dist (α := Completion α) (↑b : Completion α) (↑a : Completion α)
Tactic: rw [Completion.dist_eq, Completion.dist_eq, dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : Completion α
a b : α
refine_2 : dist a b = dist (α := Completion α) (↑b : Completion α) (↑a : Completion α)
⊢ dist (α := Completion α) (↑a : Completion α) (↑b : Completion α) =
    dist (α := Completion α) (↑b : Completion α) (↑a : Completion α)
have refine_2₁ : dist a b = dist b a
Tactic: rw [Completion.dist_eq, Completion.dist_eq, dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : Completion α
a b : α
refine_2 : dist a b = dist (α := Completion α) (↑b : Completion α) (↑a : Completion α)
refine_2₁ : dist a b = dist b a
⊢ dist (α := Completion α) (↑a : Completion α) (↑b : Completion α) =
    dist (α := Completion α) (↑b : Completion α) (↑a : Completion α)
have refine_2₂ : dist b a = dist b a
Tactic: rw [Completion.dist_eq, Completion.dist_eq, dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : Completion α
⊢ dist x z ≤ dist x y + dist y z
have refine_1 : IsClosed.{u} (X := Completion α × Completion α × Completion α)
  {x : Completion α × Completion α × Completion α | dist x.1 x.2.2 ≤ dist x.1 x.2.1 + dist x.2.1 x.2.2}
Tactic: refine induction_on₃ x y z ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : Completion α
refine_1 :
  IsClosed.{u} (X := Completion α × Completion α × Completion α)
    {x : Completion α × Completion α × Completion α | dist x.1 x.2.2 ≤ dist x.1 x.2.1 + dist x.2.1 x.2.2}
⊢ dist x z ≤ dist x y + dist y z
have refine_2 : ∀ (a b c : α),
  dist (α := Completion α) (↑a : Completion α) (↑c : Completion α) ≤
    dist (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
      dist (α := Completion α) (↑b : Completion α) (↑c : Completion α)
Tactic: refine induction_on₃ x y z ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : Completion α
⊢ IsClosed.{u} (X := Completion α × Completion α × Completion α)
    {x : Completion α × Completion α × Completion α | dist x.1 x.2.2 ≤ dist x.1 x.2.1 + dist x.2.1 x.2.2}
have refine_1 : Continuous (Y := ℝ) fun (x : Completion α × Completion α × Completion α) ↦ dist x.1 x.2.2
Tactic: refine isClosed_le ?_ (Continuous.add ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : Completion α
refine_1 : Continuous (Y := ℝ) fun (x : Completion α × Completion α × Completion α) ↦ dist x.1 x.2.2
⊢ IsClosed.{u} (X := Completion α × Completion α × Completion α)
    {x : Completion α × Completion α × Completion α | dist x.1 x.2.2 ≤ dist x.1 x.2.1 + dist x.2.1 x.2.2}
have refine_1₁ : Continuous (Y := ℝ) fun (x : Completion α × Completion α × Completion α) ↦ dist x.1 x.2.1
Tactic: refine isClosed_le ?_ (Continuous.add ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : Completion α
refine_1 : Continuous (Y := ℝ) fun (x : Completion α × Completion α × Completion α) ↦ dist x.1 x.2.2
refine_1₁ : Continuous (Y := ℝ) fun (x : Completion α × Completion α × Completion α) ↦ dist x.1 x.2.1
⊢ IsClosed.{u} (X := Completion α × Completion α × Completion α)
    {x : Completion α × Completion α × Completion α | dist x.1 x.2.2 ≤ dist x.1 x.2.1 + dist x.2.1 x.2.2}
have refine_1₂ : Continuous (Y := ℝ) fun (x : Completion α × Completion α × Completion α) ↦ dist x.2.1 x.2.2
Tactic: refine isClosed_le ?_ (Continuous.add ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist (α := Completion α) (↑a : Completion α) (↑c : Completion α) ≤
    dist (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
      dist (α := Completion α) (↑b : Completion α) (↑c : Completion α)
have refine_2 : dist a c ≤ dist a b + dist b c
Tactic: rw [Completion.dist_eq, Completion.dist_eq, Completion.dist_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s ↔
    ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
have mp : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s →
  ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
mp :
  Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s →
    ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
⊢ Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s ↔
    ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
have mpr : (∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s) →
  Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
⊢ ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
have mp : ∀ (t : Set (Completion α × Completion α))
  (ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t) (tclosed : IsClosed t)
  (ts : t ⊆ s), ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
Tactic: rcases mem_uniformity_isClosed hs with ⟨t, ht, ⟨tclosed, ts⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
⊢ ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
have A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
Tactic: have A : { x : α × α | (↑x.1, ↑x.2) ∈ t } ∈ uniformity α :=
      uniformContinuous_def.1 (uniformContinuous_coe α) t ht
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
t : Set (Completion α × Completion α)
ht : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t
tclosed : IsClosed t
ts : t ⊆ s
A : {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} ∈ 𝓤 α
⊢ ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
have mp : ∀ (ε : ℝ) (εpos : ε > 0)
  (hε :
    ∀ ⦃a b : α⦄,
      dist a b < ε →
        Membership.mem (γ := Set (α × α)) {x : α × α | ((↑x.1 : Completion α), (↑x.2 : Completion α)) ∈ t} (a, b)),
  ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
Tactic: rcases mem_uniformity_dist.1 A with ⟨ε, εpos, hε⟩