awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : 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 : ℕ), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
h' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (s n)) atTop (𝓝 0)
u : (N : ℕ) → α := fun (N : ℕ) ↦ ⋯.some (s := ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
⊢ ∃ x ∈ s 0, Tendsto (fun (n : ℕ) ↦ u n) atTop (𝓝 x)

Tactic:
cauchySeq_tendsto_of_isComplete h0 (fun n => I 0 n zero_le) this

Premises used: zero_le, cauchySeq_tendsto_of_isComplete, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : 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 : ℕ), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
h' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (s n)) atTop (𝓝 0)
u : (N : ℕ) → α := fun (N : ℕ) ↦ ⋯.some (s := ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
obtain : ∀ (x : α) (xlim : Tendsto (fun (n : ℕ) ↦ u n) atTop (𝓝 x)), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), s n)
⊢ Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), s n)

Tactic:
obtain ⟨x, -, xlim⟩ : ∃ x ∈ s 0, Tendsto (fun n : ℕ => u n) atTop (𝓝 x) :=
    cauchySeq_tendsto_of_isComplete h0 (fun n => I 0 n zero_le) this

Premises used: zero_le, cauchySeq_tendsto_of_isComplete, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : 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 : ℕ), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
h' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (s n)) atTop (𝓝 0)
u : (N : ℕ) → α := fun (N : ℕ) ↦ ⋯.some (s := ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun (n : ℕ) ↦ u n) atTop (𝓝 x)
⊢ Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), s n)

Tactic:
⟨x, mem_iInter.2 fun n => ?_⟩

Premises used: Iff.mpr, Set.mem_iInter, Set.Nonempty, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : 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 : ℕ), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
h' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (s n)) atTop (𝓝 0)
u : (N : ℕ) → α := fun (N : ℕ) ↦ ⋯.some (s := ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun (n : ℕ) ↦ u n) atTop (𝓝 x)
refine : ∀ (n : ℕ), x ∈ s n
⊢ Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), s n)

Tactic:
refine ⟨x, mem_iInter.2 fun n => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : 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 : ℕ), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
h' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (s n)) atTop (𝓝 0)
u : (N : ℕ) → α := fun (N : ℕ) ↦ ⋯.some (s := ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun (n : ℕ) ↦ u n) atTop (𝓝 x)
n : ℕ
apply : ∀ᶠ (x : ℕ) in atTop, u x ∈ s n
⊢ x ∈ s n

Tactic:
apply (hs n).mem_of_tendsto xlim

Premises used: IsClosed.mem_of_tendsto
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : 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 : ℕ), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
h' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (s n)) atTop (𝓝 0)
u : (N : ℕ) → α := fun (N : ℕ) ↦ ⋯.some (s := ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun (n : ℕ) ↦ u n) atTop (𝓝 x)
n : ℕ
h₁ : ∀ (p : ℕ) (hp : p ∈ Ici n), u p ∈ s n
⊢ ∀ᶠ (x : ℕ) in atTop, u x ∈ s n

Tactic:
filter_upwards [Ici_mem_atTop n] with p hp

Premises used: Filter.Ici_mem_atTop
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : 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 : ℕ), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
h' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (s n)) atTop (𝓝 0)
u : (N : ℕ) → α := fun (N : ℕ) ↦ ⋯.some (s := ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun (n : ℕ) ↦ u n) atTop (𝓝 x)
n p : ℕ
hp : p ∈ Ici n
⊢ u p ∈ s n

Tactic:
I n p hp
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : 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 : ℕ), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
h' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (s n)) atTop (𝓝 0)
u : (N : ℕ) → α := fun (N : ℕ) ↦ ⋯.some (s := ⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
I : ∀ (n N : ℕ), n ≤ N → u N ∈ s n
this : CauchySeq u
x : α
xlim : Tendsto (fun (n : ℕ) ↦ u n) atTop (𝓝 x)
n p : ℕ
hp : p ∈ Ici n
⊢ u p ∈ s n

Tactic:
exact I n p hp
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : CompleteSpace α
s : ℕ → Set α
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), ⋂ (_ : n ≤ N), s n)
h' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ diam (s n)) atTop (𝓝 0)
⊢ Set.Nonempty.{u} (α := α) (⋂ (n : ℕ), s n)

