mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a b x : α
⊢ Icc a b ∈ 𝓝 x ↔ Icc a b ∈ 𝓝 x

Tactic:
]

Goal state after:
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.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : α
⊢ Ioo a b = Ioo a b

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b x : α
⊢ Ico a b ∈ 𝓝 x ↔ Ico a b ∈ 𝓝 x

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b : α
⊢ Ioo a b = Ioo a b

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b x : α
⊢ Ioc a b ∈ 𝓝 x ↔ Ioc a b ∈ 𝓝 x

Tactic:
]

Goal state after:
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)
ε : ℝ≥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)) < ε}
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : a < b
⊢ {a, b} = {a, b}

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : α
h : a < b
⊢ {a, b} = {a, b}

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
s : Set α
a : α
hsa : a ∈ upperBounds s
hsf : (𝓟 s ⊓ 𝓝 a).NeBot
⊢ IsLUB s a

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
s : Set α
a : α
hsa : a ∈ upperBounds s
hsf : (𝓟 s ⊓ 𝓝 a).NeBot
⊢ IsLUB s a
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b : α
h : a < b
⊢ {a, b} = {a, b}

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
H₁ : (Ioi a).Nonempty
H₂ : a ≤ b
⊢ b ∈ Ici a

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
H₁ : (Ioi a).Nonempty
H₂ : a ≤ b
⊢ b ∈ Ici a
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b c : α
H₁ : (Iio c).Nonempty
H₂ : b ≤ c
⊢ b ∈ Iic c

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
b c : α
H₁ : (Iio c).Nonempty
H₂ : b ≤ c
⊢ b ∈ Iic c
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
x : α
hx : x ∈ upperBounds (f '' S)
i : α
hi : ∃ᶠ (x : α) in 𝓝 i, x ∈ f '' S
⊢ i ≤ x

Tactic:
]

Goal state after:
γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
x : α
hx : x ∈ upperBounds (f '' S)
i : α
hi : ∃ᶠ (x : α) in 𝓝 i, x ∈ f '' S
⊢ i ≤ x
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
h : BddAbove (range f)
⊢ sSup (range fun s ↦ f ↑s) = sSup (range fun i ↦ f i)

Tactic:
]

Goal state after:
γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
h : BddAbove (range f)
⊢ sSup (range fun s ↦ f ↑s) = sSup (range fun i ↦ f i)
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : DiscreteTopology α
a b : α
contra : a < b
⊢ Icc a b = Icc a b

Tactic:
]

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)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < r
⊢ ((∃ x, ¬nndist (f x) (g x) < r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r) ↔
    (∃ i, nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r

Tactic:
]

Goal state after:
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < r
⊢ ((∃ x, ¬nndist (f x) (g x) < r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r) ↔
    (∃ i, nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed[inst✝³] (Ico a b)
hab : a < b
this : ¬a ≤ b
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed[inst✝³] (Ico a b)
hab : a < b
this : ¬a ≤ b
⊢ False
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed[inst✝³] (Ioc a b)
hab : a < b
this : ¬a ≤ b
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed[inst✝³] (Ioc a b)
hab : a < b
this : ¬a ≤ b
⊢ False
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed[inst✝³] (Ioo a b)
hab : a < b
this : ¬a ≤ b
⊢ False

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : IsClosed[inst✝³] (Ioo a b)
hab : a < b
this : ¬a ≤ b
⊢ False
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 : β
⊢ edist (f b) (g b) ≤ edist f g

Tactic:
]

Goal state after:
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
b : β
⊢ edist (f b) (g b) ≤ edist f g
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 simp [closedBall_eq_empty.2 hr]

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:
]

Goal state after:
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})
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
⊢ sphere x 0 ⊆ ⋃ i, Function.eval i ⁻¹' sphere (x i) 0

Tactic:
]

Goal state after:
case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
⊢ sphere x 0 ⊆ ⋃ i, Function.eval i ⁻¹' sphere (x i) 0
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x✝ : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
x : (x : β) → X x
hx : ∀ (b : β), dist (x b) (x✝ b) ≤ 0
⊢ x ∈ Function.eval default ⁻¹' sphere (x✝ default) 0

Tactic:
]

