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

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
h : StrictAntiOn f (Icc s t)
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : IsDirectedOrder α
k : α
⊢ map (fun a ↦ a - k) atTop = atTop

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
s : Set β
⊢ (∃ C, ∀ ⦃x : α⦄, x ∈ f '' s → ∀ ⦃y : α⦄, y ∈ f '' s → dist x y ≤ C) ↔ ∃ C, ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ C

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
s : Set β
⊢ (∃ C, ∀ ⦃x : α⦄, x ∈ f '' s → ∀ ⦃y : α⦄, y ∈ f '' s → dist x y ≤ C) ↔ ∃ C, ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ C

Tactic:
by simp only [forall_mem_image]

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

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
⊢ StrictMono f

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
this : Fact (a ≤ b)
g : ↑(Icc a b) → δ := (Icc a b).domRestrict f
⊢ g ⊥ ≤ g ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ b ≤ 1 * max b 0

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
⊢ Bornology.IsBounded (range f)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a ≤ b
hfab : f a ≤ f b
hf_c : ContinuousOn f (Icc a b)
hf_i : InjOn f (Icc a b)
⊢ StrictMonoOn f (Icc a b)

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
hf : CauchySeq f
⊢ Cauchy (map f Filter.cofinite)

Tactic:
by

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

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
hJ : J ≠ ⊥
⊢ multiplicity p.asIdeal (I ⊔ J) = min (multiplicity p.asIdeal I) (multiplicity p.asIdeal J)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ 1 * max b 0 ≤ r * ↑n * max b 0

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ r * ↑n * max b 0 = r * (↑n * max b 0)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
⊢ Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ r * ↑n
x : α
hx : ↑n * max b 0 ≤ f x
⊢ r * (↑n * max b 0) ≤ r * f x

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
⊢ StrictMono f ∨ StrictAnti f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ r * f x) l atTop

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
⊢ 1 ≤ ↑n * r

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a < b
hf_c : ContinuousOn f (Ioo a b)
hf_i : InjOn f (Ioo a b)
⊢ StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
⊢ ∃ t, k ⊆ t ∧ IsOpen[inst✝] t ∧ Bornology.IsBounded (f '' (t ∩ s))

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ b ≤ max b 0 * 1

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ max b 0 * 1 ≤ max b 0 * (↑n * r)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ max b 0 * (↑n * r) = max b 0 * ↑n * r

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousAt f x
⊢ ∃ t, k ⊆ t ∧ IsOpen[inst✝] t ∧ Bornology.IsBounded (f '' t)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
b : R
n : ℕ
hn : 1 ≤ n • r
hn' : 1 ≤ ↑n * r
x : α
hx : max b 0 * ↑n ≤ f x
⊢ max b 0 * ↑n * r ≤ f x * r

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x * r) l atTop

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x * r) l atBot

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf : StrictMono f
⊢ f '' Icc a b = Icc (f a) (f b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : 0 < r
hf : Tendsto f l atBot
⊢ Tendsto (fun x ↦ f x * r) l atBot

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
f : α → R
r : R
inst✝³ : Ring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : Archimedean R
hr : r < 0
hf : Tendsto f l atBot
⊢ Tendsto (fun x ↦ f x * r) l atTop

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedCancelAddMonoid R
inst✝ : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x • r) l atTop

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
hc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hb : Bornology.IsBounded s
⊢ IsCompact s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
f : α → ℕ
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x • r) l atBot

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ s ≤ ↑n • r

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x • r) l atTop

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
f : α → ℤ
hr : r < 0
hf : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x • r) l atBot

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
f : α → ℤ
hr : 0 < r
hf : Tendsto f l atBot
⊢ Tendsto (fun x ↦ f x • r) l atBot

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf : StrictMono f
⊢ f '' Ico a b = Ico (f a) (f b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:
pp: α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝³ : AddCommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
f : α → ℤ
hr : r < 0
hf : Tendsto f l atBot
⊢ Tendsto (fun x ↦ f x • r) l atTop

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝² : PseudoMetricSpace α
inst✝¹ : Preorder α
inst✝ : CompactIccSpace α
x : α
bddBelow_ball : ∀ (r : ℝ), BddBelow (closedBall x r)
bddAbove_ball : ∀ (r : ℝ), BddAbove (closedBall x r)
s : Set α
⊢ Bornology.IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝⁴ : AddCommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompactIccSpace α
C : α
⊢ Bornology.IsBounded {x | |x| ≤ C}

Tactic:
by

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

Goal state before:
pp: α : Type u_3
inst✝⁴ : AddCommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompactIccSpace α
C : α
⊢ Bornology.IsBounded {x | |x| < C}

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf : StrictMono f
⊢ f '' Ioc a b = Ioc (f a) (f b)

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : PseudoMetricSpace α
hs : s.Subsingleton
⊢ diam s = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : PseudoMetricSpace α
⊢ diam {x, y} = dist x y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: m n : ℤ
⊢ dist m n = ↑|m - n|

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: ⊢ Pairwise fun m n ↦ 1 ≤ dist m n

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: x : ℤ
r : ℝ
⊢ ball x r = Ioo ⌊↑x - r⌋ ⌈↑x + r⌉

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: x : ℤ
r : ℝ
⊢ closedBall x r = Icc ⌈↑x - r⌉ ⌊↑x + r⌋

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: x : ℤ
r : ℝ
⊢ IsCompact (closedBall x r)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: ⊢ ∀ (r : ℝ), BddBelow (closedBall 0 r)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: ⊢ ∀ (r : ℝ), BddAbove (closedBall 0 r)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Instances.Int

Goal state before:
pp: ⊢ cofinite = atBot ⊔ atTop

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf : StrictMono f
⊢ f '' Ioo a b = Ioo (f a) (f b)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
m n : ℤ
⊢ dist m n = ‖↑(-m + n)‖

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ‖↑n‖ = ↑n

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ ↑↑n.natAbs = ↑↑n.natAbs

Tactic:
by

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

Goal state before:
pp: n : ℤ
⊢ ↑↑n.natAbs = |↑n|

Tactic:
by

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

Goal state before:
pp: z : ℤ
c : ℝ≥0
⊢ |z| ≤ ↑⌊c⌋₊ ↔ ‖z‖₊ ≤ c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedCommGroup α
n : ℤ
a : α
⊢ ‖a ^ n‖ ≤ ‖n‖ * ‖a‖

Tactic:
by

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : PseudoMetricSpace α
⊢ diam {x, y, z} = max (max (dist x y) (dist x z)) (dist y z)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : SeminormedCommGroup α
n : ℤ
a : α
⊢ ‖a ^ n‖₊ ≤ ‖n‖₊ * ‖a‖₊

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
x y : α
inst✝ : PseudoMetricSpace α
h : ediam s ≠ ∞
hx : x ∈ s
hy : y ∈ s
⊢ dist x y ≤ diam s

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
⊢ ediam univ = ∞ ↔ NoncompactSpace α

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝² : PseudoMetricSpace α
inst✝¹ : ProperSpace α
inst✝ : NoncompactSpace α
⊢ diam univ = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : PseudoMetricSpace α
h : ¬Bornology.IsBounded s
⊢ diam s = 0

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
x y : α
inst✝ : PseudoMetricSpace α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ diam (s ∪ t) ≤ diam s + dist x y + diam t

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : PseudoMetricSpace α
t : Set α
h : (s ∩ t).Nonempty
⊢ diam (s ∪ t) ≤ diam s + diam t

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
x : α
inst✝ : PseudoMetricSpace α
r : ℝ
hr : 0 ≤ r
h : s ⊆ closedBall x r
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ r + r = 2 * r

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n ↦ diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N ↦ ⋯.some
⊢ ∀ (n N : ℕ), n ≤ N → u N ∈ s n

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n ↦ diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N ↦ ⋯.some
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
⊢ CauchySeq u

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n ↦ diam (s n)) atTop (𝓝 0)
⊢ (⋂ n, s n).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 1 < g}
a_in : a ∈ H
a_pos : 1 < a
⊢ {a} ⊆ ↑H

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : MetricSpace α
hs1 : s.Nontrivial
hs2 : Bornology.IsBounded s
⊢ 0 < diam s

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
⊢ cobounded α = cocompact α

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
⊢ comap (dist x) atTop = cocompact α

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
K s : Set α
hsd : IsDiscrete s
hK : Bornology.IsBounded K
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ (K ∩ s).Finite

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : PseudoMetricSpace β
inst✝ : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝³] f
x₀ : β
h : Bornology.IsBounded {x | f x ≤ f x₀}
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝³] f

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : PseudoMetricSpace β
inst✝ : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝³] f
x₀ : β
h : Bornology.IsBounded {x | f x ≤ f x₀}
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝³] fun a ↦ f x₀

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderClosedTopology α
inst✝¹ : PseudoMetricSpace β
inst✝ : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst✝³] f
x₀ : β
h : Bornology.IsBounded {x | f x ≤ f x₀}
⊢ {x | f x₀ < f x} ∈ cocompact β

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
a_min : a ∈ lowerBounds {g | g ∈ H ∧ 1 < g}
a_in : a ∈ H
a_pos : 1 < a
g : G
g_in : g ∈ H
k : ℤ
right✝ : ∀ (y : ℤ), (fun k ↦ a ^ k ≤ g ∧ g < a ^ (k + 1)) y → y = k
nonneg : a ^ k ≤ g
lt : g < a ^ (k + 1)
h : ¬g / a ^ k = 1
⊢ 1 ≤ g / a ^ k

Tactic:
by

Goal state after: