awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
d : α → α → ℝ≥0
simp :
  (∀ (i : ℝ≥0∞) (i_1 : i > 0),
      Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ) < ε})
        {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < i}) ∧
    ∀ (i : ℝ) (i_1 : i > 0),
      Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε})
        {p : α × α | (↑(d p.1 p.2) : ℝ) < i}
⊢ Eq.{u_3 + 1} (α := Filter (α × α)) (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ) < ε})
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε})

Tactic:
simp only [le_antisymm_iff, le_iInf_iff, le_principal_iff]

Premises used: Filter.le_principal_iff, le_iInf_iff, le_antisymm_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
d : α → α → ℝ≥0
⊢ (∀ (i : ℝ≥0∞) (i_1 : i > 0),
      Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ) < ε})
        {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < i}) ∧
    ∀ (i : ℝ) (i_1 : i > 0),
      Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε})
        {p : α × α | (↑(d p.1 p.2) : ℝ) < i}

Tactic:
⟨fun ε hε => ?_, fun ε hε => ?_⟩

Premises used: And.intro
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
d : α → α → ℝ≥0
refine_1 :
  ∀ (ε : ℝ≥0∞) (hε : ε > 0),
    Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ) < ε})
      {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε}
refine_2 :
  ∀ (ε : ℝ) (hε : ε > 0),
    Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε})
      {p : α × α | (↑(d p.1 p.2) : ℝ) < ε}
⊢ (∀ (i : ℝ≥0∞) (i_1 : i > 0),
      Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ) < ε})
        {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < i}) ∧
    ∀ (i : ℝ) (i_1 : i > 0),
      Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε})
        {p : α × α | (↑(d p.1 p.2) : ℝ) < i}

Tactic:
refine ⟨fun ε hε => ?_, fun ε hε => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
refine_1 :
  ∀ (ε' : ℝ≥0) (ε'0 : 0 < (↑ε' : ℝ≥0∞)) (ε'ε : (↑ε' : ℝ≥0∞) < ε),
    Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ) < ε})
      {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε}
⊢ Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ) < ε})
    {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε}

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hε with ⟨ε', ε'0, ε'ε⟩

Premises used: ENNReal.lt_iff_exists_nnreal_btwn, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
ε' : ℝ≥0
ε'0 : 0 < (↑ε' : ℝ≥0∞)
ε'ε : (↑ε' : ℝ≥0∞) < ε
⊢ Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ) < ε})
    {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε}

Tactic:
mem_iInf_of_mem (ε' : ℝ) (mem_iInf_of_mem (ENNReal.coe_pos.1 ε'0) ?_)

Premises used: Filter.mem_iInf_of_mem, ENNReal.coe_pos, Iff.mp, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
ε' : ℝ≥0
ε'0 : 0 < (↑ε' : ℝ≥0∞)
ε'ε : (↑ε' : ℝ≥0∞) < ε
refine_1 :
  Membership.mem (γ := Filter (α × α)) (𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ) < (↑ε' : ℝ)})
    {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε}
⊢ Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ) < ε})
    {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε}

Tactic:
refine mem_iInf_of_mem (ε' : ℝ) (mem_iInf_of_mem (ENNReal.coe_pos.1 ε'0) ?_)

Premises used: Filter.mem_iInf_of_mem, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
ε' : ℝ≥0
ε'0 : 0 < (↑ε' : ℝ≥0∞)
ε'ε : (↑ε' : ℝ≥0∞) < ε
⊢ Membership.mem (γ := Filter (α × α)) (𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ) < (↑ε' : ℝ)})
    {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε}

Tactic:
fun x hx => lt_trans (ENNReal.coe_lt_coe.2 hx) ε'ε

Premises used: Iff.mpr, Set.Mem, setOf, lt_trans, ENNReal.coe_lt_coe, Set.Subset
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
ε' : ℝ≥0
ε'0 : 0 < (↑ε' : ℝ≥0∞)
ε'ε : (↑ε' : ℝ≥0∞) < ε
⊢ Membership.mem (γ := Filter (α × α)) (𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ) < (↑ε' : ℝ)})
    {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε}

Tactic:
exact fun x hx => lt_trans (ENNReal.coe_lt_coe.2 hx) ε'ε

Premises used: Iff.mpr, lt_trans, ENNReal.coe_lt_coe
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ
hε : ε > 0
⊢ 0 ≤ ε

Tactic:
le_of_lt hε

Premises used: le_of_lt
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ
hε : ε > 0
refine_2 :
  ∀ (ε : ℝ≥0) (hε : (↑ε : ℝ) > 0),
    Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε})
      {p : α × α | (↑(d p.1 p.2) : ℝ) < (↑ε : ℝ)}
