mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: case mk
α : Type u_2
inst✝ : TopologicalSpace α
m' : WeakPseudoEMetricSpace α
toEDist✝ : EDist α
edist_self✝ : ∀ (x : α), edist x x = 0
edist_comm✝ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
topology_le✝ : (uniformSpaceOfEDist edist edist_self✝ edist_comm✝ edist_triangle✝).toTopologicalSpace ≤ inst✝
topology_eq_on_restrict✝ :
  ∀ (x : α) (r : ℝ≥0∞), IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
h :
  { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
        topology_le := topology_le✝, topology_eq_on_restrict := topology_eq_on_restrict✝ }.toEDist =
    m'.toEDist
⊢ { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
      topology_le := topology_le✝, topology_eq_on_restrict := topology_eq_on_restrict✝ } =
    m'

Tactic:
;

Goal state after:
case mk
α : Type u_2
inst✝ : TopologicalSpace α
m' : WeakPseudoEMetricSpace α
toEDist✝ : EDist α
edist_self✝ : ∀ (x : α), edist x x = 0
edist_comm✝ : ∀ (x y : α), edist x y = edist y x
edist_triangle✝ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
topology_le✝ : (uniformSpaceOfEDist edist edist_self✝ edist_comm✝ edist_triangle✝).toTopologicalSpace ≤ inst✝
topology_eq_on_restrict✝ :
  ∀ (x : α) (r : ℝ≥0∞), IsOpen[instTopologicalSpaceSubtype] (Metric.eball x ∞ ↓∩ Metric.eball x r)
h :
  { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
        topology_le := topology_le✝, topology_eq_on_restrict := topology_eq_on_restrict✝ }.toEDist =
    m'.toEDist
⊢ { toEDist := toEDist✝, edist_self := edist_self✝, edist_comm := edist_comm✝, edist_triangle := edist_triangle✝,
      topology_le := topology_le✝, topology_eq_on_restrict := topology_eq_on_restrict✝ } =
    m'
Module: Mathlib.Topology.MetricSpace.Defs

Goal state before:
pp: case mk
α : Type u_3
m' : MetricSpace α
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : { toPseudoMetricSpace := toPseudoMetricSpace✝, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝ }.toDist = m'.toDist
⊢ { toPseudoMetricSpace := toPseudoMetricSpace✝, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝ } = m'

Tactic:
;

Goal state after:
case mk
α : Type u_3
m' : MetricSpace α
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h : { toPseudoMetricSpace := toPseudoMetricSpace✝, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝ }.toDist = m'.toDist
⊢ { toPseudoMetricSpace := toPseudoMetricSpace✝, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝ } = m'
Module: Mathlib.Topology.MetricSpace.Defs

Goal state before:
pp: case mk.mk
α : Type u_3
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h :
  { toPseudoMetricSpace := toPseudoMetricSpace✝¹, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝¹ }.toDist =
    { toPseudoMetricSpace := toPseudoMetricSpace✝, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝ }.toDist
⊢ { toPseudoMetricSpace := toPseudoMetricSpace✝¹, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝¹ } =
    { toPseudoMetricSpace := toPseudoMetricSpace✝, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝ }

Tactic:
;

Goal state after:
case mk.mk
α : Type u_3
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h :
  { toPseudoMetricSpace := toPseudoMetricSpace✝¹, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝¹ }.toDist =
    { toPseudoMetricSpace := toPseudoMetricSpace✝, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝ }.toDist
⊢ { toPseudoMetricSpace := toPseudoMetricSpace✝¹, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝¹ } =
    { toPseudoMetricSpace := toPseudoMetricSpace✝, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝ }
Module: Mathlib.Topology.MetricSpace.Defs

Goal state before:
pp: case mk.mk
α : Type u_3
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h :
  { toPseudoMetricSpace := toPseudoMetricSpace✝¹, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝¹ }.toDist =
    { toPseudoMetricSpace := toPseudoMetricSpace✝, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝ }.toDist
⊢ toPseudoMetricSpace✝¹ = toPseudoMetricSpace✝

Tactic:
;

