mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
b : β
⊢ dist (f b) (g b) ≤ dist f g

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
a b c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : b ≠ 0
this :
  ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
    [inst_3 : IsFractionRing R K] [IsDedekindDomain R] {a b c : FractionalIdeal R⁰ K},
    a ≤ c → a ≠ 0 → b ≠ 0 → b = 1 → ∃ x, a + FractionalIdeal.spanSingleton R⁰ x * b = c
hb' : ¬b = 1
⊢ b⁻¹ * a ≠ 0

Tactic:
by

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

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
hr : 0 < r
⊢ ball x r = Set.univ.pi fun b ↦ ball (x b) r

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this✝ : ∀ i < c, Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this : Icc a c ∉ f
h : b < x
⊢ Icc a b ⊆ Iio x

Tactic:
by

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

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (X b)
inst✝ : Nonempty β
x : (b : β) → X b
r : ℝ
hr : r ≤ 0
⊢ ball x r = Set.univ.pi fun b ↦ ball (x b) r

Tactic:
by

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

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ closedBall x r = Set.univ.pi fun b ↦ closedBall (x b) r

Tactic:
by

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

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝² : Fintype β
inst✝¹ : (b : β) → PseudoMetricSpace (X b)
inst✝ : Nonempty β
x : (b : β) → X b
r : ℝ
hr : r < 0
⊢ closedBall x r = Set.univ.pi fun b ↦ closedBall (x b) r

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this✝¹ : ∀ i < c, Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this✝ : Icc a c ∉ f
this : x ∈ Icc a b
⊢ Icc a x ∈ f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R✝ : Type u_1
inst✝⁸ : CommRing R✝
K✝ : Type u_2
inst✝⁷ : Field K✝
inst✝⁶ : Algebra R✝ K✝
inst✝⁵ : IsFractionRing R✝ K✝
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
a c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
⊢ Ideal.span {↑c.den} * a.num ≤ c.num * Ideal.span {↑a.den}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R✝ : Type u_1
inst✝⁸ : CommRing R✝
K✝ : Type u_2
inst✝⁷ : Field K✝
inst✝⁶ : Algebra R✝ K✝
inst✝⁵ : IsFractionRing R✝ K✝
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
a c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
H : Ideal.span {↑c.den} * a.num ≤ c.num * Ideal.span {↑a.den}
⊢ Ideal.span {↑c.den} * a.num ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this✝² : ∀ i < c, Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this✝¹ : Icc a c ∉ f
this✝ : x ∈ Icc a b
this : Icc a x ∈ f
⊢ {x} ∈ f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
⊢ IsCompact (Icc a b)

