awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
r : ℝ
hr : 0 ≤ 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_le_ofReal_iff hr]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
r : ℝ
hr : 0 ≤ 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_le_ofReal_iff hr]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ nndist x y = (dist x y).toNNReal
have rw : nndist x y = (↑(nndist x y) : ℝ).toNNReal
Tactic: rw [dist_nndist, Real.toNNReal_coe]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
rw : nndist x y = (↑(nndist x y) : ℝ).toNNReal
⊢ nndist x y = (dist x y).toNNReal
have rw₁ : nndist x y = nndist x y
Tactic: rw [dist_nndist, Real.toNNReal_coe]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ dist x y = (edist x y).toReal
have rw : dist x y = (ENNReal.ofReal (dist x y)).toReal
Tactic: rw [edist_dist, ENNReal.toReal_ofReal dist_nonneg]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
rw : dist x y = (ENNReal.ofReal (dist x y)).toReal
⊢ dist x y = (edist x y).toReal
have rw₁ : dist x y = dist x y
Tactic: rw [edist_dist, ENNReal.toReal_ofReal dist_nonneg]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ y ∈ ball x ε ↔ dist x y < ε
have rw : y ∈ ball x ε ↔ dist y x < ε
Tactic: rw [dist_comm, mem_ball]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
rw : y ∈ ball x ε ↔ dist y x < ε
⊢ y ∈ ball x ε ↔ dist x y < ε
have rw₁ : dist y x < ε ↔ dist y x < ε
Tactic: rw [dist_comm, mem_ball]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 < ε
⊢ x ∈ ball x ε
have rwa : dist x x < ε
Tactic: rwa [mem_ball, dist_self]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ ball x ε = ∅ ↔ ε ≤ 0
have rw : ¬(ball x ε).Nonempty ↔ ε ≤ 0
Tactic: rw [← not_nonempty_iff_eq_empty, nonempty_ball, not_lt]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
rw : ¬(ball x ε).Nonempty ↔ ε ≤ 0
⊢ ball x ε = ∅ ↔ ε ≤ 0
have rw₁ : ¬0 < ε ↔ ε ≤ 0
Tactic: rw [← not_nonempty_iff_eq_empty, nonempty_ball, not_lt]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
rw : ¬(ball x ε).Nonempty ↔ ε ≤ 0
rw₁ : ¬0 < ε ↔ ε ≤ 0
⊢ ball x ε = ∅ ↔ ε ≤ 0
have rw₂ : ε ≤ 0 ↔ ε ≤ 0
Tactic: rw [← not_nonempty_iff_eq_empty, nonempty_ball, not_lt]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ ball x 0 = ∅
have rw : LE.le (α := ℝ) 0 0
Tactic: rw [ball_eq_empty]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
ε : ℝ
x : α
⊢ UniformSpace.ball x {p : α × α | dist p.1 p.2 < ε} = ball x ε
have h : ∀ (x_1 : α), x_1 ∈ UniformSpace.ball x {p : α × α | dist p.1 p.2 < ε} ↔ x_1 ∈ ball x ε
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ y ∈ closedBall x ε ↔ dist x y ≤ ε
have rw : y ∈ closedBall x ε ↔ dist y x ≤ ε
Tactic: rw [dist_comm, mem_closedBall]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
rw : y ∈ closedBall x ε ↔ dist y x ≤ ε
⊢ y ∈ closedBall x ε ↔ dist x y ≤ ε
have rw₁ : dist y x ≤ ε ↔ dist y x ≤ ε
Tactic: rw [dist_comm, mem_closedBall]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ y ∈ sphere x ε ↔ dist x y = ε
have rw : y ∈ sphere x ε ↔ dist y x = ε
Tactic: rw [dist_comm, mem_sphere]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
rw : y ∈ sphere x ε ↔ dist y x = ε
⊢ y ∈ sphere x ε ↔ dist x y = ε
have rw₁ : dist y x = ε ↔ dist y x = ε
Tactic: rw [dist_comm, mem_sphere]
-- 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 : α
δ ε ε₁ ε₂ : ℝ
s : Set α
inst_1 : Subsingleton α
inst_2 : NeZero ε
⊢ IsEmpty.{u + 1} (↑(sphere x ε) : Type u)
have rw : IsEmpty.{u + 1} (↑∅ : Type u)
Tactic: rw [sphere_eq_empty_of_subsingleton (NeZero.ne ε)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
inst_1 : Subsingleton α
h : 0 ≤ ε
⊢ closedBall x ε = {x}
have h₁ : ∀ (x' : α), x' ∈ closedBall x ε ↔ Membership.mem (γ := Set α) {x} x'
Tactic: ext x'
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
inst_1 : Subsingleton α
h : 0 < ε
⊢ ball x ε = {x}
have h₁ : ∀ (x' : α), x' ∈ ball x ε ↔ Membership.mem (γ := Set α) {x} x'
Tactic: ext x'
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 ≤ ε
⊢ x ∈ closedBall x ε
have rwa : dist x x ≤ ε
Tactic: rwa [mem_closedBall, dist_self]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ closedBall x ε = ∅ ↔ ε < 0
have rw : ¬(closedBall x ε).Nonempty ↔ ε < 0
Tactic: rw [← not_nonempty_iff_eq_empty, nonempty_closedBall, not_le]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
rw : ¬(closedBall x ε).Nonempty ↔ ε < 0
⊢ closedBall x ε = ∅ ↔ ε < 0
have rw₁ : ¬0 ≤ ε ↔ ε < 0
Tactic: rw [← not_nonempty_iff_eq_empty, nonempty_closedBall, not_le]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
rw : ¬(closedBall x ε).Nonempty ↔ ε < 0
rw₁ : ¬0 ≤ ε ↔ ε < 0
⊢ closedBall x ε = ∅ ↔ ε < 0
have rw₂ : ε < 0 ↔ ε < 0
Tactic: rw [← not_nonempty_iff_eq_empty, nonempty_closedBall, not_le]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
δ ε : ℝ
h : δ + ε ≤ dist x y
⊢ ε + δ ≤ dist y x
have rwa : δ + ε ≤ dist y x
Tactic: rwa [add_comm, dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ sphere x ε ∪ ball x ε = closedBall x ε
have rw : ball x ε ∪ sphere x ε = closedBall x ε
Tactic: rw [union_comm, ball_union_sphere]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
rw : ball x ε ∪ sphere x ε = closedBall x ε
⊢ sphere x ε ∪ ball x ε = closedBall x ε
have rw₁ : closedBall x ε = closedBall x ε
Tactic: rw [union_comm, ball_union_sphere]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ closedBall x ε \ sphere x ε = ball x ε
have rw : (ball x ε ∪ sphere x ε) \ sphere x ε = ball x ε
Tactic: rw [← ball_union_sphere, Set.union_diff_cancel_right sphere_disjoint_ball.symm.le_bot]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
rw : (ball x ε ∪ sphere x ε) \ sphere x ε = ball x ε
⊢ closedBall x ε \ sphere x ε = ball x ε
have rw₁ : ball x ε = ball x ε
Tactic: rw [← ball_union_sphere, Set.union_diff_cancel_right sphere_disjoint_ball.symm.le_bot]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ closedBall x ε \ ball x ε = sphere x ε
have rw : (ball x ε ∪ sphere x ε) \ ball x ε = sphere x ε
Tactic: rw [← ball_union_sphere, Set.union_diff_cancel_left sphere_disjoint_ball.symm.le_bot]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
rw : (ball x ε ∪ sphere x ε) \ ball x ε = sphere x ε
⊢ closedBall x ε \ ball x ε = sphere x ε
have rw₁ : sphere x ε = sphere x ε
Tactic: rw [← ball_union_sphere, Set.union_diff_cancel_left sphere_disjoint_ball.symm.le_bot]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ x ∈ ball y ε ↔ y ∈ ball x ε
have rw : dist y x < ε ↔ y ∈ ball x ε
Tactic: rw [mem_ball', mem_ball]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
rw : dist y x < ε ↔ y ∈ ball x ε
⊢ x ∈ ball y ε ↔ y ∈ ball x ε
have rw₁ : dist y x < ε ↔ dist y x < ε
Tactic: rw [mem_ball', mem_ball]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ x ∈ closedBall y ε ↔ y ∈ closedBall x ε
have rw : dist y x ≤ ε ↔ y ∈ closedBall x ε
Tactic: rw [mem_closedBall', mem_closedBall]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
rw : dist y x ≤ ε ↔ y ∈ closedBall x ε
⊢ x ∈ closedBall y ε ↔ y ∈ closedBall x ε
have rw₁ : dist y x ≤ ε ↔ dist y x ≤ ε
Tactic: rw [mem_closedBall', mem_closedBall]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ x ∈ sphere y ε ↔ y ∈ sphere x ε
have rw : dist y x = ε ↔ y ∈ sphere x ε
Tactic: rw [mem_sphere', mem_sphere]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
rw : dist y x = ε ↔ y ∈ sphere x ε
⊢ x ∈ sphere y ε ↔ y ∈ sphere x ε
have rw₁ : dist y x = ε ↔ dist y x = ε
Tactic: rw [mem_sphere', mem_sphere]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ closedBall x ε = ⋂ (δ : ℝ), ⋂ (_ : δ > ε), ball x δ
have h : ∀ (y : α), y ∈ closedBall x ε ↔ Membership.mem (γ := Set α) (⋂ (δ : ℝ), ⋂ (_ : δ > ε), ball x δ) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ y ∈ closedBall x ε ↔ Membership.mem (γ := Set α) (⋂ (δ : ℝ), ⋂ (_ : δ > ε), ball x δ) y
have h : (∀ ⦃c : ℝ⦄, ε < c → dist y x < c) ↔ ∀ (i : ℝ) (j : i > ε), y ∈ ball x i
Tactic: rw [mem_closedBall, ← forall_gt_iff_le, mem_iInter₂]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y ≤ ε₂
z : α
hz : z ∈ ball x ε₁
⊢ dist z x + dist x y < ε₁ + dist x y
have bc : dist z x < ε₁
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y ≤ ε₂
z : α
hz : z ∈ closedBall x ε₁
⊢ dist z x + dist x y ≤ ε₁ + dist x y
have bc : dist z x ≤ ε₁
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y < ε₂
z : α
hz : z ∈ closedBall x ε₁
⊢ dist z x + dist x y ≤ ε₁ + dist x y
have bc : dist z x ≤ ε₁
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (ball x ε₁ ∩ closedBall y ε₂).Nonempty
⊢ dist x y < ε₁ + ε₂
have h₁ : (closedBall y ε₂ ∩ ball x ε₁).Nonempty
Tactic: rw [inter_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (closedBall y ε₂ ∩ ball x ε₁).Nonempty
⊢ dist x y < ε₁ + ε₂
have rw : dist y x < ε₂ + ε₁
Tactic: rw [add_comm, dist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
⊢ ⋃ (n : ℕ), s ∩ closedBall x (↑n : ℝ) = s
have rw : s ∩ ⋃ (i : ℕ), closedBall x (↑i : ℝ) = s
Tactic: rw [← inter_iUnion, iUnion_closedBall_nat, inter_univ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
rw : s ∩ ⋃ (i : ℕ), closedBall x (↑i : ℝ) = s
⊢ ⋃ (n : ℕ), s ∩ closedBall x (↑n : ℝ) = s
have rw₁ : s ∩ univ = s
Tactic: rw [← inter_iUnion, iUnion_closedBall_nat, inter_univ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
x : α
rw : s ∩ ⋃ (i : ℕ), closedBall x (↑i : ℝ) = s
rw₁ : s ∩ univ = s
⊢ ⋃ (n : ℕ), s ∩ closedBall x (↑n : ℝ) = s
have rw₂ : s = s
Tactic: rw [← inter_iUnion, iUnion_closedBall_nat, inter_univ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : dist x y ≤ ε₂ - ε₁
z : α
zx : z ∈ ball x ε₁
⊢ z ∈ ball y ε₂
have rw : z ∈ ball y (ε₁ + (ε₂ - ε₁))
Tactic: rw [← add_sub_cancel ε₁ ε₂]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
y : α
h : y ∈ ball x (ε / 2)
⊢ dist y x ≤ ε - ε / 2
have rw : dist y x ≤ ε / 2
Tactic: rw [sub_self_div_two]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
h : y ∈ ball x ε
⊢ dist y x ≤ ε - (ε - dist y x)
have rw : dist y x ≤ dist y x
Tactic: rw [sub_sub_self]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall x R, p y
y : α
⊢ p y
have obtain : ∀ (R : ℝ) (hR : R ≥ dist y x) (h : ∀ z ∈ closedBall x R, p z), p y
Tactic: obtain ⟨R, hR, h⟩ : ∃ R ≥ dist y x, ∀ z : α, z ∈ closedBall x R → p z :=
    frequently_iff.1 H (Ici_mem_atTop (dist y x))
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ ball x R, p y
y : α
⊢ p y
have obtain : ∀ (R : ℝ) (hR : R > dist y x) (h : ∀ z ∈ ball x R, p z), p y
Tactic: obtain ⟨R, hR, h⟩ : ∃ R > dist y x, ∀ z : α, z ∈ ball x R → p z :=
    frequently_iff.1 H (Ioi_mem_atTop (dist y x))
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
⊢ Bornology.IsBounded s ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
have rw : sᶜ ∈ cobounded α ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
Tactic: rw [isBounded_def, ← Filter.mem_sets, @PseudoMetricSpace.cobounded_sets α, mem_setOf_eq,
    compl_compl]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
rw : sᶜ ∈ cobounded α ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
⊢ Bornology.IsBounded s ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
have rw₁ : sᶜ ∈ (cobounded α).sets ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
Tactic: rw [isBounded_def, ← Filter.mem_sets, @PseudoMetricSpace.cobounded_sets α, mem_setOf_eq,
    compl_compl]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
rw : sᶜ ∈ cobounded α ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
rw₁ : sᶜ ∈ (cobounded α).sets ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
⊢ Bornology.IsBounded s ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
have rw₂ : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C} sᶜ ↔
  ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
Tactic: rw [isBounded_def, ← Filter.mem_sets, @PseudoMetricSpace.cobounded_sets α, mem_setOf_eq,
    compl_compl]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
rw : sᶜ ∈ cobounded α ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
rw₁ : sᶜ ∈ (cobounded α).sets ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
rw₂ :
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C} sᶜ ↔
    ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
⊢ Bornology.IsBounded s ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
have rw₃ : (∃ (C : ℝ), ∀ x ∈ sᶜᶜ, ∀ y ∈ sᶜᶜ, dist x y ≤ C) ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
Tactic: rw [isBounded_def, ← Filter.mem_sets, @PseudoMetricSpace.cobounded_sets α, mem_setOf_eq,
    compl_compl]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
rw : sᶜ ∈ cobounded α ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
rw₁ : sᶜ ∈ (cobounded α).sets ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
rw₂ :
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C} sᶜ ↔
    ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
rw₃ : (∃ (C : ℝ), ∀ x ∈ sᶜᶜ, ∀ y ∈ sᶜᶜ, dist x y ≤ C) ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
⊢ Bornology.IsBounded s ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
have rw₄ : (∃ (C : ℝ), ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ C) ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
Tactic: rw [isBounded_def, ← Filter.mem_sets, @PseudoMetricSpace.cobounded_sets α, mem_setOf_eq,
    compl_compl]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ BoundedSpace α ↔ ∃ (C : ℝ), ∀ (a b : α), dist a b ≤ C
have rw : (∃ (C : ℝ),
    ∀ ⦃x : α⦄, Membership.mem (γ := Set α) univ x → ∀ ⦃y : α⦄, Membership.mem (γ := Set α) univ y → dist x y ≤ C) ↔
  ∃ (C : ℝ), ∀ (a b : α), dist a b ≤ C
Tactic: rw [← isBounded_univ, Metric.isBounded_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ BoundedSpace α ↔ ∃ (C : ℝ≥0), ∀ (a b : α), nndist a b ≤ C
have rw : (∃ (C : ℝ≥0),
    ∀ ⦃x : α⦄, Membership.mem (γ := Set α) univ x → ∀ ⦃y : α⦄, Membership.mem (γ := Set α) univ y → nndist x y ≤ C) ↔
  ∃ (C : ℝ≥0), ∀ (a b : α), nndist a b ≤ C
Tactic: rw [← isBounded_univ, Metric.isBounded_iff_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ (𝓤 α).HasBasis (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {p : α × α | dist p.1 p.2 < ε}
have rw : (𝓤 α).HasBasis (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦ {p : α × α | dist p.1 p.2 < ε}
Tactic: rw [toUniformSpace_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ (i : β), p i ∧ f i ≤ ε
⊢ (𝓤 α).HasBasis p fun (i : β) ↦ {p : α × α | dist p.1 p.2 < f i}
have refine : ∀ (s : Set (α × α)),
  (∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 < f i} ⊆ s
Tactic: refine ⟨fun s => uniformity_basis_dist.mem_iff.trans ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ (i : β), p i ∧ f i ≤ ε
s : Set (α × α)
⊢ (∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 < f i} ⊆ s
have mp : (∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s) → ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 < f i} ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ (i : β), p i ∧ f i ≤ ε
s : Set (α × α)
mp : (∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s) → ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 < f i} ⊆ s
⊢ (∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 < f i} ⊆ s
have mpr : (∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 < f i} ⊆ s) → ∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
β : Type u_3
p : β → Prop
f : β → ℝ
hf₀ : ∀ (i : β), p i → 0 < f i
hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ (i : β), p i ∧ f i ≤ ε
s : Set (α × α)
ε : ℝ
ε₀ : 0 < ε
hε : {p : α × α | dist p.1 p.2 < ε} ⊆ s
⊢ ∃ (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 ε₀ with ⟨i, hi, H⟩
-- 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 ≤ ε
⊢ (𝓤 α).HasBasis p fun (x : β) ↦ {p : α × α | dist p.1 p.2 ≤ f x}
have refine : ∀ (s : Set (α × α)),
  (∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s
Tactic: refine ⟨fun s => uniformity_basis_dist.mem_iff.trans ?_⟩
-- 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 (α × α)
⊢ (∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s
have mp : (∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s) → ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s
Tactic: constructor
-- 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 (α × α)
mp : (∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s) → ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s
⊢ (∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s) ↔ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s
have mpr : (∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s) → ∃ (i : ℝ), 0 < i ∧ {p : α × α | dist p.1 p.2 < i} ⊆ s
Tactic: constructor
-- 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
⊢ ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s
have mp : ∀ (ε' : ℝ) (hε' : 0 < ε' ∧ ε' < ε), ∃ (i : β), p i ∧ {p : α × α | dist p.1 p.2 ≤ f i} ⊆ s
Tactic: rcases exists_between ε₀ with ⟨ε', hε'⟩