Goal state after:
case mk.mk
α : Type u_3
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h :
  { toPseudoMetricSpace := toPseudoMetricSpace✝¹, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝¹ }.toDist =
    { toPseudoMetricSpace := toPseudoMetricSpace✝, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝ }.toDist
⊢ toPseudoMetricSpace✝¹ = toPseudoMetricSpace✝
Module: Mathlib.Topology.MetricSpace.Defs

Goal state before:
pp: case mk.mk
α : Type u_3
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h :
  { toPseudoMetricSpace := toPseudoMetricSpace✝¹, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝¹ }.toDist =
    { toPseudoMetricSpace := toPseudoMetricSpace✝, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝ }.toDist
⊢ toPseudoMetricSpace✝¹.toDist = toPseudoMetricSpace✝.toDist

Tactic:
;

Goal state after:
case mk.mk
α : Type u_3
toPseudoMetricSpace✝¹ : PseudoMetricSpace α
eq_of_dist_eq_zero✝¹ : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace✝ : PseudoMetricSpace α
eq_of_dist_eq_zero✝ : ∀ {x y : α}, dist x y = 0 → x = y
h :
  { toPseudoMetricSpace := toPseudoMetricSpace✝¹, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝¹ }.toDist =
    { toPseudoMetricSpace := toPseudoMetricSpace✝, eq_of_dist_eq_zero := eq_of_dist_eq_zero✝ }.toDist
⊢ toPseudoMetricSpace✝¹.toDist = toPseudoMetricSpace✝.toDist
Module: Mathlib.Topology.MetricSpace.Defs

Goal state before:
pp: γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ nndist x y = 0 ↔ x = y

Tactic:
simp only [NNReal.eq_iff, ← dist_nndist, NNReal.coe_zero, dist_eq_zero]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Defs

Goal state before:
pp: γ : Type u_3
U : UniformSpace γ
m : MetricSpace γ
H : 𝓤 γ = 𝓤 γ
x✝¹ x✝ : γ
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Tactic:
;

Goal state after:
γ : Type u_3
U : UniformSpace γ
m : MetricSpace γ
H : 𝓤 γ = 𝓤 γ
x✝¹ x✝ : γ
⊢ dist x✝¹ x✝ = dist x✝¹ x✝
Module: Mathlib.Topology.MetricSpace.Defs

Goal state before:
pp: γ : Type u_3
U : TopologicalSpace γ
m : MetricSpace γ
H : U = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x✝¹ x✝ : γ
⊢ dist x✝¹ x✝ = dist x✝¹ x✝

Tactic:
;

Goal state after:
γ : Type u_3
U : TopologicalSpace γ
m : MetricSpace γ
H : U = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
x✝¹ x✝ : γ
⊢ dist x✝¹ x✝ = dist x✝¹ x✝
Module: Mathlib.Analysis.Normed.Group.Defs

Goal state before:
pp: 𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝² : Norm E
inst✝¹ : Group E
inst✝ : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)
x y : E
⊢ dist x y = dist 1 (x⁻¹ * y)

Tactic:
;

Goal state after:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝² : Norm E
inst✝¹ : Group E
inst✝ : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)
x y : E
⊢ dist x y = dist 1 (x⁻¹ * y)
Module: Mathlib.Analysis.Normed.Group.Defs

Goal state before:
pp: 𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝² : Norm E
inst✝¹ : Group E
inst✝ : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y
x y : E
⊢ dist x y = dist 1 (x⁻¹ * y)

Tactic:
;

Goal state after:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝² : Norm E
inst✝¹ : Group E
inst✝ : PseudoMetricSpace E
h₁ : ∀ (x : E), ‖x‖ = dist 1 x
h₂ : ∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y
x y : E
⊢ dist x y = dist 1 (x⁻¹ * y)
Module: Mathlib.Analysis.Normed.Group.Defs

Goal state before:
pp: 𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝ : Group E
f : GroupSeminorm E
x y : E
⊢ x⁻¹ * y = (y⁻¹ * x)⁻¹

Tactic:
;

Goal state after:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝ : Group E
f : GroupSeminorm E
x y : E
⊢ x⁻¹ * y = (y⁻¹ * x)⁻¹
Module: Mathlib.Analysis.Normed.Group.Defs