⊢ Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε})
    {p : α × α | (↑(d p.1 p.2) : ℝ) < ε}

Tactic:
lift ε to ℝ≥0 using le_of_lt hε

Premises used: le_of_lt
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0
hε : (↑ε : ℝ) > 0
⊢ Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε})
    {p : α × α | (↑(d p.1 p.2) : ℝ) < (↑ε : ℝ)}

Tactic:
mem_iInf_of_mem (ε : ℝ≥0∞) (mem_iInf_of_mem (ENNReal.coe_pos.2 hε) ?_)

Premises used: Iff.mpr, ENNReal.ofNNReal, Filter.mem_iInf_of_mem, ENNReal.coe_pos
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0
hε : (↑ε : ℝ) > 0
refine_2 :
  Membership.mem (γ := Filter (α × α)) (𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < (↑ε : ℝ≥0∞)})
    {p : α × α | (↑(d p.1 p.2) : ℝ) < (↑ε : ℝ)}
⊢ Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε})
    {p : α × α | (↑(d p.1 p.2) : ℝ) < (↑ε : ℝ)}

Tactic:
refine mem_iInf_of_mem (ε : ℝ≥0∞) (mem_iInf_of_mem (ENNReal.coe_pos.2 hε) ?_)

Premises used: ENNReal.ofNNReal, Filter.mem_iInf_of_mem
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0
hε : (↑ε : ℝ) > 0
⊢ Membership.mem (γ := Filter (α × α)) (𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < (↑ε : ℝ≥0∞)})
    {p : α × α | (↑(d p.1 p.2) : ℝ) < (↑ε : ℝ)}

Tactic:
fun _ => ENNReal.coe_lt_coe.1

Premises used: Set.Mem, setOf, ENNReal.coe_lt_coe, Set.Subset, Iff.mp, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0
hε : (↑ε : ℝ) > 0
⊢ Membership.mem (γ := Filter (α × α)) (𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < (↑ε : ℝ≥0∞)})
    {p : α × α | (↑(d p.1 p.2) : ℝ) < (↑ε : ℝ)}

Tactic:
exact fun _ => ENNReal.coe_lt_coe.1

Premises used: ENNReal.coe_lt_coe, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ 𝓤 α = ⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | edist p.1 p.2 < ε}

Tactic:
simp only [PseudoMetricSpace.uniformity_dist, dist_nndist, edist_nndist,
    Metric.uniformity_edist_aux]

Premises used: dist_nndist, PseudoMetricSpace.uniformity_dist, edist_nndist, Metric.uniformity_edist_aux
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
⊢ ∀ (x : α), edist x x = 0

Tactic:
simp [edist_dist]

Premises used: PseudoMetricSpace.edist_dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
x x_1 : α
⊢ edist x x_1 = edist x_1 x

Tactic:
simp only [edist_dist, dist_comm]

Premises used: PseudoMetricSpace.dist_comm, PseudoMetricSpace.edist_dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
x y z : α
simp : ENNReal.ofReal (dist x z) ≤ ENNReal.ofReal (dist x y + dist y z)
⊢ edist x z ≤ edist x y + edist y z

Tactic:
simp only [edist_dist, ← ENNReal.ofReal_add, dist_nonneg]

