awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Closeds
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
⊢ F y ∈ s

Tactic:
(Fspec y).1

Premises used: And.left
-- Module: Mathlib.Topology.MetricSpace.Closeds
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
⊢ F y ∈ s

Tactic:
exact (Fspec y).1

Premises used: And.left
-- Module: Mathlib.Topology.MetricSpace.Closeds
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 }
⊢ 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
-- Module: Mathlib.Topology.MetricSpace.Closeds
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
⊢ d ∈ v

Tactic:
have : d ∈ v := ⟨‹c.Finite›, this⟩
-- Module: Mathlib.Topology.MetricSpace.Closeds
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_5 : c ⊆ s
this : d ∈ v
⊢ ∃ y ∈ v, edist t y < ε

Tactic:
⟨d, ‹d ∈ v›, Dtc⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Closeds
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_5 : c ⊆ s
this : d ∈ v
⊢ ∃ y ∈ v, edist t y < ε

Tactic:
exact ⟨d, ‹d ∈ v›, Dtc⟩
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
⊢ Isometry (β := NonemptyCompacts α) fun (x : α) ↦ {x}

Tactic:
fun _ _ => hausdorffEDist_singleton

Premises used: setOf, Set.singleton, Metric.hausdorffEDist_singleton, Isometry
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : EMetricSpace α
⊢ LipschitzWith (β := NonemptyCompacts α) 1 fun (p : NonemptyCompacts α × NonemptyCompacts α) ↦ p.1 ⊔ p.2

Tactic:
.of_edist_le fun _ _ => hausdorffEDist_union_le

Premises used: LipschitzWith.of_edist_le, Metric.hausdorffEDist_union_le
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : EMetricSpace α
inst_1 : EMetricSpace β
⊢ LipschitzWith (β := NonemptyCompacts (α × β)) 1 fun (p : Prod.{u_1, u_2} (NonemptyCompacts α) (NonemptyCompacts β)) ↦
    p.1 ×ˢ p.2

Tactic:
.of_edist_le fun _ _ => hausdorffEDist_prod_le

Premises used: LipschitzWith.of_edist_le, Metric.hausdorffEDist_prod_le
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : MetricSpace α
x y : NonemptyCompacts α
⊢ dist x y = hausdorffDist (↑x : Set α) (↑y : Set α)

Tactic:
rfl

Premises used: Metric.hausdorffDist, rfl
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : MetricSpace α
x : α
s t : NonemptyCompacts α
rw : infDist x (↑s : Set α) ≤ infDist x (↑t : Set α) + dist t s
⊢ infDist x (↑s : Set α) ≤ infDist x (↑t : Set α) + dist s t

Tactic:
rw [dist_comm]

Premises used: dist_comm
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : MetricSpace α
x : α
s t : NonemptyCompacts α
⊢ infDist x (↑s : Set α) ≤ infDist x (↑t : Set α) + dist t s

Tactic:
infDist_le_infDist_add_hausdorffDist (edist_ne_top t s)

Premises used: Metric.hausdorffDist, edist_ne_top, Metric.infDist_le_infDist_add_hausdorffDist
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : MetricSpace α
x : α
s t : NonemptyCompacts α
⊢ infDist x (↑s : Set α) ≤ infDist x (↑t : Set α) + dist t s

Tactic:
exact infDist_le_infDist_add_hausdorffDist (edist_ne_top t s)

Premises used: edist_ne_top, Metric.infDist_le_infDist_add_hausdorffDist
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : MetricSpace α
rw : LipschitzWith (β := ℝ) (HAdd.hAdd (α := NNReal) 1 1) fun (p : α × NonemptyCompacts α) ↦ infDist p.1 (↑p.2 : Set α)
⊢ LipschitzWith (β := ℝ) 2 fun (p : α × NonemptyCompacts α) ↦ infDist p.1 (↑p.2 : Set α)

Tactic:
rw [← one_add_one_eq_two]

Premises used: one_add_one_eq_two
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : MetricSpace α
⊢ LipschitzWith (β := ℝ) (HAdd.hAdd (α := NNReal) 1 1) fun (p : α × NonemptyCompacts α) ↦ infDist p.1 (↑p.2 : Set α)

Tactic:
LipschitzWith.uncurry
    (fun s : NonemptyCompacts α => lipschitz_infDist_pt (s : Set α)) lipschitz_infDist_set

Premises used: Metric.infDist, LipschitzWith.uncurry, ENNReal.toReal, SetLike.coe, Metric.lipschitz_infDist_pt, Metric.lipschitz_infDist_set, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : MetricSpace α
⊢ LipschitzWith (β := ℝ) (HAdd.hAdd (α := NNReal) 1 1) fun (p : α × NonemptyCompacts α) ↦ infDist p.1 (↑p.2 : Set α)