Goal state before:
pp: case e'_3
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝ : Group E
f : GroupSeminorm E
x y z : E
⊢ x⁻¹ * z = x⁻¹ * y * (y⁻¹ * z)

Tactic:
;

Goal state after:
case e'_3
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝ : Group E
f : GroupSeminorm E
x y z : E
⊢ x⁻¹ * z = x⁻¹ * y * (y⁻¹ * z)
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ ENNReal.ofReal x⁻¹ = (ENNReal.ofReal x)⁻¹

Tactic:
ENNReal.ofReal,

Goal state after:
x : ℝ
hx : 0 < x
⊢ ↑x⁻¹.toNNReal = (ENNReal.ofReal x)⁻¹
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ ↑x⁻¹.toNNReal = (ENNReal.ofReal x)⁻¹

Tactic:
ENNReal.ofReal,

Goal state after:
x : ℝ
hx : 0 < x
⊢ ↑x⁻¹.toNNReal = (↑x.toNNReal)⁻¹
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y z : α
⊢ dist x y ≤ dist x z + dist z y

Tactic:
;

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y z : α
⊢ dist x y ≤ dist x z + dist z y
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case h₁
α : Type u
inst✝ : PseudoMetricSpace α
x y z w : α
⊢ dist x z ≤ dist x y + dist y z

Tactic:
;

Goal state after:
case h₁
α : Type u
inst✝ : PseudoMetricSpace α
x y z w : α
⊢ dist x z ≤ dist x y + dist y z
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe.inl
⊢ (↑0)⁻¹.toNNReal = (↑0).toNNReal⁻¹

pp: case coe.inr
a : ℝ≥0
ha : a ≠ 0
⊢ (↑a)⁻¹.toNNReal = (↑a).toNNReal⁻¹

Tactic:
;

Goal state after:
case coe.inl
⊢ (↑0)⁻¹.toNNReal = (↑0).toNNReal⁻¹

case coe.inr
a : ℝ≥0
ha : a ≠ 0
⊢ (↑a)⁻¹.toNNReal = (↑a).toNNReal⁻¹
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ Function.swap dist x y = dist x y

Tactic:
;

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ Function.swap dist x y = dist x y
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
r : ℝ
⊢ ENNReal.ofReal (dist x y) < ENNReal.ofReal r ↔ dist x y < r

Tactic:
ENNReal.ofReal_lt_ofReal_iff_of_nonneg dist_nonneg

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
r : ℝ
⊢ dist x y < r ↔ dist x y < r
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝² : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
inst✝¹ : Subsingleton α
inst✝ : NeZero ε
⊢ IsEmpty ↑∅

Tactic:
;

Goal state after:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝² : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
inst✝¹ : Subsingleton α
inst✝ : NeZero ε
⊢ IsEmpty ↑∅
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ y ∈ closedBall x ε ↔ y ∈ ⋂ δ, ⋂ (_ : δ > ε), ball x δ

Tactic:
;

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ y ∈ closedBall x ε ↔ y ∈ ⋂ δ, ⋂ (_ : δ > ε), ball x δ
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ (∀ ⦃c : ℝ⦄, ε < c → dist y x < c) ↔ ∀ i > ε, y ∈ ball x i

Tactic:
;

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ (∀ ⦃c : ℝ⦄, ε < c → dist y x < c) ↔ ∀ i > ε, y ∈ ball x i
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case bc
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y ≤ ε₂
z : α
hz : z ∈ ball x ε₁
⊢ dist z x < ε₁

Tactic:
;

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

Goal state before:
pp: case h₁
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y ≤ ε₂
z : α
hz : z ∈ closedBall x ε₁
⊢ dist z x ≤ ε₁

Tactic:
;

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

Goal state before:
pp: case h₁
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y < ε₂
z : α
hz : z ∈ closedBall x ε₁
⊢ dist z x ≤ ε₁

Tactic:
;

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
h : y ∈ ball x (ε / 2)
⊢ dist y x ≤ ε / 2

Tactic:
;

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
h : y ∈ ball x (ε / 2)
⊢ dist y x ≤ ε / 2
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 ≤ ε
y : α
⊢ y ∈ closedEBall x (ENNReal.ofReal ε) ↔ y ∈ closedBall x ε