Premises used: dist_nonneg, ENNReal.ofReal_add, PseudoMetricSpace.edist_dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
x y z : α
rw : dist x z ≤ dist x y + dist y z
rw₁ : 0 ≤ dist x y + dist y z
⊢ ENNReal.ofReal (dist x z) ≤ ENNReal.ofReal (dist x y + dist y z)

Tactic:
rw [ENNReal.ofReal_le_ofReal_iff _]

Premises used: ENNReal.ofReal_le_ofReal_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
x y z : α
⊢ dist x z ≤ dist x y + dist y z

Tactic:
dist_triangle _ _ _

Premises used: PseudoMetricSpace.dist_triangle
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
x y z : α
⊢ dist x z ≤ dist x y + dist y z

Tactic:
exact dist_triangle _ _ _

Premises used: PseudoMetricSpace.dist_triangle
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
x y z : α
⊢ 0 ≤ dist x y + dist y z

Tactic:
simpa using add_le_add (dist_nonneg : 0 ≤ dist x y) dist_nonneg

Premises used: add_le_add, dist_nonneg
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ eball x ∞ = univ

Tactic:
Set.eq_univ_iff_forall.mpr fun y => edist_lt_top y x

Premises used: Iff.mpr, Set.eq_univ_iff_forall, edist_lt_top
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
h : ∀ (y : α), y ∈ eball x (ENNReal.ofReal ε) ↔ y ∈ ball x ε
⊢ eball x (ENNReal.ofReal ε) = ball x ε

Tactic:
ext y
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
y : α
h : ENNReal.ofReal (dist y x) < ENNReal.ofReal ε ↔ dist y x < ε
⊢ y ∈ eball x (ENNReal.ofReal ε) ↔ y ∈ ball x ε

Tactic:
simp only [mem_eball, mem_ball, edist_dist]

Premises used: Metric.mem_ball, edist_dist, Metric.mem_eball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ ENNReal.ofReal (dist y x) < ENNReal.ofReal ε ↔ dist y x < ε

Tactic:
ENNReal.ofReal_lt_ofReal_iff_of_nonneg dist_nonneg

Premises used: ENNReal.ofReal_lt_ofReal_iff_of_nonneg, dist_nonneg
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ ENNReal.ofReal (dist y x) < ENNReal.ofReal ε ↔ dist y x < ε

Tactic:
exact ENNReal.ofReal_lt_ofReal_iff_of_nonneg dist_nonneg

Premises used: ENNReal.ofReal_lt_ofReal_iff_of_nonneg, dist_nonneg
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ≥0
rw : eball x (↑ε : ℝ≥0∞) = eball x (ENNReal.ofReal (↑ε : ℝ))
⊢ eball x (↑ε : ℝ≥0∞) = ball x (↑ε : ℝ)

Tactic:
rw [← eball_ofReal]

Premises used: Metric.eball_ofReal
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ eball x (↑ε : ℝ≥0∞) = eball x (ENNReal.ofReal (↑ε : ℝ))

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 ≤ ε
h₁ : ∀ (y : α), y ∈ closedEBall x (ENNReal.ofReal ε) ↔ y ∈ closedBall x ε
⊢ closedEBall x (ENNReal.ofReal ε) = closedBall x ε

Tactic:
ext y
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 ≤ ε
y : α
⊢ y ∈ closedEBall x (ENNReal.ofReal ε) ↔ y ∈ closedBall x ε

Tactic:
simp [edist_le_ofReal h]

Premises used: edist_le_ofReal
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ≥0
rw : closedEBall x (↑ε : ℝ≥0∞) = closedEBall x (ENNReal.ofReal (↑ε : ℝ))
rw₁ rw₂ : closedEBall x (↑ε : ℝ≥0∞) = closedEBall x (↑ε : ℝ≥0∞)
⊢ closedEBall x (↑ε : ℝ≥0∞) = closedBall x (↑ε : ℝ)

Tactic:
rw [← closedEBall_ofReal ε.coe_nonneg, ENNReal.ofReal_coe_nnreal]