Tactic:
(hs 0).isComplete.nonempty_iInter_of_nonempty_biInter hs h's h h'

Premises used: IsClosed.isComplete, OfNat.ofNat, IsComplete.nonempty_iInter_of_nonempty_biInter
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : MetricSpace α
hs1 : s.Nontrivial
hs2 : Bornology.IsBounded s
rcases : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s) (hxy : x ≠ y), 0 < diam s
⊢ 0 < diam s

Tactic:
rcases hs1 with ⟨x, hx, y, hy, hxy⟩
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : MetricSpace α
hs2 : Bornology.IsBounded s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ 0 < diam s

Tactic:
(dist_pos.mpr hxy).trans_le <| Metric.dist_le_diam_of_mem hs2 hx hy

Premises used: Iff.mpr, Metric.dist_le_diam_of_mem, dist_pos, LT.lt.trans_le
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : MetricSpace α
hs2 : Bornology.IsBounded s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≠ y
⊢ 0 < diam s

Tactic:
exact (dist_pos.mpr hxy).trans_le <| Metric.dist_le_diam_of_mem hs2 hx hy

Premises used: Iff.mpr, Metric.dist_le_diam_of_mem, dist_pos, LT.lt.trans_le
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
h : Nontrivial α
inhabit : ∀ (inhabited_h : Inhabited α), cobounded α = cocompact α
⊢ cobounded α = cocompact α

Tactic:
inhabit α
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
h : Nontrivial α
inhabited_h : Inhabited α
⊢ cobounded α = cocompact α

Tactic:
cobounded_le_cocompact.antisymm <| (hasBasis_cobounded_compl_closedBall default).ge_iff.2
    fun _ _ ↦ (isCompact_closedBall _ _).compl_mem_cocompact

Premises used: Metric.hasBasis_cobounded_compl_closedBall, Iff.mpr, Inhabited.default, IsCompact.compl_mem_cocompact, Metric.cobounded_le_cocompact, LE.le.antisymm, Filter.HasBasis.ge_iff, ProperSpace.isCompact_closedBall
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
h : Nontrivial α
inhabited_h : Inhabited α
⊢ cobounded α = cocompact α

Tactic:
exact cobounded_le_cocompact.antisymm <| (hasBasis_cobounded_compl_closedBall default).ge_iff.2
    fun _ _ ↦ (isCompact_closedBall _ _).compl_mem_cocompact

Premises used: Metric.hasBasis_cobounded_compl_closedBall, Iff.mpr, Inhabited.default, IsCompact.compl_mem_cocompact, Metric.cobounded_le_cocompact, LE.le.antisymm, Filter.HasBasis.ge_iff, ProperSpace.isCompact_closedBall
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
⊢ Tendsto (β := ℝ) (fun (x_1 : α) ↦ dist x_1 x) (cocompact α) atTop

Tactic:
(tendsto_dist_right_cobounded_atTop x).mono_left cobounded_eq_cocompact.ge

Premises used: Eq.ge, Metric.tendsto_dist_right_cobounded_atTop, Metric.cobounded_eq_cocompact, Filter.Tendsto.mono_left
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
⊢ Tendsto (dist x) (cocompact α) atTop

Tactic:
(tendsto_dist_left_cobounded_atTop x).mono_left cobounded_eq_cocompact.ge

Premises used: Eq.ge, Metric.tendsto_dist_left_cobounded_atTop, Metric.cobounded_eq_cocompact, Filter.Tendsto.mono_left
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
x : α
⊢ comap (dist x) atTop = cocompact α

Tactic:
simp [cobounded_eq_cocompact]