Tactic:
;

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : 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

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x r : ℝ
hr : 0 ≤ r
x✝ : ℝ
⊢ x✝ ∈ sphere x r ↔ x✝ ∈ {x - r, x + r}

Tactic:
;

Goal state after:
x r : ℝ
hr : 0 ≤ r
x✝ : ℝ
⊢ x✝ ∈ sphere x r ↔ x✝ ∈ {x - r, x + r}
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x r : ℝ
hr : 0 ≤ r
x✝ : ℝ
⊢ |x✝ - x| = r ↔ x✝ = x - r ∨ x✝ = x + r

Tactic:
;

Goal state after:
x r : ℝ
hr : 0 ≤ r
x✝ : ℝ
⊢ |x✝ - x| = r ↔ x✝ = x - r ∨ x✝ = x + r
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n

Tactic:
;

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n
Module: Mathlib.Topology.Bornology.Constructions

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : Bornology α
inst✝ : Bornology β
t : Set β
⊢ IsBounded (∅ ×ˢ t) ↔ ∅ = ∅ ∨ t = ∅ ∨ IsBounded ∅ ∧ IsBounded t

pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : Bornology α
inst✝ : Bornology β
s : Set α
t : Set β
hs : s.Nonempty
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t

Tactic:
;

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : Bornology α
inst✝ : Bornology β
t : Set β
⊢ IsBounded (∅ ×ˢ t) ↔ ∅ = ∅ ∨ t = ∅ ∨ IsBounded ∅ ∧ IsBounded t

case inr
α : Type u_1
β : Type u_2
inst✝¹ : Bornology α
inst✝ : Bornology β
s : Set α
t : Set β
hs : s.Nonempty
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
Module: Mathlib.Topology.Bornology.Constructions

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : Bornology α
inst✝ : Bornology β
s : Set α
hs : s.Nonempty
⊢ IsBounded (s ×ˢ ∅) ↔ s = ∅ ∨ ∅ = ∅ ∨ IsBounded s ∧ IsBounded ∅

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : Bornology α
inst✝ : Bornology β
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t

Tactic:
;

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : Bornology α
inst✝ : Bornology β
s : Set α
hs : s.Nonempty
⊢ IsBounded (s ×ˢ ∅) ↔ s = ∅ ∨ ∅ = ∅ ∨ IsBounded s ∧ IsBounded ∅

case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : Bornology α
inst✝ : Bornology β
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
⊢ IsBounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ IsBounded s ∧ IsBounded t
Module: Mathlib.Topology.Bornology.Constructions

Goal state before:
pp: case inl
α : Type u_1
inst✝ : Bornology α
⊢ IsBounded (∅ ×ˢ ∅) ↔ IsBounded ∅

pp: case inr
α : Type u_1
inst✝ : Bornology α
s : Set α
hs : s.Nonempty
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s

Tactic:
;

Goal state after:
case inl
α : Type u_1
inst✝ : Bornology α
⊢ IsBounded (∅ ×ˢ ∅) ↔ IsBounded ∅

case inr
α : Type u_1
inst✝ : Bornology α
s : Set α
hs : s.Nonempty
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n

Tactic:
;

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n✝ n : ℕ
hle : m ≤ n
ihn : edist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, edist (f i) (f (i + 1))
⊢ n ∉ Finset.Ico m n
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
⊢ (∀ (i' : ℝ≥0∞),
      0 < i' →
        ∃ i,
          0 < i ∧ ∀ (a b : α), (a, b) ∈ Prod.map f f ⁻¹' {p | edist p.1 p.2 < i} → (a, b) ∈ {p | edist p.1 p.2 < i'}) ↔
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
f : α → β
⊢ (∀ (i' : ℝ≥0∞),
      0 < i' →
        ∃ i,
          0 < i ∧ ∀ (a b : α), (a, b) ∈ Prod.map f f ⁻¹' {p | edist p.1 p.2 < i} → (a, b) ∈ {p | edist p.1 p.2 < i'}) ↔
    ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : Filter α