Premises used: Metric.closedEBall_ofReal, NNReal.coe_nonneg, ENNReal.ofReal_coe_nnreal
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ eball x ∞ = univ

Tactic:
eq_univ_of_forall fun _ => edist_lt_top _ _

Premises used: Set.eq_univ_of_forall, edist_lt_top
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
U : UniformSpace α
m : PseudoMetricSpace α
H : 𝓤 α = 𝓤 α
h : ∀ (x x_1 : α), dist x x_1 = dist x x_1
⊢ m.replaceUniformity H = m

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
U : UniformSpace α
m : PseudoMetricSpace α
H : 𝓤 α = 𝓤 α
x x_1 : α
⊢ dist x x_1 = dist x x_1

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α_1
α : Type u_3
U : UniformSpace α
m : PseudoMetricSpace α
H : 𝓤 α = 𝓤 α
⊢ Eq.{u_3 + 1} (α := Bornology α) PseudoMetricSpace.toBornology PseudoMetricSpace.toBornology

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α_1
α : Type u_3
U : UniformSpace α
m : PseudoMetricSpace α
H : 𝓤 α = 𝓤 α
⊢ Eq.{u_3 + 1} (α := Bornology α) PseudoMetricSpace.toBornology PseudoMetricSpace.toBornology

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
γ : Type u_3
U : TopologicalSpace γ
m : PseudoMetricSpace γ
H : U = UniformSpace.toTopologicalSpace
h : ∀ (x x_1 : γ), dist x x_1 = dist x x_1
⊢ m.replaceTopology H = m

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
γ : Type u_3
U : TopologicalSpace γ
m : PseudoMetricSpace γ
H : U = UniformSpace.toTopologicalSpace
x x_1 : γ
⊢ dist x x_1 = dist x x_1

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
X_1 : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
X : Type u_3
e : PseudoEMetricSpace X
dist : X → X → ℝ
dist_nonneg : ∀ (x y : X), 0 ≤ dist x y
h : ∀ (x y : X), edist x y = ENNReal.ofReal (dist x y)
x : X
⊢ dist x x = 0

Tactic:
simpa [h, (dist_nonneg _ _).ge_iff_eq', -edist_self] using edist_self x

Premises used: PseudoEMetricSpace.edist_self, LE.le.ge_iff_eq'
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
X_1 : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
X : Type u_3
e : PseudoEMetricSpace X
dist : X → X → ℝ
dist_nonneg : ∀ (x y : X), 0 ≤ dist x y
h : ∀ (x y : X), edist x y = ENNReal.ofReal (dist x y)
x y : X
⊢ dist x y = dist y x

Tactic:
simpa [h, dist_nonneg] using edist_comm x y

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
X_1 : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
X : Type u_3
e : PseudoEMetricSpace X
dist : X → X → ℝ
dist_nonneg : ∀ (x y : X), 0 ≤ dist x y
h : ∀ (x y : X), edist x y = ENNReal.ofReal (dist x y)
x y z : X
⊢ dist x z ≤ dist x y + dist y z

Tactic:
simpa [h, dist_nonneg, add_nonneg, ← ENNReal.ofReal_add] using edist_triangle x y z

Premises used: add_nonneg, ENNReal.ofReal_add, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
X_1 : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
X : Type u_3
e : PseudoEMetricSpace X
dist : X → X → ℝ
dist_nonneg : ∀ (x y : X), 0 ≤ dist x y
h : ∀ (x y : X), edist x y = ENNReal.ofReal (dist x y)
x x_1 : X
⊢ edist x x_1 = ENNReal.ofReal (dist x x_1)

Tactic:
simp only [h]
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
X_1 : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
X : Type u_3
e : PseudoEMetricSpace X
dist : X → X → ℝ
dist_nonneg : ∀ (x y : X), 0 ≤ dist x y
h : ∀ (x y : X), edist x y = ENNReal.ofReal (dist x y)
⊢ Eq.{u_3 + 1} (α := Filter (X × X)) (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : X × X | edist p.1 p.2 < ε})
    (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : X × X | dist p.1 p.2 < ε})

