awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ (↑(nndist x y) : ℝ) = dist x y

Tactic:
rfl

Premises used: NNReal.toReal, rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
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∞)
rw₂ rw₃ : (↑(nndist x y) : ℝ≥0∞) = (↑(nndist x y) : ℝ≥0∞)
⊢ edist x y = (↑(nndist x y) : ℝ≥0∞)

Tactic:
rw [edist_dist, dist_nndist, ENNReal.ofReal_coe_nnreal]

Premises used: dist_nndist, edist_dist, ENNReal.ofReal_coe_nnreal
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ nndist x y = (edist x y).toNNReal

Tactic:
simp [edist_nndist]

Premises used: edist_nndist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ (↑(nndist x y) : ℝ≥0∞) = edist x y

Tactic:
(edist_nndist x y).symm

Premises used: edist_nndist, Eq.symm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
c : ℝ≥0
rw : (↑(nndist x y) : ℝ≥0∞) < (↑c : ℝ≥0∞) ↔ nndist x y < c
rw₁ rw₂ : nndist x y < c ↔ nndist x y < c
⊢ edist x y < (↑c : ℝ≥0∞) ↔ nndist x y < c

Tactic:
rw [edist_nndist, ENNReal.coe_lt_coe]

Premises used: ENNReal.coe_lt_coe, edist_nndist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
c : ℝ≥0
rw : (↑(nndist x y) : ℝ≥0∞) ≤ (↑c : ℝ≥0∞) ↔ nndist x y ≤ c
rw₁ rw₂ : nndist x y ≤ c ↔ nndist x y ≤ c
⊢ edist x y ≤ (↑c : ℝ≥0∞) ↔ nndist x y ≤ c

Tactic:
rw [edist_nndist, ENNReal.coe_le_coe]

Premises used: ENNReal.coe_le_coe, edist_nndist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u_3
inst : PseudoMetricSpace α
x y : α
⊢ edist x y < ∞

Tactic:
(edist_dist x y).symm ▸ ENNReal.ofReal_lt_top

Premises used: ENNReal.ofReal_lt_top, Eq.rec, edist_dist, Eq.symm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ edist x y ≠ ∞

Tactic:
(edist_lt_top x y).ne

Premises used: edist_lt_top, LT.lt.ne
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
a : α
⊢ nndist a a = 0

Tactic:
NNReal.coe_eq_zero.1 (dist_self a)

Premises used: NNReal.coe_eq_zero, dist_self, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
c : ℝ≥0
⊢ dist x y < (↑c : ℝ) ↔ nndist x y < c

Tactic:
Iff.rfl

Premises used: Iff.rfl, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
c : ℝ≥0
⊢ dist x y ≤ (↑c : ℝ) ↔ nndist x y ≤ c

Tactic:
Iff.rfl

Premises used: Iff.rfl, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
r : ℝ
rw : ENNReal.ofReal (dist x y) < ENNReal.ofReal r ↔ dist x y < r
rw₁ rw₂ : dist x y < r ↔ dist x y < r
⊢ edist x y < ENNReal.ofReal r ↔ dist x y < r

Tactic:
rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff_of_nonneg dist_nonneg]

Premises used: ENNReal.ofReal_lt_ofReal_iff_of_nonneg, dist_nonneg, edist_dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
r : ℝ
hr : 0 ≤ r
rw : ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal r ↔ dist x y ≤ r
rw₁ rw₂ : dist x y ≤ r ↔ dist x y ≤ r
⊢ edist x y ≤ ENNReal.ofReal r ↔ dist x y ≤ r

Tactic:
rw [edist_dist, ENNReal.ofReal_le_ofReal_iff hr]

Premises used: ENNReal.ofReal_le_ofReal_iff, edist_dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
rw : nndist x y = (↑(nndist x y) : ℝ).toNNReal
rw₁ rw₂ : nndist x y = nndist x y
⊢ nndist x y = (dist x y).toNNReal

Tactic:
rw [dist_nndist, Real.toNNReal_coe]