Tactic:
by

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

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
h : 0 < r ∨ Nonempty β
⊢ sphere x r = (⋃ i, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_4
inst✝ : (i : Fin (n + 1)) → PseudoMetricSpace (α i)
i : Fin (n + 1)
x y : α i
f g : (j : Fin n) → α (i.succAbove j)
c : ℝ≥0
⊢ nndist (i.insertNth x f) (i.insertNth y g) ≤ c ↔ max (nndist x y) (nndist f g) ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : IsClosed[inst✝¹] s
⊢ IsClosed[inst✝¹] ↑(upperClosure s)

Tactic:
by

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

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_4
inst✝ : (i : Fin (n + 1)) → PseudoMetricSpace (α i)
i : Fin (n + 1)
x y : α i
f g : (j : Fin n) → α (i.succAbove j)
⊢ dist (i.insertNth x f) (i.insertNth y g) = max (dist x y) (dist f g)

Tactic:
by

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

Goal state before:
pp: case pos
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
hkj : k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

Tactic:
simp_all [nndist_comm]

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

Goal state before:
pp: case neg
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
hkj : ¬k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

Tactic:
simp_all [nndist_comm]

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

Goal state before:
pp: case pos
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : ¬k = i
hkj : k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

Tactic:
simp_all [nndist_comm]

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

Goal state before:
pp: case neg
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : ¬k = i
hkj : ¬k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

Tactic:
simp_all [nndist_comm]

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

Goal state before:
pp: β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
⊢ nndist (Pi.single i a) (Pi.single j b) = max (nndist a 0) (nndist b 0)

Tactic:
by

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

Goal state before:
pp: β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
⊢ dist (Pi.single i a) (Pi.single j b) = max (dist a 0) (dist b 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
by

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

Goal state before:
pp: β : Type v
γ : Type w
inst✝¹ : MetricSpace γ
inst✝ : PseudoMetricSpace β
f : γ → β
⊢ IsUniformEmbedding f ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ

Tactic:
by

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

Goal state before:
pp: γ : Type w
inst✝ : MetricSpace γ
s : Set γ
ε : ℝ
hε : 0 < ε
hs : s.Pairwise fun x y ↦ ε ≤ dist x y
⊢ s.Pairwise fun x y ↦ (x, y) ∉ {p | dist p.1 p.2 < ε}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
ht : t.Nonempty
⊢ ∃ u, Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
by

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

Goal state before:
pp: γ : Type w
inst✝² : MetricSpace γ
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
ε : ℝ
hε : 0 < ε
f : α → γ
hf : Pairwise fun x y ↦ ε ≤ dist (f x) (f y)
⊢ Pairwise fun x y ↦ (f x, f y) ∉ {p | dist p.1 p.2 < ε}

Tactic:
by

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

Goal state before:
pp: α : Type u
β✝ : Type v
X : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
x : γ
s : Set γ
β : Type u_2
ε : ℝ
hε : 0 < ε
f : β → α
hf : Pairwise fun x y ↦ ε ≤ dist (f x) (f y)
⊢ UniformSpace α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : DenselyOrdered α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_2
ε : ℝ
hε : 0 < ε
f : β → α
hf : Pairwise fun x y ↦ ε ≤ dist (f x) (f y)
⊢ Pairwise fun x y ↦ (f x, f y) ∉ {p | dist p.1 p.2 < ε}

Tactic:
by

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

Goal state before:
pp: α✝ : Type u
β : Type v
X : Type u_1
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : EMetricSpace α
h : ∀ (x y : α), edist x y ≠ ⊤
⊢ ∀ (x y : α), 0 ≤ (edist x y).toReal

Tactic:
by

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

Goal state before:
pp: α✝ : Type u
β : Type v
X : Type u_1
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : EMetricSpace α
h : ∀ (x y : α), edist x y ≠ ⊤
⊢ ∀ (x y : α), edist x y = ENNReal.ofReal (edist x y).toReal

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
x : α
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
S : Set α
hS : S.Nonempty
hS' : BddAbove S
⊢ ∃ u, Monotone u ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
⊢ (Ioo y x ∩ s).Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
⊢ SecondCountableTopology α

Tactic:
by

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

Goal state before:
pp: α✝ : Type u
β : Type v
X : Type u_1
inst✝² : PseudoMetricSpace α✝
γ : Type w
inst✝¹ : MetricSpace γ
α : Type u
inst✝ : PseudoMetricSpace α
x y x' y' : α
hx : Inseparable x x'
hy : Inseparable y y'
⊢ dist x y = dist x' y'

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x : X), d x x = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x y : X), d x y = d y x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x y z : X), d x z ≤ d x y + d y z

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ 𝓤 X = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | d p.1 p.2 < ε}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
hnonempty : (Ioo y x ∩ s).Nonempty
hx : IsLUB (Ioo y x ∩ s) x
⊢ x ∉ Ioo y x ∩ s

Tactic:
by

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

Goal state before:
pp: X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ m.replaceEDist d hd = m

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ toUniformSpace = toUniformSpace

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x : X), d x x = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x y : X), d x y = d y x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x y z : X), d x z ≤ d x y + d y z

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x y : X), edist x y = ENNReal.ofReal (d x y)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ 𝓤 X = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | d p.1 p.2 < ε}

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ (cobounded X).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, d x y ≤ C}

Tactic:
by

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

Goal state before:
pp: X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ m.replaceDist d hd = m

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ toUniformSpace = toUniformSpace

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x ∩ s) ∧ Tendsto u atTop (𝓝 x)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ toBornology = toBornology

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x : X), d x x = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x y : X), d x y = d y x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ (x y z : X), d x z ≤ d x y + d y z

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ ∀ {x y : X}, d x y = 0 → x = y

Tactic:
by

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

Goal state before:
pp: X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ m.replaceEDist d hd = m

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ PseudoEMetricSpace.toUniformSpace = PseudoEMetricSpace.toUniformSpace

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x : X), d x x = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x y : X), d x y = d y x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ (x y z : X), d x z ≤ d x y + d y z

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ ∀ {x y : X}, d x y = 0 → x = y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
s : Set α
hs : Dense s
x : α
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Iio x ∩ s) ∧ Tendsto u atTop (𝓝 x)

Tactic:
by

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

Goal state before:
pp: X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ m.replaceDist d hd = m

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ PseudoMetricSpace.toUniformSpace = PseudoMetricSpace.toUniformSpace

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ PseudoMetricSpace.toBornology = PseudoMetricSpace.toBornology

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
β : Type u_3
inst✝² : LinearOrder β
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
f : β → α
x y : α
hf : DenseRange f
hmono : Monotone f
hlt : y < x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : LinearOrder α
inst✝⁴ : OrderTopology α
β : Type u_3
inst✝³ : LinearOrder β
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
x y : α
hy : x < y
⊢ ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo x y) ∧ Tendsto u atTop (𝓝 x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
x y : α
h : x < y
⊢ ∃ u v,
    StrictAnti u ∧
      StrictMono v ∧
        (∀ (k : ℕ), u k ∈ Ioo x y) ∧
          (∀ (l : ℕ), v l ∈ Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : x < y
⊢ ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo x y ∩ s) ∧ Tendsto u atTop (𝓝 x)

Tactic:
by

Goal state after: