awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
α : Type u_3
dist : α → α → ℝ
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
s t : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ t
Cs : ℝ
hs : ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ Cs
Ct : ℝ
ht : ∀ ⦃x : α⦄, x ∈ t → ∀ ⦃y : α⦄, y ∈ t → dist x y ≤ Ct
⊢ ∃ (C : ℝ), ∀ z ∈ s ∪ t, dist x z ≤ C

Tactic:
refine ⟨max Cs (dist x y + Ct), fun z hz => hz.elim
        (fun hz => (hs hx hz).trans (le_max_left _ _))
        (fun hz => (dist_triangle x y z).trans <|
          (add_le_add le_rfl (ht hy hz)).trans (le_max_right _ _))⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Sort u_3
x y : α
dist : α → α → ℝ
dist_self : ∀ (x : α), dist x x = 0
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
rw : dist x y + dist y x = dist x y + dist x y
rw₁ rw₂ : dist y x + dist y x = dist y x + dist y x
⊢ dist x y + dist y x = 2 * dist x y

Tactic:
rw [two_mul, dist_comm]

Premises used: two_mul
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
m m' : PseudoMetricSpace α
h : Eq.{u_3 + 1} (α := Dist α) toDist toDist
d : Dist α := toDist
obtain :
  ∀ [toDist : Dist α] (dist_self : ∀ (x : α), dist x x = 0) (dist_comm : ∀ (x y : α), dist x y = dist y x)
    (dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z) (edist : α → α → ℝ≥0∞)
    (hed : ∀ (x y : α), edist x y = ENNReal.ofReal (dist x y)) (toUniformSpace : UniformSpace α)
    (hU : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}) (toBornology : Bornology α)
    (hB : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C})
    (h : Eq.{u_3 + 1} (α := Dist α) PseudoMetricSpace.toDist PseudoMetricSpace.toDist),
    { toDist := toDist, dist_self := dist_self, dist_comm := dist_comm, dist_triangle := dist_triangle, edist := edist,
        edist_dist := hed, toUniformSpace := toUniformSpace, uniformity_dist := hU, toBornology := toBornology,
        cobounded_sets := hB : PseudoMetricSpace α } =
      m'
⊢ m = m'