Premises used: dist_nndist, Real.toNNReal_coe
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ nndist x y = nndist y x

Tactic:
NNReal.eq <| dist_comm x y

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

Tactic:
dist_triangle _ _ _

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

Tactic:
dist_triangle_left _ _ _

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

Tactic:
dist_triangle_right _ _ _

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

Tactic:
rw [edist_dist, ENNReal.toReal_ofReal dist_nonneg]

Premises used: dist_nonneg, ENNReal.toReal_ofReal, edist_dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ y ∈ ball x ε ↔ dist y x < ε

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, Metric.ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
rw : y ∈ ball x ε ↔ dist y x < ε
rw₁ rw₂ : dist y x < ε ↔ dist y x < ε
⊢ y ∈ ball x ε ↔ dist x y < ε

Tactic:
rw [dist_comm, mem_ball]

Premises used: dist_comm, Metric.mem_ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
hy : y ∈ ball x ε
⊢ 0 < ε

Tactic:
dist_nonneg.trans_lt hy

Premises used: dist_nonneg, LE.le.trans_lt
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 < ε
rwa : dist x x < ε
rwa₁ rwa₂ rwa₃ rwa₄ : 0 < ε
⊢ x ∈ ball x ε

Tactic:
rwa [mem_ball, dist_self]

Premises used: Metric.mem_ball, dist_self
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ (ball x ε).Nonempty ↔ 0 < ε

Tactic:
⟨fun ⟨_x, hx⟩ => pos_of_mem_ball hx, fun h => ⟨x, mem_ball_self h⟩⟩

Premises used: Metric.mem_ball_self, LT.lt, Iff.intro, Exists.intro, _private.0.Metric.nonempty_ball.match_1, Metric.pos_of_mem_ball, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
rw : ¬(ball x ε).Nonempty ↔ ε ≤ 0
rw₁ : ¬0 < ε ↔ ε ≤ 0
rw₂ rw₃ : ε ≤ 0 ↔ ε ≤ 0
⊢ ball x ε = ∅ ↔ ε ≤ 0

Tactic:
rw [← not_nonempty_iff_eq_empty, nonempty_ball, not_lt]

Premises used: Set.not_nonempty_iff_eq_empty, Metric.nonempty_ball, not_lt
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
rw rw₁ : LE.le (α := ℝ) 0 0
⊢ ball x 0 = ∅

Tactic:
rw [ball_eq_empty]

Premises used: Metric.ball_eq_empty
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
h : x ∈ ball y ε
⊢ ∃ ε' < ε, x ∈ ball y ε'

Tactic:
simpa [mem_ball] using exists_between' h

Premises used: exists_between', Metric.mem_ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
ε : ℝ
x : α
⊢ UniformSpace.ball x {p : α × α | dist p.2 p.1 < ε} = ball x ε

Tactic:
rfl

Premises used: Set.Mem, setOf, Metric.ball, UniformSpace.ball, Set.preimage, rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
ε : ℝ
x : α
h : ∀ (x_1 : α), x_1 ∈ UniformSpace.ball x {p : α × α | dist p.1 p.2 < ε} ↔ x_1 ∈ ball x ε
⊢ UniformSpace.ball x {p : α × α | dist p.1 p.2 < ε} = ball x ε

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
ε : ℝ
x x_1 : α
⊢ x_1 ∈ UniformSpace.ball x {p : α × α | dist p.1 p.2 < ε} ↔ x_1 ∈ ball x ε

Tactic:
simp [dist_comm, UniformSpace.ball]

Premises used: dist_comm, UniformSpace.ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ Eq.{u + 1} (α := Set α) (⋃ (n : ℕ), ball x (↑n : ℝ)) univ

Tactic:
iUnion_eq_univ_iff.2 fun y => exists_nat_gt (dist y x)

Premises used: Iff.mpr, Set.iUnion_eq_univ_iff, Dist.dist, exists_nat_gt
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ Eq.{u + 1} (α := Set α) (⋃ (n : ℕ), ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) univ

Tactic:
iUnion_eq_univ_iff.2 fun y => (exists_nat_gt (dist y x)).imp fun _ h => h.trans (lt_add_one _)

