awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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
⊢ { 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' }
have 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' }
Tactic: obtain rfl : d = d' := h
Cleared hypotheses: toDist_1, dist_self_1, dist_comm_1, dist_triangle_1, hed', hU', hB', h, d'
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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
⊢ { 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' }
have e_edist : edist = edist_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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
⊢ { 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' }
have e_toUniformSpace : toUniformSpace = toUniformSpace_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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
⊢ { 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' }
have e_toBornology : toBornology = toBornology_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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
⊢ edist = edist_1
have e_edist : ∀ (x y : α), edist x y = edist_1 x y
Tactic: ext x y : 2
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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 : α
⊢ edist x y = edist_1 x y
have e_edist : ENNReal.ofReal (dist x y) = edist_1 x y
Tactic: rw [hed, hed']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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
⊢ edist x y = edist_1 x y
have e_edist₁ : ENNReal.ofReal (dist x y) = ENNReal.ofReal (dist x y)
Tactic: rw [hed, hed']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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
⊢ toBornology = toBornology_1
have e_toBornology : ∀ (s : Set α), s ∈ cobounded α ↔ s ∈ cobounded α
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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 α
⊢ s ∈ cobounded α ↔ s ∈ cobounded α
have e_toBornology : s ∈ (cobounded α).sets ↔ s ∈ cobounded α
Tactic: rw [← Filter.mem_sets, ← Filter.mem_sets, hB, hB']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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 α
⊢ s ∈ cobounded α ↔ s ∈ cobounded α
have e_toBornology₁ : s ∈ (cobounded α).sets ↔ s ∈ (cobounded α).sets
Tactic: rw [← Filter.mem_sets, ← Filter.mem_sets, hB, hB']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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
⊢ s ∈ cobounded α ↔ s ∈ cobounded α
have e_toBornology₂ : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C} s ↔ s ∈ (cobounded α).sets
Tactic: rw [← Filter.mem_sets, ← Filter.mem_sets, hB, hB']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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
⊢ s ∈ cobounded α ↔ s ∈ cobounded α
have 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
Tactic: rw [← Filter.mem_sets, ← Filter.mem_sets, hB, hB']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : α
⊢ dist x y ≤ dist z x + dist z y
have rw : dist x y ≤ dist x z + dist z y
Tactic: rw [dist_comm z]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : α
⊢ dist x y ≤ dist x z + dist y z
have rw : dist x y ≤ dist x z + dist z y
Tactic: rw [dist_comm y]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z w : α
⊢ dist x z + dist z w ≤ dist x y + dist y z + dist z w
have bc : dist x z ≤ dist x y + dist y z
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₂ y₂ ≤ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂)
have rw : dist x₂ y₂ ≤ dist x₂ x₁ + dist x₁ y₁ + dist y₁ y₂
Tactic: rw [add_left_comm, dist_comm x₁, ← add_assoc]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₁ y₁ ≤ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂
have rw : dist x₁ y₁ ≤ dist x₁ x₂ + dist x₂ y₂ + dist y₂ y₁
Tactic: rw [add_right_comm, dist_comm y₁]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
a b c d e f 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
have 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
Tactic: apply le_trans (dist_triangle4 a f g h)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
a b c d e f g h : α
⊢ 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
have bc : dist a f ≤ dist a b + dist b c + dist c d + dist d e + dist e f
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
a b c d e f g h : α
⊢ dist a f ≤ dist a b + dist b c + dist c d + dist d e + dist e f
have 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
Tactic: apply le_trans (dist_triangle4 a d e f)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
a b c d e f g h : α
⊢ dist a d + dist d e + dist e f ≤ dist a b + dist b c + dist c d + dist d e + dist e f
have bc : dist a d ≤ dist a b + dist b c + dist c d
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ Eq.{u + 1} (α := (y x : α) → ℝ) (Function.swap (φ := fun (x y : α) ↦ ℝ) dist) dist
have h : ∀ (x y : α), Function.swap (φ := fun (x y : α) ↦ ℝ) dist x y = dist x y
Tactic: funext x y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ edist x y = (↑(nndist x y) : ℝ≥0∞)
have rw : ENNReal.ofReal (dist x y) = (↑(nndist x y) : ℝ≥0∞)
Tactic: rw [edist_dist, dist_nndist, ENNReal.ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
rw : ENNReal.ofReal (dist x y) = (↑(nndist x y) : ℝ≥0∞)
⊢ edist x y = (↑(nndist x y) : ℝ≥0∞)
have rw₁ : ENNReal.ofReal (↑(nndist x y) : ℝ) = (↑(nndist x y) : ℝ≥0∞)
Tactic: rw [edist_dist, dist_nndist, ENNReal.ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
rw : ENNReal.ofReal (dist x y) = (↑(nndist x y) : ℝ≥0∞)
rw₁ : ENNReal.ofReal (↑(nndist x y) : ℝ) = (↑(nndist x y) : ℝ≥0∞)
⊢ edist x y = (↑(nndist x y) : ℝ≥0∞)
have rw₂ : (↑(nndist x y) : ℝ≥0∞) = (↑(nndist x y) : ℝ≥0∞)
Tactic: rw [edist_dist, dist_nndist, ENNReal.ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
c : ℝ≥0
⊢ edist x y < (↑c : ℝ≥0∞) ↔ nndist x y < c
have rw : (↑(nndist x y) : ℝ≥0∞) < (↑c : ℝ≥0∞) ↔ nndist x y < c
Tactic: rw [edist_nndist, ENNReal.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
c : ℝ≥0
rw : (↑(nndist x y) : ℝ≥0∞) < (↑c : ℝ≥0∞) ↔ nndist x y < c
⊢ edist x y < (↑c : ℝ≥0∞) ↔ nndist x y < c
have rw₁ : nndist x y < c ↔ nndist x y < c
Tactic: rw [edist_nndist, ENNReal.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
c : ℝ≥0
⊢ edist x y ≤ (↑c : ℝ≥0∞) ↔ nndist x y ≤ c
have rw : (↑(nndist x y) : ℝ≥0∞) ≤ (↑c : ℝ≥0∞) ↔ nndist x y ≤ c
Tactic: rw [edist_nndist, ENNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
c : ℝ≥0
rw : (↑(nndist x y) : ℝ≥0∞) ≤ (↑c : ℝ≥0∞) ↔ nndist x y ≤ c
⊢ edist x y ≤ (↑c : ℝ≥0∞) ↔ nndist x y ≤ c
have rw₁ : nndist x y ≤ c ↔ nndist x y ≤ c
Tactic: rw [edist_nndist, ENNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
r : ℝ
⊢ edist x y < ENNReal.ofReal r ↔ dist x y < r
have rw : ENNReal.ofReal (dist x y) < ENNReal.ofReal r ↔ dist x y < r
Tactic: rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff_of_nonneg dist_nonneg]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
r : ℝ
rw : ENNReal.ofReal (dist x y) < ENNReal.ofReal r ↔ dist x y < r
⊢ edist x y < ENNReal.ofReal r ↔ dist x y < r
have rw₁ : dist x y < r ↔ dist x y < r
Tactic: rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff_of_nonneg dist_nonneg]