Premises used: Metric.cobounded_eq_cocompact
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
f : β → α
l : Filter β
x : α
h : Tendsto (β := ℝ) (fun (y : β) ↦ dist (f y) x) l atTop
⊢ Tendsto f l (cocompact α)

Tactic:
((tendsto_dist_right_atTop_iff _).1 h).mono_right cobounded_le_cocompact

Premises used: Metric.cobounded_le_cocompact, Iff.mp, Filter.Tendsto.mono_right, Metric.tendsto_dist_right_atTop_iff
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
K s : Set α
hsd : IsDiscrete s
hK : Bornology.IsBounded K
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ (K ∩ s).Finite

Tactic:
(IsCompact.finite ?_ ?_).subset (Set.inter_subset_inter_left s subset_closure)

Premises used: subset_closure, Set.Finite.subset, Set.inter_subset_inter_left, IsCompact.finite
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
K s : Set α
hsd : IsDiscrete s
hK : Bornology.IsBounded K
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
refine_1 : IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩ s)
refine_2 : IsDiscrete (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩ s)
⊢ (K ∩ s).Finite

Tactic:
refine (IsCompact.finite ?_ ?_).subset (Set.inter_subset_inter_left s subset_closure)

Premises used: subset_closure, Set.Finite.subset, Set.inter_subset_inter_left, IsCompact.finite
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
K s : Set α
hsd : IsDiscrete s
hK : Bornology.IsBounded K
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩ s)

Tactic:
hK.isCompact_closure.inter_right hs

Premises used: Bornology.IsBounded.isCompact_closure, IsCompact.inter_right
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
K s : Set α
hsd : IsDiscrete s
hK : Bornology.IsBounded K
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩ s)

Tactic:
exact hK.isCompact_closure.inter_right hs

Premises used: Bornology.IsBounded.isCompact_closure, IsCompact.inter_right
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
K s : Set α
hsd : IsDiscrete s
hK : Bornology.IsBounded K
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsDiscrete (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩ s)

Tactic:
hsd.mono Set.inter_subset_right

Premises used: IsDiscrete.mono, Set.inter_subset_right
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
K s : Set α
hsd : IsDiscrete s
hK : Bornology.IsBounded K
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ IsDiscrete (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K ∩ s)

Tactic:
exact hsd.mono Set.inter_subset_right

Premises used: IsDiscrete.mono, Set.inter_subset_right
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : PseudoMetricSpace β
inst_4 : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f
x₀ : β
h : Bornology.IsBounded.{u_4} (α := β) {x : β | f x ≤ f x₀}
⊢ ∃ (x : β), ∀ (y : β), f x ≤ f y

Tactic:
hf.exists_forall_le' (x₀ := x₀) ?_

Premises used: Continuous.exists_forall_le'
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : PseudoMetricSpace β
inst_4 : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f
x₀ : β
h : Bornology.IsBounded.{u_4} (α := β) {x : β | f x ≤ f x₀}
refine : ∀ᶠ (x : β) in cocompact β, f x₀ ≤ f x
⊢ ∃ (x : β), ∀ (y : β), f x ≤ f y

Tactic:
refine hf.exists_forall_le' (x₀ := x₀) ?_

Premises used: Continuous.exists_forall_le'
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : PseudoMetricSpace β
inst_4 : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f
x₀ : β
h : Bornology.IsBounded.{u_4} (α := β) {x : β | f x ≤ f x₀}
⊢ {x : β | f x₀ < f x} ∈ cocompact β

Tactic:
Filter.mem_cocompact'.mpr ⟨_, ?_, fun ⦃_⦄ a ↦ a⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Filter.mem_cocompact'
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : PseudoMetricSpace β
inst_4 : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f
x₀ : β
h : Bornology.IsBounded.{u_4} (α := β) {x : β | f x ≤ f x₀}
refine : IsCompact.{u_4} (X := β) {x : β | f x₀ < f x}ᶜ
⊢ {x : β | f x₀ < f x} ∈ cocompact β