Tactic:
obtain ⟨_, _, _, _, hed, _, hU, _, hB⟩ := m
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
m' : PseudoMetricSpace α
toDist : Dist α
dist_self : ∀ (x : α), dist x x = 0
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist x y = ENNReal.ofReal (dist x y)
toUniformSpace : UniformSpace α
hU : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
toBornology : Bornology α
hB : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
h : Eq.{u_3 + 1} (α := Dist α) PseudoMetricSpace.toDist PseudoMetricSpace.toDist
d : Dist α := PseudoMetricSpace.toDist
d' : Dist α := PseudoMetricSpace.toDist
obtain :
  ∀ [toDist_1 : Dist α] (dist_self_1 : ∀ (x : α), dist x x = 0) (dist_comm_1 : ∀ (x y : α), dist x y = dist y x)
    (dist_triangle_1 : ∀ (x y z : α), dist x z ≤ dist x y + dist y z) (edist_1 : α → α → ℝ≥0∞)
    (hed' : ∀ (x y : α), edist_1 x y = ENNReal.ofReal (dist x y)) (toUniformSpace_1 : UniformSpace α)
    (hU' : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}) (toBornology_1 : Bornology α)
    (hB' : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C})
    (h : Eq.{u_3 + 1} (α := Dist α) PseudoMetricSpace.toDist PseudoMetricSpace.toDist),
    { toDist := toDist, dist_self := dist_self, dist_comm := dist_comm, dist_triangle := dist_triangle, edist := edist,
        edist_dist := hed, toUniformSpace := toUniformSpace, uniformity_dist := hU, toBornology := toBornology,
        cobounded_sets := hB : PseudoMetricSpace α } =
      { toDist := toDist_1, dist_self := dist_self_1, dist_comm := dist_comm_1, dist_triangle := dist_triangle_1,
        edist := edist_1, edist_dist := hed', toUniformSpace := toUniformSpace_1, uniformity_dist := hU',
        toBornology := toBornology_1, cobounded_sets := hB' }
⊢ { toDist := toDist, dist_self := dist_self, dist_comm := dist_comm, dist_triangle := dist_triangle, edist := edist,
      edist_dist := hed, toUniformSpace := toUniformSpace, uniformity_dist := hU, toBornology := toBornology,
      cobounded_sets := hB : PseudoMetricSpace α } =
    m'

Tactic:
obtain ⟨_, _, _, _, hed', _, hU', _, hB'⟩ := m'
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
toDist : Dist α
dist_self : ∀ (x : α), dist x x = 0
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist x y = ENNReal.ofReal (dist x y)
toUniformSpace : UniformSpace α
hU : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
toBornology : Bornology α
hB : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d : Dist α := PseudoMetricSpace.toDist
toDist_1 : Dist α
dist_self_1 : ∀ (x : α), dist x x = 0
dist_comm_1 : ∀ (x y : α), dist x y = dist y x
dist_triangle_1 : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist_1 : α → α → ℝ≥0∞
hed' : ∀ (x y : α), edist_1 x y = ENNReal.ofReal (dist x y)
toUniformSpace_1 : UniformSpace α
hU' : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
toBornology_1 : Bornology α
hB' : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
h : Eq.{u_3 + 1} (α := Dist α) PseudoMetricSpace.toDist PseudoMetricSpace.toDist
d' : Dist α := PseudoMetricSpace.toDist
⊢ d = d'

Tactic:
h
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
toDist : Dist α
dist_self : ∀ (x : α), dist x x = 0
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist x y = ENNReal.ofReal (dist x y)
toUniformSpace : UniformSpace α
hU : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
toBornology : Bornology α
hB : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d : Dist α := PseudoMetricSpace.toDist
toDist_1 : Dist α
dist_self_1 : ∀ (x : α), dist x x = 0
dist_comm_1 : ∀ (x y : α), dist x y = dist y x
dist_triangle_1 : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist_1 : α → α → ℝ≥0∞
hed' : ∀ (x y : α), edist_1 x y = ENNReal.ofReal (dist x y)
toUniformSpace_1 : UniformSpace α
hU' : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
toBornology_1 : Bornology α
hB' : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
h : Eq.{u_3 + 1} (α := Dist α) PseudoMetricSpace.toDist PseudoMetricSpace.toDist
d' : Dist α := PseudoMetricSpace.toDist
obtain :
  ∀ (dist_self_2 : ∀ (x : α), dist x x = 0) (dist_comm_2 : ∀ (x y : α), dist x y = dist y x)
    (dist_triangle_2 : ∀ (x y z : α), dist x z ≤ dist x y + dist y z)
    (hed' : ∀ (x y : α), edist_1 x y = ENNReal.ofReal (dist x y))
    (hU' : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε})
    (hB' : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}),
    { toDist := toDist, dist_self := dist_self, dist_comm := dist_comm, dist_triangle := dist_triangle, edist := edist,
        edist_dist := hed, toUniformSpace := toUniformSpace, uniformity_dist := hU, toBornology := toBornology,
        cobounded_sets := hB : PseudoMetricSpace α } =
      { toDist := d, dist_self := dist_self_2, dist_comm := dist_comm_2, dist_triangle := dist_triangle_2,
        edist := edist_1, edist_dist := hed', toUniformSpace := toUniformSpace_1, uniformity_dist := hU',
        toBornology := toBornology_1, cobounded_sets := hB' }
⊢ { toDist := toDist, dist_self := dist_self, dist_comm := dist_comm, dist_triangle := dist_triangle, edist := edist,
      edist_dist := hed, toUniformSpace := toUniformSpace, uniformity_dist := hU, toBornology := toBornology,
      cobounded_sets := hB : PseudoMetricSpace α } =
    { toDist := toDist_1, dist_self := dist_self_1, dist_comm := dist_comm_1, dist_triangle := dist_triangle_1,
      edist := edist_1, edist_dist := hed', toUniformSpace := toUniformSpace_1, uniformity_dist := hU',
      toBornology := toBornology_1, cobounded_sets := hB' }

Tactic:
obtain rfl : d = d' := h

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
toDist : Dist α
dist_self : ∀ (x : α), dist x x = 0
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist x y = ENNReal.ofReal (dist x y)
toUniformSpace : UniformSpace α
hU : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
toBornology : Bornology α
hB : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d : Dist α := PseudoMetricSpace.toDist
edist_1 : α → α → ℝ≥0∞
toUniformSpace_1 : UniformSpace α
toBornology_1 : Bornology α
dist_self_1 : ∀ (x : α), dist x x = 0
dist_comm_1 : ∀ (x y : α), dist x y = dist y x
dist_triangle_1 : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
hed' : ∀ (x y : α), edist_1 x y = ENNReal.ofReal (dist x y)
hU' : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
hB' : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d' : Dist α := PseudoMetricSpace.toDist
e_edist : edist = edist_1
e_toUniformSpace : toUniformSpace = toUniformSpace_1
e_toBornology : toBornology = toBornology_1
⊢ { toDist := toDist, dist_self := dist_self, dist_comm := dist_comm, dist_triangle := dist_triangle, edist := edist,
      edist_dist := hed, toUniformSpace := toUniformSpace, uniformity_dist := hU, toBornology := toBornology,
      cobounded_sets := hB : PseudoMetricSpace α } =
    { toDist := d, dist_self := dist_self_1, dist_comm := dist_comm_1, dist_triangle := dist_triangle_1,
      edist := edist_1, edist_dist := hed', toUniformSpace := toUniformSpace_1, uniformity_dist := hU',
      toBornology := toBornology_1, cobounded_sets := hB' }

Tactic:
congr
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
toDist : Dist α
dist_self : ∀ (x : α), dist x x = 0
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist x y = ENNReal.ofReal (dist x y)
toUniformSpace : UniformSpace α
hU : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
toBornology : Bornology α
hB : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d : Dist α := PseudoMetricSpace.toDist
edist_1 : α → α → ℝ≥0∞
toUniformSpace_1 : UniformSpace α
toBornology_1 : Bornology α
dist_self_1 : ∀ (x : α), dist x x = 0
dist_comm_1 : ∀ (x y : α), dist x y = dist y x
dist_triangle_1 : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
hed' : ∀ (x y : α), edist_1 x y = ENNReal.ofReal (dist x y)
hU' : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
hB' : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d' : Dist α := PseudoMetricSpace.toDist
e_edist : ∀ (x y : α), edist x y = edist_1 x y
⊢ edist = edist_1

Tactic:
ext x y : 2
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
toDist : Dist α
dist_self : ∀ (x : α), dist x x = 0
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist x y = ENNReal.ofReal (dist x y)
toUniformSpace : UniformSpace α
hU : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
toBornology : Bornology α
hB : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d : Dist α := PseudoMetricSpace.toDist
edist_1 : α → α → ℝ≥0∞
toUniformSpace_1 : UniformSpace α
toBornology_1 : Bornology α
dist_self_1 : ∀ (x : α), dist x x = 0
dist_comm_1 : ∀ (x y : α), dist x y = dist y x
dist_triangle_1 : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
hed' : ∀ (x y : α), edist_1 x y = ENNReal.ofReal (dist x y)
hU' : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
hB' : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d' : Dist α := PseudoMetricSpace.toDist
x y : α
e_edist : ENNReal.ofReal (dist x y) = edist_1 x y
e_edist₁ e_edist₂ : ENNReal.ofReal (dist x y) = ENNReal.ofReal (dist x y)
⊢ edist x y = edist_1 x y

Tactic:
rw [hed, hed']
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
toDist : Dist α
dist_self : ∀ (x : α), dist x x = 0
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist x y = ENNReal.ofReal (dist x y)
toUniformSpace : UniformSpace α
hU : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
toBornology : Bornology α
hB : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d : Dist α := PseudoMetricSpace.toDist
edist_1 : α → α → ℝ≥0∞
toUniformSpace_1 : UniformSpace α
toBornology_1 : Bornology α
dist_self_1 : ∀ (x : α), dist x x = 0
dist_comm_1 : ∀ (x y : α), dist x y = dist y x
dist_triangle_1 : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
hed' : ∀ (x y : α), edist_1 x y = ENNReal.ofReal (dist x y)
hU' : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
hB' : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d' : Dist α := PseudoMetricSpace.toDist
⊢ toUniformSpace = toUniformSpace_1

Tactic:
UniformSpace.ext (hU.trans hU'.symm)

Premises used: UniformSpace.ext, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
toDist : Dist α
dist_self : ∀ (x : α), dist x x = 0
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist x y = ENNReal.ofReal (dist x y)
toUniformSpace : UniformSpace α
hU : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
toBornology : Bornology α
hB : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d : Dist α := PseudoMetricSpace.toDist
edist_1 : α → α → ℝ≥0∞
toUniformSpace_1 : UniformSpace α
toBornology_1 : Bornology α
dist_self_1 : ∀ (x : α), dist x x = 0
dist_comm_1 : ∀ (x y : α), dist x y = dist y x
dist_triangle_1 : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
hed' : ∀ (x y : α), edist_1 x y = ENNReal.ofReal (dist x y)
hU' : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
hB' : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d' : Dist α := PseudoMetricSpace.toDist
⊢ toUniformSpace = toUniformSpace_1

Tactic:
exact UniformSpace.ext (hU.trans hU'.symm)

Premises used: UniformSpace.ext, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
toDist : Dist α
dist_self : ∀ (x : α), dist x x = 0
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist x y = ENNReal.ofReal (dist x y)
toUniformSpace : UniformSpace α
hU : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
toBornology : Bornology α
hB : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d : Dist α := PseudoMetricSpace.toDist
edist_1 : α → α → ℝ≥0∞
toUniformSpace_1 : UniformSpace α
toBornology_1 : Bornology α
dist_self_1 : ∀ (x : α), dist x x = 0
dist_comm_1 : ∀ (x y : α), dist x y = dist y x
dist_triangle_1 : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
hed' : ∀ (x y : α), edist_1 x y = ENNReal.ofReal (dist x y)
hU' : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
hB' : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d' : Dist α := PseudoMetricSpace.toDist
e_toBornology : ∀ (s : Set α), s ∈ cobounded α ↔ s ∈ cobounded α
⊢ toBornology = toBornology_1

Tactic:
ext : 2
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
toDist : Dist α
dist_self : ∀ (x : α), dist x x = 0
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
edist : α → α → ℝ≥0∞
hed : ∀ (x y : α), edist x y = ENNReal.ofReal (dist x y)
toUniformSpace : UniformSpace α
hU : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
toBornology : Bornology α
hB : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d : Dist α := PseudoMetricSpace.toDist
edist_1 : α → α → ℝ≥0∞
toUniformSpace_1 : UniformSpace α
toBornology_1 : Bornology α
dist_self_1 : ∀ (x : α), dist x x = 0
dist_comm_1 : ∀ (x y : α), dist x y = dist y x
dist_triangle_1 : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
hed' : ∀ (x y : α), edist_1 x y = ENNReal.ofReal (dist x y)
hU' : 𝓤 α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | dist p.1 p.2 < ε}
hB' : (cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
d' : Dist α := PseudoMetricSpace.toDist
s : Set α
e_toBornology : s ∈ (cobounded α).sets ↔ s ∈ cobounded α
e_toBornology₁ : s ∈ (cobounded α).sets ↔ s ∈ (cobounded α).sets
e_toBornology₂ :
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C} s ↔ s ∈ (cobounded α).sets
e_toBornology₃ e_toBornology₄ :
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C} s ↔
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C} s
⊢ s ∈ cobounded α ↔ s ∈ cobounded α

Tactic:
rw [← Filter.mem_sets, ← Filter.mem_sets, hB, hB']

Premises used: Filter.mem_sets
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ dist x x = 0

Tactic:
PseudoMetricSpace.dist_self x

Premises used: PseudoMetricSpace.dist_self
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ dist x y = dist y x

Tactic:
PseudoMetricSpace.dist_comm x y

Premises used: PseudoMetricSpace.dist_comm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ edist x y = ENNReal.ofReal (dist x y)

Tactic:
PseudoMetricSpace.edist_dist x y

Premises used: PseudoMetricSpace.edist_dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : α
⊢ dist x z ≤ dist x y + dist y z

Tactic:
PseudoMetricSpace.dist_triangle x y z

Premises used: PseudoMetricSpace.dist_triangle
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : α
rw : dist x y ≤ dist x z + dist z y
⊢ dist x y ≤ dist z x + dist z y

Tactic:
rw [dist_comm z]

Premises used: dist_comm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : α
⊢ dist x y ≤ dist x z + dist z y

Tactic:
apply dist_triangle

Premises used: dist_triangle
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : α
rw : dist x y ≤ dist x z + dist z y
⊢ dist x y ≤ dist x z + dist y z

Tactic:
rw [dist_comm y]

Premises used: dist_comm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z w : α
bc : dist x z ≤ dist x y + dist y z
⊢ dist x z + dist z w ≤ dist x y + dist y z + dist z w

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z w : α
⊢ dist x z ≤ dist x y + dist y z

Tactic:
apply dist_triangle x y z

Premises used: dist_triangle
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
rw : dist x₂ y₂ ≤ dist x₂ x₁ + dist x₁ y₁ + dist y₁ y₂
⊢ dist x₂ y₂ ≤ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂)

Tactic:
rw [add_left_comm, dist_comm x₁, ← add_assoc]

Premises used: add_left_comm, add_assoc, dist_comm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₂ y₂ ≤ dist x₂ x₁ + dist x₁ y₁ + dist y₁ y₂

Tactic:
apply dist_triangle4

Premises used: dist_triangle4
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
rw : dist x₁ y₁ ≤ dist x₁ x₂ + dist x₂ y₂ + dist y₂ y₁
⊢ dist x₁ y₁ ≤ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂

Tactic:
rw [add_right_comm, dist_comm y₁]

Premises used: add_right_comm, dist_comm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₁ y₁ ≤ dist x₁ x₂ + dist x₂ y₂ + dist y₂ y₁

Tactic:
apply dist_triangle4

Premises used: dist_triangle4
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
a b c d e f g h : α
apply : dist a f + dist f g + dist g h ≤ dist a b + dist b c + dist c d + dist d e + dist e f + dist f g + dist g h
⊢ dist a h ≤ dist a b + dist b c + dist c d + dist d e + dist e f + dist f g + dist g h

Tactic:
apply le_trans (dist_triangle4 a f g h)

Premises used: dist_triangle4, le_trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
a b c d e f g h : α
bc : dist a f ≤ dist a b + dist b c + dist c d + dist d e + dist e f
⊢ dist a f + dist f g + dist g h ≤ dist a b + dist b c + dist c d + dist d e + dist e f + dist f g + dist g h

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
a b c d e f g h : α
bc : dist a d + dist d e + dist e f ≤ dist a b + dist b c + dist c d + dist d e + dist e f
⊢ dist a f ≤ dist a b + dist b c + dist c d + dist d e + dist e f

Tactic:
apply le_trans (dist_triangle4 a d e f)

Premises used: dist_triangle4, le_trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
a b c d e f g h : α
bc : dist a d ≤ dist a b + dist b c + dist c d
⊢ dist a d + dist d e + dist e f ≤ dist a b + dist b c + dist c d + dist d e + dist e f

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
a b c d e f g h : α
⊢ dist a d ≤ dist a b + dist b c + dist c d

Tactic:
dist_triangle4 a b c d

Premises used: dist_triangle4
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
a b c d e f g h : α
⊢ dist a d ≤ dist a b + dist b c + dist c d

Tactic:
exact dist_triangle4 a b c d

Premises used: dist_triangle4
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
h : ∀ (x y : α), Function.swap (φ := fun (x y : α) ↦ ℝ) dist x y = dist x y
⊢ Eq.{u + 1} (α := (y x : α) → ℝ) (Function.swap (φ := fun (x y : α) ↦ ℝ) dist) dist

Tactic:
funext x y
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ Function.swap (φ := fun (x y : α) ↦ ℝ) dist x y = dist x y

Tactic:
dist_comm _ _

Premises used: dist_comm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ Function.swap (φ := fun (x y : α) ↦ ℝ) dist x y = dist x y

Tactic:
exact dist_comm _ _

Premises used: dist_comm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : α
⊢ |dist x z - dist y z| ≤ dist x y

Tactic:
abs_sub_le_iff.2
    ⟨sub_le_iff_le_add.2 (dist_triangle _ _ _), sub_le_iff_le_add.2 (dist_triangle_left _ _ _)⟩

Premises used: dist_triangle, Iff.mpr, abs_sub_le_iff, sub_le_iff_le_add, dist_triangle_left, And.intro
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ 0 ≤ dist x y

Tactic:
dist_nonneg' dist dist_self dist_comm dist_triangle

Premises used: dist_triangle, dist_comm, dist_self, _private.0.dist_nonneg', Dist.dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
x y : α
⊢ 0 ≤ dist x y

Tactic:
positivity
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
a b : α
⊢ |dist a b| = dist a b

Tactic:
abs_of_nonneg dist_nonneg

Premises used: dist_nonneg, abs_of_nonneg
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ dist x y = (↑(nndist x y) : ℝ)

Tactic:
rfl

Premises used: NNReal.toReal, rfl