Goal state after:
case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x✝ : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
x : (x : β) → X x
hx : ∀ (b : β), dist (x b) (x✝ b) ≤ 0
⊢ x ∈ Function.eval default ⁻¹' sphere (x✝ default) 0
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
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
have : ∀ k, ∀ᶠ l in atTop, v k < v l := fun k => hvx.eventually (lt_mem_nhds hvx')

Goal state after:
α : 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
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: case refine_1
α : 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
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ v (N^[x✝] 0) < v (N (N^[x✝] 0))

Tactic:
]

Goal state after:
case refine_1
α : 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
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ v (N^[x✝] 0) < v (N (N^[x✝] 0))
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: case refine_2
α : 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
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ N^[x✝] 0 < N (N^[x✝] 0)

Tactic:
]

Goal state after:
case refine_2
α : 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
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ N^[x✝] 0 < N (N^[x✝] 0)
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: β : Type v
γ : Type w
inst✝¹ : MetricSpace γ
inst✝ : PseudoMetricSpace β
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 < δ) ↔
    (∀ ε > 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:
]

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'
⊢ (edist (mk x') (mk y')).toReal = (edist (mk x') (mk y')).toReal

Tactic:
]

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

Goal state before:
pp: case inl.inr
α : Type u_1
γ : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
l : Filter γ
inst✝ : CountableInterFilter l
f : γ → α
d : α
hd : IsGLB (Ioi d) d
h✝ : ∃ b, d < b
u : ℕ → α
hu_tt : Tendsto u atTop (𝓝 d)
hu_gt : ∀ (n : ℕ), u n ∈ Ioi d
h : ∀ᶠ (x : γ) in l, ∀ (i : ℕ), f x < u i
⊢ ∀ᶠ (x : γ) in l, f x ≤ d

Tactic:
]

Goal state after:
case inl.inr
α : Type u_1
γ : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
l : Filter γ
inst✝ : CountableInterFilter l
f : γ → α
d : α
hd : IsGLB (Ioi d) d
h✝ : ∃ b, d < b
u : ℕ → α
hu_tt : Tendsto u atTop (𝓝 d)
hu_gt : ∀ (n : ℕ), u n ∈ Ioi d
h : ∀ᶠ (x : γ) in l, ∀ (i : ℕ), f x < u i
⊢ ∀ᶠ (x : γ) in l, f x ≤ d
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
l : Filter γ
inst✝ : CountableInterFilter l
f : γ → α
a d : α
h : ∀ᶠ (x : γ) in l, f x < d
hd : IsGLB (Ioi a) d
H0 : Iic a = Iio d
x : γ
hx : f x < d
⊢ f x ≤ a

Tactic:
]

Goal state after:
α : Type u_1
γ : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
l : Filter γ
inst✝ : CountableInterFilter l
f : γ → α
a d : α
h : ∀ᶠ (x : γ) in l, f x < d
hd : IsGLB (Ioi a) d
H0 : Iic a = Iio d
x : γ
hx : f x < d
⊢ f x ≤ a
Module: Mathlib.Analysis.Normed.Group.Real

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
r _r _y : ℝ
⊢ |_y + -_r| = |_y + -_r|

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Real

Goal state before:
pp: r : ℝ
hr : 0 ≤ r
⊢ ENNReal.ofReal r = ENNReal.ofReal r

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Real

Goal state before:
pp: r : ℝ
⊢ ‖r‖ₑ = ‖r‖ₑ

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Real

Goal state before:
pp: r : ℝ
hr : 0 ≤ r
⊢ NNReal.mk r hr = ‖r‖₊

Tactic:
]

Goal state after:
r : ℝ
hr : 0 ≤ r
⊢ NNReal.mk r hr = ‖r‖₊
Module: Mathlib.Analysis.Normed.Group.Real

Goal state before:
pp: r : ℝ
hr : 0 ≤ r
⊢ r = r

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Real

Goal state before:
pp: r : ℝ
⊢ ENNReal.ofReal r ≤ ENNReal.ofReal |r|

Tactic:
]

Goal state after:
r : ℝ
⊢ ENNReal.ofReal r ≤ ENNReal.ofReal |r|
Module: Mathlib.Topology.Instances.Discrete

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ ∀ (a : α), (pure a).IsCountablyGenerated

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
⊢ ∀ (a : α), (pure a).IsCountablyGenerated
Module: Mathlib.Topology.Instances.Discrete

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
h : DiscreteTopology α
⊢ ⊥ = Preorder.topology α