Tactic:
refine Filter.mem_cocompact'.mpr ⟨_, ?_, fun ⦃_⦄ a ↦ a⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Filter.mem_cocompact'
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : PseudoMetricSpace β
inst_4 : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f
x₀ : β
h : Bornology.IsBounded.{u_4} (α := β) {x : β | f x ≤ f x₀}
simp : IsCompact.{u_4} (X := β) {a : β | f a ≤ f x₀}
⊢ IsCompact.{u_4} (X := β) {x : β | f x₀ < f x}ᶜ

Tactic:
simp only [Set.compl_setOf, not_lt]

Premises used: not_lt, Set.compl_setOf
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : PseudoMetricSpace β
inst_4 : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f
x₀ : β
h : Bornology.IsBounded.{u_4} (α := β) {x : β | f x ≤ f x₀}
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : PseudoMetricSpace β
inst_4 : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f
x₀ : β
h : Bornology.IsBounded.{u_4} (α := β) {x : β | f x ≤ f x₀}
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] fun (a : β) ↦ f x₀

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : PseudoMetricSpace β
inst_4 : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f
x₀ : β
h : Bornology.IsBounded.{u_4} (α := β) {x : β | f x ≤ f x₀}
⊢ IsCompact.{u_4} (X := β) {a : β | f a ≤ f x₀}

Tactic:
exact Metric.isCompact_of_isClosed_isBounded (isClosed_le (by fun_prop) (by fun_prop)) h

Premises used: Metric.isCompact_of_isClosed_isBounded, isClosed_le
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : PseudoMetricSpace β
inst_4 : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f
x₀ : β
h : Bornology.IsBounded.{u_4} (α := β) {x : β | f x ≤ f x₀}
⊢ {x : β | f x₀ < f x} ∈ cocompact β

Tactic:
have hU : {x : β | f x₀ < f x} ∈ Filter.cocompact β := by
    refine Filter.mem_cocompact'.mpr ⟨_, ?_, fun ⦃_⦄ a ↦ a⟩
    simp only [Set.compl_setOf, not_lt]
    exact Metric.isCompact_of_isClosed_isBounded (isClosed_le (by fun_prop) (by fun_prop)) h
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : PseudoMetricSpace β
inst_4 : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f
x₀ : β
h : Bornology.IsBounded.{u_4} (α := β) {x : β | f x ≤ f x₀}
hU : {x : β | f x₀ < f x} ∈ cocompact β
x : β
hx : f x₀ < f x
⊢ f x₀ ≤ f x

Tactic:
hx.le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : PseudoMetricSpace β
inst_4 : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f
x₀ : β
h : Bornology.IsBounded.{u_4} (α := β) {x : β | f x ≤ f x₀}
hU : {x : β | f x₀ < f x} ∈ cocompact β
h₁ :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | f x₀ < f x} x →
          Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ f x₀ ≤ f x) x} x}
      a
h₂ h₃ : ∀ (x : β) (hx : f x₀ < f x), f x₀ ≤ f x
⊢ ∀ᶠ (x : β) in cocompact β, f x₀ ≤ f x

Tactic:
filter_upwards [hU] with x hx using hx.le
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
inst_3 : PseudoMetricSpace β
inst_4 : ProperSpace β
f : β → α
hf : Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, inst_1] f
x₀ : β
h : Bornology.IsBounded.{u_4} (α := β) {x : β | f x₀ ≤ f x}
⊢ ∃ (x : β), ∀ (y : β), f y ≤ f x

Tactic:
hf.exists_forall_le_of_isBounded (α := αᵒᵈ) x₀ h

Premises used: Continuous.exists_forall_le_of_isBounded
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : Add R
inst_2 : LE R
d x : PseudoMetric X R
⊢ ∀ ⦃a₂ : PseudoMetric X R⦄, x.toFun = a₂.toFun → x = a₂