Tactic:
simpa [h, dist_nonneg, ENNReal.coe_toNNReal_eq_toReal]
      using (Metric.uniformity_edist_aux fun x y : X => (edist x y).toNNReal).symm

Premises used: ENNReal.coe_toNNReal_eq_toReal, ENNReal.toNNReal, EDist.edist, Eq.symm, Metric.uniformity_edist_aux
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α_1
α : Type u
inst_1 : PseudoEMetricSpace α
h : ∀ (x y : α), edist x y ≠ ∞
⊢ ∀ (x y : α), LE.le (α := ℝ) 0 ((fun (x1 x2 : α) ↦ (edist x1 x2).toReal) x y)

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α_1
α : Type u
inst_1 : PseudoEMetricSpace α
h : ∀ (x y : α), edist x y ≠ ∞
⊢ ∀ (x y : α), edist x y = ENNReal.ofReal ((fun (x1 x2 : α) ↦ (edist x1 x2).toReal) x y)

Tactic:
simp [h]
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α_1
α : Type u_3
B : Bornology α
m : PseudoMetricSpace α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
s : Set α
rw :
  (∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C) ↔
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C} sᶜ
rw₁ : (∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C) ↔ ∃ (C : ℝ), ∀ x ∈ sᶜᶜ, ∀ y ∈ sᶜᶜ, dist x y ≤ C
rw₂ rw₃ : (∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C) ↔ ∃ (C : ℝ), ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C
⊢ Bornology.IsBounded s ↔ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C} sᶜ

Tactic:
rw [isBounded_iff, mem_setOf_eq, compl_compl]

Premises used: compl_compl, Metric.isBounded_iff, Set.mem_setOf_eq
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
m : PseudoMetricSpace α
B : Bornology α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
h : ∀ (x x_1 : α), dist x x_1 = dist x x_1
⊢ m.replaceBornology H = m

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
m : PseudoMetricSpace α
B : Bornology α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
x x_1 : α
⊢ dist x x_1 = dist x x_1

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α_1
α : Type u_3
B : Bornology α
m : PseudoMetricSpace α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
⊢ Eq.{u_3 + 1} (α := UniformSpace α) PseudoMetricSpace.toUniformSpace PseudoMetricSpace.toUniformSpace

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α_1 : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α_1
α : Type u_3
B : Bornology α
m : PseudoMetricSpace α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
⊢ Eq.{u_3 + 1} (α := UniformSpace α) PseudoMetricSpace.toUniformSpace PseudoMetricSpace.toUniformSpace

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
⊢ ∀ (x : ℝ), |x - x| = 0

Tactic:
simp [abs_zero]

Premises used: abs_zero
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
x y : ℝ
⊢ sorry = |x - y|

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
x y : ℝ
⊢ Eq (α := ℝ≥0) (sorry : ℝ≥0) ((nnabs : (a : ℝ) → ℝ≥0) (x - y) : ℝ≥0)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
x y : ℝ
⊢ Eq (α := ℝ≥0) (sorry : ℝ≥0) ((nnabs : (a : ℝ) → ℝ≥0) (y - x) : ℝ≥0)

Tactic:
nndist_comm _ _

Premises used: Unit.unit, sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, Function.const, Lean.Name, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
x y : ℝ
rw : x - y ≤ x - y ∨ x - y ≤ -(x - y)
x₁ y₁ : ℝ
⊢ x - y ≤ sorry

Tactic:
rw [Real.dist_eq, le_abs]

Premises used: le_abs, Real.dist_eq
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
x y : ℝ
⊢ x - y ≤ x - y ∨ x - y ≤ -(x - y)

Tactic:
Or.inl (le_refl _)

Premises used: le_refl, Or.inl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
x r : ℝ
h : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) sorry y ↔ y ∈ Icc (x - r) (x + r)
⊢ sorry = Icc (x - r) (x + r)