Premises used: Iff.mpr, Set.iUnion_eq_univ_iff, Exists.imp, Dist.dist, exists_nat_gt
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ y ∈ closedBall x ε ↔ dist y x ≤ ε

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, Metric.closedBall
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
rw : y ∈ closedBall x ε ↔ dist y x ≤ ε
rw₁ rw₂ : dist y x ≤ ε ↔ dist y x ≤ ε
⊢ y ∈ closedBall x ε ↔ dist x y ≤ ε

Tactic:
rw [dist_comm, mem_closedBall]

Premises used: dist_comm, Metric.mem_closedBall
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ y ∈ sphere x ε ↔ dist y x = ε

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Metric.sphere
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
rw : y ∈ sphere x ε ↔ dist y x = ε
rw₁ rw₂ : dist y x = ε ↔ dist y x = ε
⊢ y ∈ sphere x ε ↔ dist x y = ε

Tactic:
rw [dist_comm, mem_sphere]

Premises used: dist_comm, Metric.mem_sphere
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
h : y ∈ sphere x ε
hε : ε ≠ 0
⊢ x ∉ sphere x ε

Tactic:
simpa using hε.symm

Premises used: Ne.symm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
hy : y ∈ sphere x ε
⊢ 0 ≤ ε

Tactic:
dist_nonneg.trans_eq hy

Premises used: LE.le.trans_eq, dist_nonneg
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
hε : ε < 0
⊢ sphere x ε = ∅

Tactic:
Set.eq_empty_iff_forall_notMem.mpr fun _y hy => (nonneg_of_mem_sphere hy).not_gt hε

Premises used: Iff.mpr, Metric.nonneg_of_mem_sphere, LE.le.not_gt, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
inst_1 : Subsingleton α
hε : ε ≠ 0
⊢ sphere x ε = ∅

Tactic:
Set.eq_empty_iff_forall_notMem.mpr fun _ h => ne_of_mem_sphere h hε (Subsingleton.elim _ _)

Premises used: Iff.mpr, Metric.ne_of_mem_sphere, Set.eq_empty_iff_forall_notMem, Subsingleton.elim
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
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 ε
rw : IsEmpty.{u + 1} (↑∅ : Type u)
⊢ IsEmpty.{u + 1} (↑(sphere x ε) : Type u)

Tactic:
rw [sphere_eq_empty_of_subsingleton (NeZero.ne ε)]

Premises used: Metric.sphere_eq_empty_of_subsingleton, NeZero.ne
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
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} (↑∅ : Type u)

