awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p : α × α | dist p.1 p.2 < ε} ⊆ s
ε' : ℝ
hε' : 0 < ε' ∧ ε' < ε
⊢ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s
have mp : ∀ (i : β) (hi : p i) (H : f i ≤ ε'), ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s
Tactic: rcases hf ε' hε'.1 with ⟨i, hi, H⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
ι : Type u_2
inst : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : α × ι → Prop
⊢ (∀ᶠ (x : α × ι) in 𝓝 x₀ ×ˢ f, p x) ↔
    ∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i)
have refine : (∃ (i : ℝ × Set ι), (0 < i.1 ∧ i.2 ∈ f) ∧ ∀ ⦃x : α × ι⦄, x ∈ ball x₀ i.1 ×ˢ id i.2 → p x) ↔
  ∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i)
Tactic: refine (nhds_basis_ball.prod f.basis_sets).eventually_iff.trans ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
ι : Type u_2
inst : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∀ᶠ (x : ι × α) in f ×ˢ 𝓝 x₀, p x) ↔
    ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)
have rw : (∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap) ↔
  ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)
Tactic: rw [eventually_swap_iff, Metric.eventually_nhds_prod_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
ι : Type u_2
inst : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
⊢ (∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap) ↔
    ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)
have mp : (∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap) →
  ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
ι : Type u_2
inst : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
mp :
  (∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap) →
    ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)
⊢ (∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap) ↔
    ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)
have mpr : (∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)) →
  ∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
s : Set α
inst_1 : PseudoMetricSpace β
f : α → β
a : α
b : β
⊢ Tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) b < ε
have rw : (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → Membership.mem (γ := Set β) univ (f x) ∧ dist (f x) b < ε) ↔
  ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) b < ε
Tactic: rw [← nhdsWithin_univ b, tendsto_nhdsWithin_nhdsWithin]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
a : α
⊢ ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε
have rw : Tendsto f (𝓝 a) (𝓝 (f a)) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε
Tactic: rw [ContinuousAt, tendsto_nhds_nhds]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
a : α
rw : Tendsto f (𝓝 a) (𝓝 (f a)) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε
⊢ ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε
have rw₁ : (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε) ↔
  ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε
Tactic: rw [ContinuousAt, tendsto_nhds_nhds]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
a : α
s : Set α
⊢ ContinuousWithinAt f s a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) (f a) < ε
have rw : Tendsto f (𝓝[s] a) (𝓝 (f a)) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) (f a) < ε
Tactic: rw [ContinuousWithinAt, tendsto_nhdsWithin_nhds]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
a : α
s : Set α
rw : Tendsto f (𝓝[s] a) (𝓝 (f a)) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) (f a) < ε
⊢ ContinuousWithinAt f s a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) (f a) < ε
have rw₁ : (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) (f a) < ε) ↔
  ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) (f a) < ε