Tactic:
ext y
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
x y : ℝ
rw : Ioo x y = Ioo (HDiv.hDiv (α := ℝ) sorry 2) ((HDiv.hDiv (α := ℝ) sorry 2 - HDiv.hDiv (α := ℝ) sorry 2 + sorry) / 2)
b : ℝ
⊢ Ioo x y = sorry

Tactic:
rw [Real.ball_eq_Ioo, ← sub_div, add_comm, ← sub_add, add_sub_cancel_left, add_self_div_two,
    ← add_div, add_assoc, add_sub_cancel, add_self_div_two]

Premises used: sub_add, Real.ball_eq_Ioo, add_sub_cancel_left, add_assoc, sub_div, add_comm, add_sub_cancel, add_div, add_self_div_two
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
x y : ℝ
rw : Icc x y = Icc (HDiv.hDiv (α := ℝ) sorry 2) ((HDiv.hDiv (α := ℝ) sorry 2 - HDiv.hDiv (α := ℝ) sorry 2 + sorry) / 2)
b : ℝ
⊢ Icc x y = sorry

Tactic:
rw [Real.closedBall_eq_Icc, ← sub_div, add_comm, ← sub_add, add_sub_cancel_left, add_self_div_two,
    ← add_div, add_assoc, add_sub_cancel, add_self_div_two]

Premises used: sub_add, add_sub_cancel_left, Real.closedBall_eq_Icc, add_assoc, sub_div, add_comm, add_sub_cancel, add_div, add_self_div_two
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
ι : Type u_2
inst : PseudoMetricSpace α
f₁ f₂ : ι → α
p : Filter ι
a : α
h₁ : Tendsto f₁ p (𝓝 a)
h : Tendsto (β := ℝ) (fun (x : ι) ↦ dist (f₁ x) (f₂ x)) p (𝓝 0)
⊢ Tendsto f₂ p (𝓝 a)

Tactic:
h₁.congr_uniformity <| tendsto_uniformity_iff_dist_tendsto_zero.2 h

Premises used: Unit.unit, Filter.Tendsto.congr_uniformity, sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, Function.const, Lean.Name, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
ι : Type u_2
inst : PseudoMetricSpace α
f₁ f₂ : ι → α
p : Filter ι
a : α
h : Tendsto (β := ℝ) (fun (x : ι) ↦ dist (f₁ x) (f₂ x)) p (𝓝 0)
⊢ Tendsto f₁ p (𝓝 a) ↔ Tendsto f₂ p (𝓝 a)

Tactic:
Uniform.tendsto_congr <| tendsto_uniformity_iff_dist_tendsto_zero.2 h

Premises used: Unit.unit, sorryAx, Uniform.tendsto_congr, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, Function.const, Lean.Name, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : α
h : dist y z = 0
⊢ dist x y = dist x z

Tactic:
dist_comm y x ▸ dist_comm z x ▸ sub_eq_zero.1 (abs_nonpos_iff.1 (h ▸ abs_dist_sub_le y z x))

Premises used: sub_eq_zero, Eq.rec, PseudoMetricSpace.dist_comm, abs_nonpos_iff, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y z : α
⊢ sorry ≤ dist x y

Tactic:
abs_dist_sub_le ..

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

Tactic:
simpa only [dist_comm x] using dist_dist_dist_le_left y z x

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

Tactic:
(dist_triangle _ _ _).trans <|
    add_le_add (dist_dist_dist_le_left _ _ _) (dist_dist_dist_le_right _ _ _)

Premises used: dist_triangle, add_le_add, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
a : α
simp : comap (β := ℝ) (fun (x : α) ↦ dist a x) (𝓝 0) = comap (Prod.mk a) (𝓤 α)
⊢ comap (β := ℝ) (fun (x : α) ↦ dist x a) (𝓝 0) = 𝓝 a

Tactic:
simp only [@nhds_eq_comap_uniformity α, Metric.uniformity_eq_comap_nhds_zero, comap_comap,
    Function.comp_def, dist_comm]

Premises used: dist_comm, Function.comp_def, Filter.comap_comap, nhds_eq_comap_uniformity