Tactic:
infer_instance
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
inst_1 : Subsingleton α
h : 0 ≤ ε
h₁ : ∀ (x' : α), x' ∈ closedBall x ε ↔ Membership.mem (γ := Set α) {x} x'
⊢ closedBall x ε = {x}

Tactic:
ext x'
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
inst_1 : Subsingleton α
h : 0 ≤ ε
x' : α
⊢ x' ∈ closedBall x ε ↔ Membership.mem (γ := Set α) {x} x'

Tactic:
simpa [Subsingleton.allEq x x']

Premises used: Subsingleton.allEq
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
inst_1 : Subsingleton α
h : 0 < ε
h₁ : ∀ (x' : α), x' ∈ ball x ε ↔ Membership.mem (γ := Set α) {x} x'
⊢ ball x ε = {x}

Tactic:
ext x'
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
inst_1 : Subsingleton α
h : 0 < ε
x' : α
⊢ x' ∈ ball x ε ↔ Membership.mem (γ := Set α) {x} x'

Tactic:
simpa [Subsingleton.allEq x x']

Premises used: Subsingleton.allEq
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 ≤ ε
rwa : dist x x ≤ ε
rwa₁ rwa₂ rwa₃ rwa₄ : 0 ≤ ε
⊢ x ∈ closedBall x ε

Tactic:
rwa [mem_closedBall, dist_self]

Premises used: dist_self, Metric.mem_closedBall
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ (closedBall x ε).Nonempty ↔ 0 ≤ ε

Tactic:
⟨fun ⟨_x, hx⟩ => dist_nonneg.trans hx, fun h => ⟨x, mem_closedBall_self h⟩⟩

Premises used: dist_nonneg, LE.le, Iff.intro, Exists.intro, LE.le.trans, OfNat.ofNat, Metric.mem_closedBall_self, _private.0.Metric.nonempty_closedBall.match_1
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
rw : ¬(closedBall x ε).Nonempty ↔ ε < 0
rw₁ : ¬0 ≤ ε ↔ ε < 0
rw₂ rw₃ : ε < 0 ↔ ε < 0
⊢ closedBall x ε = ∅ ↔ ε < 0

Tactic:
rw [← not_nonempty_iff_eq_empty, nonempty_closedBall, not_le]

Premises used: not_le, Set.not_nonempty_iff_eq_empty, Metric.nonempty_closedBall
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
hε : ε ≤ 0
⊢ closedBall x ε = sphere x ε

Tactic:
Set.ext fun _ => (hε.trans dist_nonneg).ge_iff_eq'

Premises used: Set.ext, dist_nonneg, LE.le.ge_iff_eq', LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ ball x ε ⊆ closedBall x ε

Tactic:
fun _y hy =>
  mem_closedBall.2 (le_of_lt hy)

Premises used: Iff.mpr, le_of_lt, Set.Subset, Metric.mem_closedBall
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ sphere x ε ⊆ closedBall x ε

Tactic:
fun _ => le_of_eq

Premises used: Set.Mem, setOf, Set.Subset, Metric.closedBall, le_of_eq, Metric.sphere
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
r R : ℝ
h : r < R
⊢ sphere x r ⊆ ball x R

Tactic:
fun _x hx ↦
  (mem_sphere.1 hx).trans_lt h

Premises used: Set.Mem, setOf, Metric.ball, Set.Subset, Metric.mem_sphere, Eq.trans_lt, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
δ ε : ℝ
h : δ + ε ≤ dist x y
⊢ Disjoint (closedBall x δ) (ball y ε)

Tactic:
Set.disjoint_left.mpr fun _a ha1 ha2 =>
    (h.trans <| dist_triangle_left _ _ _).not_gt <| add_lt_add_of_le_of_lt ha1 ha2

Premises used: Iff.mpr, add_lt_add_of_le_of_lt, Set.disjoint_left, dist_triangle_left, LE.le.not_gt, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
δ ε : ℝ
h : δ + ε ≤ dist x y
rwa : δ + ε ≤ dist y x
rwa₁ rwa₂ rwa₃ rwa₄ : δ + ε ≤ dist x y
⊢ ε + δ ≤ dist y x

Tactic:
rwa [add_comm, dist_comm]

Premises used: dist_comm, add_comm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
δ ε : ℝ
h : δ + ε ≤ dist x y
⊢ Disjoint (ball x δ) (ball y ε)

Tactic:
(closedBall_disjoint_ball h).mono_left ball_subset_closedBall

Premises used: Metric.ball_subset_closedBall, Disjoint.mono_left, Metric.closedBall_disjoint_ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
δ ε : ℝ
h : δ + ε < dist x y
⊢ Disjoint (closedBall x δ) (closedBall y ε)

Tactic:
Set.disjoint_left.mpr fun _a ha1 ha2 =>
    h.not_ge <| (dist_triangle_left _ _ _).trans <| add_le_add ha1 ha2

Premises used: Iff.mpr, Set.disjoint_left, add_le_add, dist_triangle_left, LE.le.trans, LT.lt.not_ge
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ Disjoint (sphere x ε) (ball x ε)

Tactic:
Set.disjoint_left.mpr fun _y hy₁ hy₂ => absurd hy₁ <| ne_of_lt hy₂

Premises used: Iff.mpr, Set.disjoint_left, absurd, ne_of_lt
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
⊢ ball x ε ∪ sphere x ε = closedBall x ε

Tactic:
Set.ext fun _y => (@le_iff_lt_or_eq ℝ _ _ _).symm

Premises used: Set.ext, le_iff_lt_or_eq, Iff.symm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
rw : ball x ε ∪ sphere x ε = closedBall x ε
rw₁ rw₂ : closedBall x ε = closedBall x ε
⊢ sphere x ε ∪ ball x ε = closedBall x ε

Tactic:
rw [union_comm, ball_union_sphere]

Premises used: Set.union_comm, Metric.ball_union_sphere
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
rw : (ball x ε ∪ sphere x ε) \ sphere x ε = ball x ε
rw₁ rw₂ : ball x ε = ball x ε
⊢ closedBall x ε \ sphere x ε = ball x ε

Tactic:
rw [← ball_union_sphere, Set.union_diff_cancel_right sphere_disjoint_ball.symm.le_bot]

Premises used: Disjoint.le_bot, Metric.ball_union_sphere, Disjoint.symm, Set.union_diff_cancel_right, Metric.sphere_disjoint_ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
rw : (ball x ε ∪ sphere x ε) \ ball x ε = sphere x ε
rw₁ rw₂ : sphere x ε = sphere x ε
⊢ closedBall x ε \ ball x ε = sphere x ε

Tactic:
rw [← ball_union_sphere, Set.union_diff_cancel_left sphere_disjoint_ball.symm.le_bot]

Premises used: Disjoint.le_bot, Metric.ball_union_sphere, Disjoint.symm, Set.union_diff_cancel_left, Metric.sphere_disjoint_ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
rw : dist y x < ε ↔ y ∈ ball x ε
rw₁ rw₂ : dist y x < ε ↔ dist y x < ε
⊢ x ∈ ball y ε ↔ y ∈ ball x ε

Tactic:
rw [mem_ball', mem_ball]

Premises used: Metric.mem_ball, Metric.mem_ball'
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
rw : dist y x ≤ ε ↔ y ∈ closedBall x ε
rw₁ rw₂ : dist y x ≤ ε ↔ dist y x ≤ ε
⊢ x ∈ closedBall y ε ↔ y ∈ closedBall x ε

Tactic:
rw [mem_closedBall', mem_closedBall]

Premises used: Metric.mem_closedBall', Metric.mem_closedBall
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε : ℝ
rw : dist y x = ε ↔ y ∈ sphere x ε
rw₁ rw₂ : dist y x = ε ↔ dist y x = ε
⊢ x ∈ sphere y ε ↔ y ∈ sphere x ε

Tactic:
rw [mem_sphere', mem_sphere]

Premises used: Metric.mem_sphere, Metric.mem_sphere'
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε₁ ε₂ : ℝ
h : ε₁ ≤ ε₂
⊢ ball x ε₁ ⊆ ball x ε₂

Tactic:
fun _y yx =>
  lt_of_lt_of_le (mem_ball.1 yx) h

Premises used: Set.Mem, setOf, Metric.ball, Set.Subset, Metric.mem_ball, Iff.mp, lt_of_lt_of_le
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
h : ∀ (y : α), y ∈ closedBall x ε ↔ Membership.mem (γ := Set α) (⋂ (δ : ℝ), ⋂ (_ : δ > ε), ball x δ) y
⊢ closedBall x ε = ⋂ (δ : ℝ), ⋂ (_ : δ > ε), ball x δ

Tactic:
ext y
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
y : α
h : (∀ ⦃c : ℝ⦄, ε < c → dist y x < c) ↔ ∀ (i : ℝ) (j : i > ε), y ∈ ball x i
⊢ y ∈ closedBall x ε ↔ Membership.mem (γ := Set α) (⋂ (δ : ℝ), ⋂ (_ : δ > ε), ball x δ) y

Tactic:
rw [mem_closedBall, ← forall_gt_iff_le, mem_iInter₂]

Premises used: Set.mem_iInter₂, forall_gt_iff_le, Metric.mem_closedBall
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ (∀ ⦃c : ℝ⦄, ε < c → dist y x < c) ↔ ∀ (i : ℝ) (j : i > ε), y ∈ ball x i

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y ≤ ε₂
z : α
hz : z ∈ ball x ε₁
bc : dist z x < ε₁
⊢ dist z x + dist x y < ε₁ + dist x y

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y ≤ ε₂
z : α
hz : z ∈ ball x ε₁
⊢ dist z x < ε₁

Tactic:
hz

Premises used: Set.Mem, Metric.ball
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y ≤ ε₂
z : α
hz : z ∈ ball x ε₁
⊢ dist z x < ε₁

Tactic:
exact hz
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε₁ ε₂ : ℝ
h : ε₁ ≤ ε₂
⊢ closedBall x ε₁ ⊆ closedBall x ε₂

Tactic:
fun _y (yx : _ ≤ ε₁) => le_trans yx h

Premises used: Set.Mem, setOf, Set.Subset, Metric.closedBall, le_trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y ≤ ε₂
z : α
hz : z ∈ closedBall x ε₁
bc : dist z x ≤ ε₁
⊢ dist z x + dist x y ≤ ε₁ + dist x y

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y ≤ ε₂
z : α
hz : z ∈ closedBall x ε₁
⊢ dist z x ≤ ε₁

Tactic:
hz

Premises used: Set.Mem, Metric.closedBall
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y ≤ ε₂
z : α
hz : z ∈ closedBall x ε₁
⊢ dist z x ≤ ε₁

Tactic:
exact hz
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
ε₁ ε₂ : ℝ
h : ε₁ < ε₂
⊢ closedBall x ε₁ ⊆ ball x ε₂

Tactic:
fun y (yh : dist y x ≤ ε₁) => lt_of_le_of_lt yh h

Premises used: lt_of_le_of_lt, Set.Mem, setOf, Metric.ball, Set.Subset, Metric.closedBall
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y < ε₂
z : α
hz : z ∈ closedBall x ε₁
bc : dist z x ≤ ε₁
⊢ dist z x + dist x y ≤ ε₁ + dist x y

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y < ε₂
z : α
hz : z ∈ closedBall x ε₁
⊢ dist z x ≤ ε₁

Tactic:
hz

Premises used: Set.Mem, Metric.closedBall
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y < ε₂
z : α
hz : z ∈ closedBall x ε₁
⊢ dist z x ≤ ε₁

Tactic:
exact hz
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (closedBall x ε₁ ∩ closedBall y ε₂).Nonempty
⊢ dist x y ≤ ε₁ + ε₂

Tactic:
let ⟨z, hz⟩ := h
  calc
    dist x y ≤ dist z x + dist z y := dist_triangle_left _ _ _
    _ ≤ ε₁ + ε₂ := add_le_add hz.1 hz.2

Premises used: _private.0.Metric.dist_le_add_of_nonempty_closedBall_inter_closedBall.match_1, Trans.trans, add_le_add, dist_triangle_left, LE.le, And.right, And.left, HAdd.hAdd, Dist.dist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (closedBall x ε₁ ∩ ball y ε₂).Nonempty
⊢ dist x y < ε₁ + ε₂

Tactic:
let ⟨z, hz⟩ := h
  calc
    dist x y ≤ dist z x + dist z y := dist_triangle_left _ _ _
    _ < ε₁ + ε₂ := add_lt_add_of_le_of_lt hz.1 hz.2

Premises used: add_lt_add_of_le_of_lt, Trans.trans, dist_triangle_left, And.right, And.left, HAdd.hAdd, LT.lt, Dist.dist, _private.0.Metric.dist_lt_add_of_nonempty_closedBall_inter_ball.match_1
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (ball x ε₁ ∩ closedBall y ε₂).Nonempty
⊢ (closedBall y ε₂ ∩ ball x ε₁).Nonempty

Tactic:
rw [inter_comm] at h

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Defs
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (closedBall y ε₂ ∩ ball x ε₁).Nonempty
rw : dist y x < ε₂ + ε₁
⊢ dist x y < ε₁ + ε₂

Tactic:
rw [add_comm, dist_comm]

Premises used: dist_comm, add_comm