⊢ Cauchy f ↔ f.NeBot ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε

Tactic:
;

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
f : Filter α
⊢ Cauchy f ↔ f.NeBot ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hc₂ : s ⊆ ⋃ i, ↑i
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, eball x δ ⊆ t

Tactic:
;

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
hc₂ : s ⊆ ⋃ i, ↑i
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, eball x δ ⊆ t
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: c x : ℝ≥0
⊢ x ∈ ball 0 ↑c ↔ x ∈ Ico 0 c

Tactic:
;

Goal state after:
c x : ℝ≥0
⊢ x ∈ ball 0 ↑c ↔ x ∈ Ico 0 c
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: c x : ℝ≥0
⊢ x ∈ closedBall 0 ↑c ↔ x ∈ Icc 0 c

Tactic:
;

Goal state after:
c x : ℝ≥0
⊢ x ∈ closedBall 0 ↑c ↔ x ∈ Icc 0 c
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x y : α × β
⊢ edist x y = ENNReal.ofReal (max (dist x.1 y.1) (dist x.2 y.2))

Tactic:
simp only [ENNReal.ofReal_max, Prod.edist_eq, edist_dist]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
x' : α
y' : β
hr : 0 < dist x' x.1
⊢ dist y' x.2 ≤ dist x' x.1 ↔ dist y' x.2 ≤ dist x' x.1

Tactic:
;

Goal state after:
case inr.inr.refine_1
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
x' : α
y' : β
hr : 0 < dist x' x.1
⊢ dist y' x.2 ≤ dist x' x.1 ↔ dist y' x.2 ≤ dist x' x.1
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: case inr.inr.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
x' : α
y' : β
hr : 0 < dist y' x.2
⊢ dist x' x.1 ≤ dist y' x.2 ↔ dist x' x.1 ≤ dist y' x.2

Tactic:
;

Goal state after:
case inr.inr.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
x' : α
y' : β
hr : 0 < dist y' x.2
⊢ dist x' x.1 ≤ dist y' x.2 ↔ dist x' x.1 ≤ dist y' x.2
Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hc₂ : s ⊆ ⋃ i, ↑i
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, ball x δ ⊆ t

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : PseudoMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hc₂ : s ⊆ ⋃ i, ↑i
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, ball x δ ⊆ t
Module: Mathlib.Topology.EMetricSpace.Pi

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
⊢ ⨅ j, ⨅ i, ⨅ (_ : 0 < j), 𝓟 {a | edist (a.1 i) (a.2 i) < j} =
    ⨅ ε, ⨅ (_ : 0 < ε), 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}

Tactic:
;

Goal state after:
α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
⊢ ⨅ j, ⨅ i, ⨅ (_ : 0 < j), 𝓟 {a | edist (a.1 i) (a.2 i) < j} =
    ⨅ ε, ⨅ (_ : 0 < ε), 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}
Module: Mathlib.Topology.EMetricSpace.Pi

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
⊢ (fun j ↦ ⨅ i, ⨅ (_ : 0 < j), 𝓟 {a | edist (a.1 i) (a.2 i) < j}) = fun ε ↦
    ⨅ (_ : 0 < ε), 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}

Tactic:
;

Goal state after:
α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
⊢ (fun j ↦ ⨅ i, ⨅ (_ : 0 < j), 𝓟 {a | edist (a.1 i) (a.2 i) < j}) = fun ε ↦
    ⨅ (_ : 0 < ε), 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}
Module: Mathlib.Topology.EMetricSpace.Pi

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
ε : ℝ≥0∞
⊢ ⨅ (_ : 0 < ε), ⨅ i, 𝓟 {a | edist (a.1 i) (a.2 i) < ε} =
    ⨅ (_ : 0 < ε), 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}

Tactic:
;

Goal state after:
α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
ε : ℝ≥0∞
⊢ ⨅ (_ : 0 < ε), ⨅ i, 𝓟 {a | edist (a.1 i) (a.2 i) < ε} =
    ⨅ (_ : 0 < ε), 𝓟 {p | (Finset.univ.sup fun b ↦ edist (p.1 b) (p.2 b)) < ε}