Tactic: rw [ContinuousWithinAt, tendsto_nhdsWithin_nhds]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε
have rw : Tendsto f (𝓝 b) (𝓝 (f b)) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε
Tactic: rw [ContinuousAt, tendsto_nhds]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
rw : Tendsto f (𝓝 b) (𝓝 (f b)) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε
⊢ ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε
have rw₁ : (∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε
Tactic: rw [ContinuousAt, tendsto_nhds]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
s : Set β
⊢ ContinuousWithinAt f s b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε
have rw : Tendsto f (𝓝[s] b) (𝓝 (f b)) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε
Tactic: rw [ContinuousWithinAt, tendsto_nhds]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
f : β → α
b : β
s : Set β
rw : Tendsto f (𝓝[s] b) (𝓝 (f b)) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε
⊢ ContinuousWithinAt f s b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε
have rw₁ : (∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε) ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε
Tactic: rw [ContinuousWithinAt, tendsto_nhds]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
hs : Dense s
x : α
ε : ℝ
hε : 0 < ε
⊢ ∃ y ∈ s, dist x y < ε
have this : (ball x ε).Nonempty
Tactic: have : (ball x ε).Nonempty := by simp [hε]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u_3
inst : PseudoMetricSpace α
r : ℝ
hpos : 0 < r
hr : Pairwise fun (x1 x2 : α) ↦ r ≤ dist x1 x2
⊢ Eq.{u_3 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace ⊥
have rw : Eq.{u_3 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace ⊥
Tactic: rw [Metric.uniformSpace_eq_bot.2 ⟨r, hpos, hr⟩, UniformSpace.toTopologicalSpace_bot]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u_3
inst : PseudoMetricSpace α
r : ℝ
hpos : 0 < r
hr : Pairwise fun (x1 x2 : α) ↦ r ≤ dist x1 x2
rw : Eq.{u_3 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace ⊥
⊢ Eq.{u_3 + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace ⊥
have rw₁ : Eq.{u_3 + 1} (α := TopologicalSpace α) ⊥ ⊥
Tactic: rw [Metric.uniformSpace_eq_bot.2 ⟨r, hpos, hr⟩, UniformSpace.toTopologicalSpace_bot]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u_3
d : α → α → ℝ≥0
⊢ Eq.{u_3 + 1} (α := Filter (α × α)) (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ) < ε})
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε})
have 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}
Tactic: simp only [le_antisymm_iff, le_iInf_iff, le_principal_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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}
have refine_1 : ∀ (ε : ℝ≥0∞) (hε : ε > 0),
  Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ) < ε})
    {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε}
Tactic: refine ⟨fun ε hε => ?_, fun ε hε => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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∞) < ε}
⊢ (∀ (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}
have refine_2 : ∀ (ε : ℝ) (hε : ε > 0),
  Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε})
    {p : α × α | (↑(d p.1 p.2) : ℝ) < ε}
Tactic: refine ⟨fun ε hε => ?_, fun ε hε => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0∞
hε : ε > 0
⊢ Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ) < ε})
    {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε}
have refine_1 : ∀ (ε' : ℝ≥0) (ε'0 : 0 < (↑ε' : ℝ≥0∞)) (ε'ε : (↑ε' : ℝ≥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, ε'ε⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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∞) < ε}
have refine_1 : Membership.mem (γ := Filter (α × α)) (𝓟 {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) ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ
hε : ε > 0
⊢ Membership.mem (γ := Filter (α × α)) (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < ε})
    {p : α × α | (↑(d p.1 p.2) : ℝ) < ε}
have refine_2 : ∀ (ε : ℝ≥0) (hε : (↑ε : ℝ) > 0),
  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ε
Cleared hypotheses: ε, hε
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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) : ℝ) < (↑ε : ℝ)}
have refine_2 : Membership.mem (γ := Filter (α × α)) (𝓟 {p : α × α | (↑(d p.1 p.2) : ℝ≥0∞) < (↑ε : ℝ≥0∞)})
  {p : α × α | (↑(d p.1 p.2) : ℝ) < (↑ε : ℝ)}