Tactic:
exact LipschitzWith.uncurry
    (fun s : NonemptyCompacts α => lipschitz_infDist_pt (s : Set α)) lipschitz_infDist_set

Premises used: LipschitzWith.uncurry, SetLike.coe, Metric.lipschitz_infDist_pt, Metric.lipschitz_infDist_set
-- Module: Mathlib.Topology.MetricSpace.Closeds
Goal:
α : Type u_1
inst : MetricSpace α
⊢ UniformContinuous (β := ℝ) fun (p : α × NonemptyCompacts α) ↦ infDist p.1 (↑p.2 : Set α)

Tactic:
lipschitz_infDist.uniformContinuous

Premises used: Set.Mem, setOf, LipschitzWith.uniformContinuous, Metric.lipschitz_infDist
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ UniformContinuous (β := ℝ) fun (p : Completion α × Completion α) ↦ dist p.1 p.2

Tactic:
uniformContinuous_extension₂ dist

Premises used: UniformContinuous₂, UniformSpace.Completion.uniformContinuous_extension₂, Dist.dist
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
f g : β → Completion α
hf : Continuous[inst_1, _] f
hg : Continuous[inst_1, _] g
⊢ Continuous[inst_1, _] fun (x : β) ↦ dist (f x) (g x)

Tactic:
Completion.uniformContinuous_dist.continuous.comp (hf.prodMk hg :)

Premises used: UniformSpace.Completion.uniformContinuous_dist, Continuous.comp, UniformContinuous.continuous, Continuous.prodMk
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ dist (α := Completion α) (↑x : Completion α) (↑y : Completion α) = dist x y

Tactic:
Completion.extension₂_coe_coe uniformContinuous_dist _ _

Premises used: uniformContinuous_dist, UniformSpace.Completion.extension₂_coe_coe
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x : Completion α
⊢ dist x x = 0

Tactic:
induction_on x ?_ ?_

Premises used: UniformSpace.Completion.induction_on
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x : Completion α
refine_1 : IsClosed.{u} (X := Completion α) {a : Completion α | dist a a = 0}
refine_2 : ∀ (a : α), dist (α := Completion α) (↑a : Completion α) (↑a : Completion α) = 0
⊢ dist x x = 0

Tactic:
refine induction_on x ?_ ?_
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x : Completion α
⊢ IsClosed.{u} (X := Completion α) {a : Completion α | dist a a = 0}

Tactic:
isClosed_eq ?_ continuous_const

Premises used: continuous_const, isClosed_eq
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x : Completion α
refine_1 : Continuous (Y := ℝ) fun (a : Completion α) ↦ dist a a
⊢ IsClosed.{u} (X := Completion α) {a : Completion α | dist a a = 0}

Tactic:
refine isClosed_eq ?_ continuous_const

Premises used: continuous_const, isClosed_eq
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x : Completion α
⊢ Continuous (Y := ℝ) fun (a : Completion α) ↦ dist a a

Tactic:
Completion.continuous_dist continuous_id continuous_id

Premises used: continuous_id, UniformSpace.Completion.continuous_dist
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x : Completion α
⊢ Continuous (Y := ℝ) fun (a : Completion α) ↦ dist a a

Tactic:
exact Completion.continuous_dist continuous_id continuous_id

Premises used: continuous_id, UniformSpace.Completion.continuous_dist
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x : Completion α
a : α
refine_2 : dist a a = 0
refine_2₁ refine_2₂ : Eq (α := ℝ) 0 0
⊢ dist (α := Completion α) (↑a : Completion α) (↑a : Completion α) = 0

Tactic:
rw [Completion.dist_eq, dist_self]

Premises used: UniformSpace.Completion.dist_eq, dist_self
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : Completion α
⊢ dist x y = dist y x

Tactic:
induction_on₂ x y ?_ ?_

Premises used: UniformSpace.Completion.induction_on₂
-- Module: Mathlib.Topology.MetricSpace.Completion
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}
refine_2 :
  ∀ (a b : α),
    dist (α := Completion α) (↑a : Completion α) (↑b : Completion α) =
      dist (α := Completion α) (↑b : Completion α) (↑a : Completion α)
⊢ dist x y = dist y x

Tactic:
refine induction_on₂ x y ?_ ?_
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : Completion α
⊢ IsClosed.{u} (X := Completion α × Completion α) {x : Completion α × Completion α | dist x.1 x.2 = dist x.2 x.1}

Tactic:
isClosed_eq (Completion.continuous_dist continuous_fst continuous_snd)
        (Completion.continuous_dist continuous_snd continuous_fst)

Premises used: continuous_snd, continuous_fst, isClosed_eq, UniformSpace.Completion.continuous_dist
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : Completion α
⊢ IsClosed.{u} (X := Completion α × Completion α) {x : Completion α × Completion α | dist x.1 x.2 = dist x.2 x.1}