Tactic:
LinearOrder.bot_topologicalSpace_eq_preorderTopology

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
h : DiscreteTopology α
⊢ Preorder.topology α = Preorder.topology α
Module: Mathlib.Topology.Instances.Discrete

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
h : DiscreteTopology α
⊢ Preorder.topology α = Preorder.topology α

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Constructions

Goal state before:
pp: ι : Type u_1
E : Type u_2
F : Type u_3
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Fintype F
g : ι → E
f : F → ι
⊢ ∀ (i : F), ‖(g ∘ f) i‖ ≤ ‖g‖

Tactic:
]

Goal state after:
ι : Type u_1
E : Type u_2
F : Type u_3
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Fintype F
g : ι → E
f : F → ι
⊢ ∀ (i : F), ‖(g ∘ f) i‖ ≤ ‖g‖
Module: Mathlib.Analysis.Normed.Group.Constructions

Goal state before:
pp: case left
ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Nonempty ι
f : ι → E
⊢ ↑(Finset.univ.sup fun b ↦ ‖f b‖₊) ∈ Set.range fun x ↦ ‖f x‖

Tactic:
]

Goal state after:
case left
ι : Type u_1
E : Type u_2
inst✝² : Fintype ι
inst✝¹ : SeminormedGroup E
inst✝ : Nonempty ι
f : ι → E
⊢ ↑(Finset.univ.sup fun b ↦ ‖f b‖₊) ∈ Set.range fun x ↦ ‖f x‖
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝² : Bornology α
inst✝¹ : Lattice α
inst✝ : Nonempty α
h : inst✝² = orderBornology
s : Set α
⊢ BddBelow s ∧ BddAbove s ↔ BddBelow s ∧ BddAbove s

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s✝ t : Set α
inst✝² : Bornology α
inst✝¹ : Preorder α
inst✝ : IsOrderBornology α
s : Set αᵒᵈ
⊢ BddAbove (⇑toDual ⁻¹' s) ∧ BddBelow (⇑toDual ⁻¹' s) ↔ BddAbove (⇑toDual ⁻¹' s) ∧ BddBelow (⇑toDual ⁻¹' s)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s✝ t : Set α
inst✝⁵ : Bornology α
inst✝⁴ : Preorder α
inst✝³ : IsOrderBornology α
β : Type u_2
inst✝² : Preorder β
inst✝¹ : Bornology β
inst✝ : IsOrderBornology β
s : Set (α × β)
⊢ (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ BddBelow (snd '' s) ∧ BddAbove (snd '' s) ↔
    (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ BddBelow (snd '' s) ∧ BddAbove (snd '' s)

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
s : Set α
hs : BddBelow sᶜ ∧ BddAbove sᶜ
⊢ s ∈ Filter.atTop

Tactic:
]

Goal state after:
α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
s : Set α
hs : BddBelow sᶜ ∧ BddAbove sᶜ
⊢ s ∈ Filter.atTop
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
⊢ ((∃ i, True ∧ Iic i ⊆ s) ∧ ∃ i, True ∧ Ici i ⊆ s) → BddBelow sᶜ ∧ BddAbove sᶜ

Tactic:
]

Goal state after:
α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
⊢ ((∃ i, True ∧ Iic i ⊆ s) ∧ ∃ i, True ∧ Ici i ⊆ s) → BddBelow sᶜ ∧ BddAbove sᶜ
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝⁴ : Bornology α
inst✝³ : LinearOrder α
inst✝² : IsOrderBornology α
inst✝¹ : NoMaxOrder α
inst✝ : OrderBot α
s : Set α
⊢ (∃ i, True ∧ Ici i ⊆ s) → BddBelow sᶜ ∧ BddAbove sᶜ

Tactic:
]

Goal state after:
α : Type u_1
inst✝⁴ : Bornology α
inst✝³ : LinearOrder α
inst✝² : IsOrderBornology α
inst✝¹ : NoMaxOrder α
inst✝ : OrderBot α
s : Set α
⊢ (∃ i, True ∧ Ici i ⊆ s) → BddBelow sᶜ ∧ BddAbove sᶜ
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case refine_2
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}
x : R
hx : Ideal.span {↑c.den} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {↑a.den}
⊢ FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑c.den) * ↑a.num +
      FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) x) =
    ↑c.num * FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑a.den)

Tactic:
]

Goal state after:
case refine_2
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}
x : R
hx : Ideal.span {↑c.den} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {↑a.den}
⊢ FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑c.den) * ↑a.num +
      FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) x) =
    ↑c.num * FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑a.den)