Tactic: refine mem_iInf_of_mem (ε : ℝ≥0∞) (mem_iInf_of_mem (ENNReal.coe_pos.2 hε) ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
x y z : α
⊢ edist x z ≤ edist x y + edist y z
have simp : ENNReal.ofReal (dist x z) ≤ ENNReal.ofReal (dist x y + dist y z)
Tactic: simp only [edist_dist, ← ENNReal.ofReal_add, dist_nonneg]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
x y z : α
⊢ ENNReal.ofReal (dist x z) ≤ ENNReal.ofReal (dist x y + dist y z)
have rw : dist x z ≤ dist x y + dist y z
Tactic: rw [ENNReal.ofReal_le_ofReal_iff _]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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
⊢ ENNReal.ofReal (dist x z) ≤ ENNReal.ofReal (dist x y + dist y z)
have rw₁ : 0 ≤ dist x y + dist y z
Tactic: rw [ENNReal.ofReal_le_ofReal_iff _]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ eball x (ENNReal.ofReal ε) = ball x ε
have h : ∀ (y : α), y ∈ eball x (ENNReal.ofReal ε) ↔ y ∈ ball x ε
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ y ∈ eball x (ENNReal.ofReal ε) ↔ y ∈ ball x ε
have h : ENNReal.ofReal (dist y x) < ENNReal.ofReal ε ↔ dist y x < ε
Tactic: simp only [mem_eball, mem_ball, edist_dist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ eball x (↑ε : ℝ≥0∞) = ball x (↑ε : ℝ)
have rw : eball x (↑ε : ℝ≥0∞) = eball x (ENNReal.ofReal (↑ε : ℝ))
Tactic: rw [← eball_ofReal]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 ≤ ε
⊢ closedEBall x (ENNReal.ofReal ε) = closedBall x ε
have h₁ : ∀ (y : α), y ∈ closedEBall x (ENNReal.ofReal ε) ↔ y ∈ closedBall x ε
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ closedEBall x (↑ε : ℝ≥0∞) = closedBall x (↑ε : ℝ)
have rw : closedEBall x (↑ε : ℝ≥0∞) = closedEBall x (ENNReal.ofReal (↑ε : ℝ))
Tactic: rw [← closedEBall_ofReal ε.coe_nonneg, ENNReal.ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ≥0
rw : closedEBall x (↑ε : ℝ≥0∞) = closedEBall x (ENNReal.ofReal (↑ε : ℝ))
⊢ closedEBall x (↑ε : ℝ≥0∞) = closedBall x (↑ε : ℝ)
have rw₁ : closedEBall x (↑ε : ℝ≥0∞) = closedEBall x (↑ε : ℝ≥0∞)
Tactic: rw [← closedEBall_ofReal ε.coe_nonneg, ENNReal.ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u_3
U : UniformSpace α
m : PseudoMetricSpace α
H : 𝓤 α = 𝓤 α
⊢ m.replaceUniformity H = m
have h : ∀ (x x_1 : α), dist x x_1 = dist x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
γ : Type u_3
U : TopologicalSpace γ
m : PseudoMetricSpace γ
H : U = UniformSpace.toTopologicalSpace
⊢ m.replaceTopology H = m
have h : ∀ (x x_1 : γ), dist x x_1 = dist x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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 α
⊢ Bornology.IsBounded s ↔ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C} sᶜ
have 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ᶜ
Tactic: rw [isBounded_iff, mem_setOf_eq, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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ᶜ
⊢ Bornology.IsBounded s ↔ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C} sᶜ
have rw₁ : (∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C) ↔ ∃ (C : ℝ), ∀ x ∈ sᶜᶜ, ∀ y ∈ sᶜᶜ, dist x y ≤ C
Tactic: rw [isBounded_iff, mem_setOf_eq, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
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
⊢ Bornology.IsBounded s ↔ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C} sᶜ
have rw₂ : (∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C) ↔ ∃ (C : ℝ), ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C
Tactic: rw [isBounded_iff, mem_setOf_eq, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u_3
m : PseudoMetricSpace α
B : Bornology α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
⊢ m.replaceBornology H = m
have h : ∀ (x x_1 : α), dist x x_1 = dist x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
x y : ℝ
⊢ x - y ≤ sorry
have rw : x - y ≤ x - y ∨ x - y ≤ -(x - y)
Tactic: rw [Real.dist_eq, le_abs]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
x r : ℝ
⊢ sorry = Icc (x - r) (x + r)
have h : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) sorry y ↔ y ∈ Icc (x - r) (x + r)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
x y : ℝ
⊢ Ioo x y = sorry
have rw : Ioo x y = Ioo (HDiv.hDiv (α := ℝ) sorry 2) ((HDiv.hDiv (α := ℝ) sorry 2 - HDiv.hDiv (α := ℝ) sorry 2 + sorry) / 2)
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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
x y : ℝ
⊢ Icc x y = sorry
have rw : Icc x y = Icc (HDiv.hDiv (α := ℝ) sorry 2) ((HDiv.hDiv (α := ℝ) sorry 2 - HDiv.hDiv (α := ℝ) sorry 2 + sorry) / 2)
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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
a : α
⊢ comap (β := ℝ) (fun (x : α) ↦ dist x a) (𝓝 0) = 𝓝 a
have simp : comap (β := ℝ) (fun (x : α) ↦ dist a x) (𝓝 0) = comap (Prod.mk a) (𝓤 α)
Tactic: simp only [@nhds_eq_comap_uniformity α, Metric.uniformity_eq_comap_nhds_zero, comap_comap,
    Function.comp_def, dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
⊢ Dense s ↔ ∀ r > 0, Eq.{u + 1} (α := Set α) (⋃ c ∈ s, ball c r) univ
have simp_rw : Dense s ↔ ∀ r > 0, ∀ (x : α), Membership.mem (γ := Set α) (⋃ c ∈ s, ball c r) x
Tactic: simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop, mem_ball, Dense, mem_closure_iff,
    forall_comm (α := α)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
simp_rw : Dense s ↔ ∀ r > 0, ∀ (x : α), Membership.mem (γ := Set α) (⋃ c ∈ s, ball c r) x
⊢ Dense s ↔ ∀ r > 0, Eq.{u + 1} (α := Set α) (⋃ c ∈ s, ball c r) univ
have simp_rw₁ : Dense s ↔ ∀ r > 0, ∀ (x : α), ∃ (i : α) (_ : i ∈ s), x ∈ ball i r
Tactic: simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop, mem_ball, Dense, mem_closure_iff,
    forall_comm (α := α)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
simp_rw : Dense s ↔ ∀ r > 0, ∀ (x : α), Membership.mem (γ := Set α) (⋃ c ∈ s, ball c r) x
simp_rw₁ : Dense s ↔ ∀ r > 0, ∀ (x : α), ∃ (i : α) (_ : i ∈ s), x ∈ ball i r
⊢ Dense s ↔ ∀ r > 0, Eq.{u + 1} (α := Set α) (⋃ c ∈ s, ball c r) univ
have simp_rw₂ : Dense s ↔ ∀ r > 0, ∀ (x : α), ∃ i ∈ s, x ∈ ball i r
Tactic: simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop, mem_ball, Dense, mem_closure_iff,
    forall_comm (α := α)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
simp_rw : Dense s ↔ ∀ r > 0, ∀ (x : α), Membership.mem (γ := Set α) (⋃ c ∈ s, ball c r) x
simp_rw₁ : Dense s ↔ ∀ r > 0, ∀ (x : α), ∃ (i : α) (_ : i ∈ s), x ∈ ball i r
simp_rw₂ : Dense s ↔ ∀ r > 0, ∀ (x : α), ∃ i ∈ s, x ∈ ball i r
⊢ Dense s ↔ ∀ r > 0, Eq.{u + 1} (α := Set α) (⋃ c ∈ s, ball c r) univ
have simp_rw₃ : Dense s ↔ ∀ r > 0, ∀ (x : α), ∃ i ∈ s, dist x i < r
Tactic: simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop, mem_ball, Dense, mem_closure_iff,
    forall_comm (α := α)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
simp_rw : Dense s ↔ ∀ r > 0, ∀ (x : α), Membership.mem (γ := Set α) (⋃ c ∈ s, ball c r) x
simp_rw₁ : Dense s ↔ ∀ r > 0, ∀ (x : α), ∃ (i : α) (_ : i ∈ s), x ∈ ball i r
simp_rw₂ : Dense s ↔ ∀ r > 0, ∀ (x : α), ∃ i ∈ s, x ∈ ball i r
simp_rw₃ : Dense s ↔ ∀ r > 0, ∀ (x : α), ∃ i ∈ s, dist x i < r
⊢ Dense s ↔ ∀ r > 0, Eq.{u + 1} (α := Set α) (⋃ c ∈ s, ball c r) univ
have simp_rw₄ : (∀ (x : α), x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ↔
  ∀ r > 0, ∀ (x : α), ∃ i ∈ s, dist x i < r
Tactic: simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop, mem_ball, Dense, mem_closure_iff,
    forall_comm (α := α)]