Tactic:
exact isClosed_eq (Completion.continuous_dist continuous_fst continuous_snd)
        (Completion.continuous_dist continuous_snd continuous_fst)

Premises used: continuous_snd, continuous_fst, isClosed_eq, UniformSpace.Completion.continuous_dist
-- Module: Mathlib.Topology.MetricSpace.Completion
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
refine_2₂ refine_2₃ : dist b a = dist b a
⊢ dist (α := Completion α) (↑a : Completion α) (↑b : Completion α) =
    dist (α := Completion α) (↑b : Completion α) (↑a : Completion α)

Tactic:
rw [Completion.dist_eq, Completion.dist_eq, dist_comm]

Premises used: UniformSpace.Completion.dist_eq, dist_comm
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : Completion α
⊢ dist x z ≤ dist x y + dist y z

Tactic:
induction_on₃ x y z ?_ ?_

Premises used: UniformSpace.Completion.induction_on₃
-- Module: Mathlib.Topology.MetricSpace.Completion
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}
refine_2 :
  ∀ (a b c : α),
    dist (α := Completion α) (↑a : Completion α) (↑c : Completion α) ≤
      dist (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
        dist (α := Completion α) (↑b : Completion α) (↑c : Completion α)
⊢ dist x z ≤ dist x y + dist y z

Tactic:
refine induction_on₃ x y z ?_ ?_
-- Module: Mathlib.Topology.MetricSpace.Completion
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}

Tactic:
isClosed_le ?_ (Continuous.add ?_ ?_)

Premises used: setOf, isClosed_le, Continuous.add
-- Module: Mathlib.Topology.MetricSpace.Completion
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
refine_1₂ : Continuous (Y := ℝ) fun (x : Completion α × Completion α × Completion α) ↦ dist x.2.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}

Tactic:
refine isClosed_le ?_ (Continuous.add ?_ ?_)

Premises used: isClosed_le, Continuous.add
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : Completion α
⊢ Continuous (Y := ℝ) fun (x : Completion α × Completion α × Completion α) ↦ dist x.1 x.2.2

Tactic:
apply_rules [Completion.continuous_dist, Continuous.fst, Continuous.snd, continuous_id]

Premises used: Continuous.snd, continuous_id, Continuous.fst, UniformSpace.Completion.continuous_dist
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : Completion α
⊢ Continuous (Y := ℝ) fun (x : Completion α × Completion α × Completion α) ↦ dist x.1 x.2.1

Tactic:
apply_rules [Completion.continuous_dist, Continuous.fst, Continuous.snd, continuous_id]

Premises used: Continuous.snd, continuous_id, Continuous.fst, UniformSpace.Completion.continuous_dist
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : Completion α
⊢ Continuous (Y := ℝ) fun (x : Completion α × Completion α × Completion α) ↦ dist x.2.1 x.2.2

Tactic:
apply_rules [Completion.continuous_dist, Continuous.fst, Continuous.snd, continuous_id]

Premises used: Continuous.snd, continuous_id, Continuous.fst, UniformSpace.Completion.continuous_dist
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : Completion α
a b c : α
refine_2 : dist a c ≤ dist a b + dist b c
⊢ dist (α := Completion α) (↑a : Completion α) (↑c : Completion α) ≤
    dist (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
      dist (α := Completion α) (↑b : Completion α) (↑c : Completion α)

Tactic:
rw [Completion.dist_eq, Completion.dist_eq, Completion.dist_eq]

Premises used: UniformSpace.Completion.dist_eq
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist a c ≤ dist a b + dist b c

Tactic:
dist_triangle a b c

Premises used: dist_triangle
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : Completion α
a b c : α
⊢ dist a c ≤ dist a b + dist b c

Tactic:
exact dist_triangle a b c

Premises used: dist_triangle
-- Module: Mathlib.Topology.MetricSpace.Completion
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
mpr :
  (∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s) →
    Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
⊢ Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s ↔
    ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
hs : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s
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
⊢ ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s

Tactic:
rcases mem_uniformity_isClosed hs with ⟨t, ht, ⟨tclosed, ts⟩⟩

Premises used: mem_uniformity_isClosed
-- Module: Mathlib.Topology.MetricSpace.Completion
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
⊢ {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
-- Module: Mathlib.Topology.MetricSpace.Completion
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} ∈ 𝓤 α
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
⊢ ∃ ε > 0, ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s

Tactic:
rcases mem_uniformity_dist.1 A with ⟨ε, εpos, hε⟩

Premises used: Metric.mem_uniformity_dist, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Completion
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} ∈ 𝓤 α
ε : ℝ
ε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:
⟨ε, εpos, @fun x y hxy ↦ ?_⟩

Premises used: And.intro, Exists.intro