Tactic:
aesop
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : Add R
inst_2 : LE R
d : X → X → R
refl : ∀ (x : X), d x x = 0
symm : ∀ (x y : X), d x y = d y x
triangle : ∀ (x y z : X), d x z ≤ d x y + d y z
⊢ (⇑{ toFun := d, refl' := refl, symm' := symm, triangle' := triangle : PseudoMetric X R } : (a : X) → X → R) = d

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : Add R
inst_2 : LE R
d : X → X → R
refl : ∀ (x : X), d x x = 0
symm : ∀ (x y : X), d x y = d y x
triangle : ∀ (x y z : X), d x z ≤ d x y + d y z
x y : X
⊢ ({ toFun := d, refl' := refl, symm' := symm, triangle' := triangle : PseudoMetric X R } : (a : X) → X → R) x y = d x y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : Add R
inst_2 : LE R
d : PseudoMetric X R
x : X
⊢ Eq.{u_2 + 1} (α := R) ((d : (a : X) → X → R) x x : R) (0 : R)

Tactic:
d.refl' x

Premises used: PseudoMetric.refl'
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : Add R
inst_2 : LE R
d : PseudoMetric X R
x y : X
⊢ Eq.{u_2 + 1} (α := R) ((d : (a : X) → X → R) x y : R) ((d : (a : X) → X → R) y x : R)

Tactic:
d.symm' x y

Premises used: PseudoMetric.symm'
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : Add R
inst_2 : LE R
d : PseudoMetric X R
x y z : X
⊢ (d : (a : X) → X → R) x z ≤
    HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y : R) ((d : (a : X) → X → R) y z : R)

Tactic:
d.triangle' x y z

Premises used: PseudoMetric.triangle'
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : Zero R
inst_1 : Add R
inst_2 : LE R
d d' : PseudoMetric X R
⊢ LE.le (α := (a : X) → X → R) (⇑d : (a : X) → X → R) (⇑d' : (a : X) → X → R) ↔ d ≤ d'

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : Preorder R
x x_1 x_2 : X
⊢ 0 x x_2 ≤ HAdd.hAdd (α := R) (0 x x_1) (0 x_1 x_2)

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : Preorder R
⊢ Eq (α := (a : X) → X → R) (⇑⊥ : (a : X) → X → R) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : Preorder R
x y : X
⊢ Eq.{u_2 + 1} (α := R) ((⊥ : (a : X) → X → R) x y : R) (0 : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : SemilatticeSup R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
d d' : PseudoMetric X R
x : X
⊢ Eq.{u_2 + 1} (α := R) ((d : (a : X) → X → R) x x ⊔ (d' : (a : X) → X → R) x x : R) (0 : R)

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : SemilatticeSup R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
d d' : PseudoMetric X R
x y : X
⊢ Eq.{u_2 + 1} (α := R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
    ((d : (a : X) → X → R) y x ⊔ (d' : (a : X) → X → R) y x : R)

Tactic:
simp [d.symm, d'.symm]

Premises used: PseudoMetric.symm
-- Module: Mathlib.Topology.MetricSpace.BundledFun
Goal:
X : Type u_1
R : Type u_2
inst : AddZeroClass R
inst_1 : SemilatticeSup R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
d d' : PseudoMetric X R
x y z : X
simp :
  (d : (a : X) → X → R) x z ≤
      HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
        ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R) ∧
    (d' : (a : X) → X → R) x z ≤
      HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
        ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R)
⊢ (d : (a : X) → X → R) x z ⊔ (d' : (a : X) → X → R) x z ≤
    HAdd.hAdd (α := R) (β := R) ((d : (a : X) → X → R) x y ⊔ (d' : (a : X) → X → R) x y : R)
      ((d : (a : X) → X → R) y z ⊔ (d' : (a : X) → X → R) y z : R)

Tactic:
simp only [sup_le_iff]

Premises used: sup_le_iff