awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
c : α
f : β → α
l : Filter β
rw : Tendsto (β := ℝ) (fun (x : β) ↦ dist (f x) c) l atTop ↔ Tendsto f l (comap (β := ℝ) (fun (x : α) ↦ dist x c) atTop)
rw₁ : Tendsto (β := ℝ) (fun (x : β) ↦ dist (f x) c) l atTop ↔ Tendsto (β := ℝ) ((fun (x : α) ↦ dist x c) ∘ f) l atTop
rw₂ rw₃ : Tendsto (β := ℝ) (fun (x : β) ↦ dist (f x) c) l atTop ↔ Tendsto (β := ℝ) (fun (x : β) ↦ dist (f x) c) l atTop
⊢ Tendsto (β := ℝ) (fun (x : β) ↦ dist (f x) c) l atTop ↔ Tendsto f l (cobounded α)

Tactic:
rw [← comap_dist_right_atTop c, tendsto_comap_iff, Function.comp_def]

Premises used: Metric.comap_dist_right_atTop, Filter.tendsto_comap_iff, Function.comp_def
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
c : α
f : β → α
l : Filter β
⊢ Tendsto (β := ℝ) (fun (x : β) ↦ dist c (f x)) l atTop ↔ Tendsto f l (cobounded α)

Tactic:
simp only [dist_comm c, tendsto_dist_right_atTop_iff]

Premises used: dist_comm, Metric.tendsto_dist_right_atTop_iff
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
c : α
⊢ Tendsto (β := ℝ) (fun (x : α) ↦ dist x c) (cobounded α) atTop

Tactic:
tendsto_iff_comap.2 (comap_dist_right_atTop c).ge

Premises used: Iff.mpr, Eq.ge, Metric.comap_dist_right_atTop, Filter.tendsto_iff_comap
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
c : α
⊢ Tendsto (dist c) (cobounded α) atTop

Tactic:
tendsto_iff_comap.2 (comap_dist_left_atTop c).ge

Premises used: Iff.mpr, Eq.ge, Metric.comap_dist_left_atTop, Filter.tendsto_iff_comap
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
h : TotallyBounded s
⊢ Bornology.IsBounded s

Tactic:
let ⟨_t, fint, subs⟩ := (totallyBounded_iff.mp h) 1 zero_lt_one
  ((isBounded_biUnion fint).2 fun _ _ => isBounded_ball).subset subs

Premises used: Metric.isBounded_ball, Iff.mpr, Bornology.isBounded_biUnion, Bornology.IsBounded, zero_lt_one, Bornology.IsBounded.subset, Metric.totallyBounded_iff, Iff.mp, OfNat.ofNat, _private.0.TotallyBounded.isBounded.match_1
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
h : IsCompact s
⊢ Bornology.IsBounded s

Tactic:
h.totallyBounded.isBounded

Premises used: TotallyBounded.isBounded, IsCompact.totallyBounded
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
x : α
s t : Set α
r : ℝ
inst : PseudoMetricSpace α
inst_1 : CompactSpace α
⊢ BoundedSpace α

Tactic:
⟨isCompact_univ.isBounded⟩

Premises used: IsCompact.isBounded, BoundedSpace.mk, isCompact_univ
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ cobounded α ≤ cocompact α

Tactic:
hasBasis_cocompact.ge_iff.2 fun _s hs ↦ hs.isBounded

Premises used: Iff.mpr, IsCompact.isBounded, Filter.HasBasis.ge_iff, Filter.hasBasis_cocompact
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
c : α
rw : (∃ (r : ℝ), sᶜ ⊆ closedBall c r) ↔ ∃ (r : ℝ), (closedBall c r)ᶜ ⊆ s
⊢ Bornology.IsCobounded s ↔ ∃ (r : ℝ), (closedBall c r)ᶜ ⊆ s

Tactic:
rw [← isBounded_compl_iff, isBounded_iff_subset_closedBall c]

Premises used: Bornology.isBounded_compl_iff, Metric.isBounded_iff_subset_closedBall
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
c : α
h : ∀ (a : ℝ), sᶜ ⊆ closedBall c a ↔ (closedBall c a)ᶜ ⊆ s
⊢ (∃ (r : ℝ), sᶜ ⊆ closedBall c r) ↔ ∃ (r : ℝ), (closedBall c r)ᶜ ⊆ s

Tactic:
apply exists_congr

Premises used: exists_congr
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
c : α
r : ℝ
h h₁ : (closedBall c r)ᶜ ⊆ s ↔ (closedBall c r)ᶜ ⊆ s
⊢ sᶜ ⊆ closedBall c r ↔ (closedBall c r)ᶜ ⊆ s

Tactic:
rw [compl_subset_comm]

Premises used: Set.compl_subset_comm
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
hs : Bornology.IsCobounded s
c : α
⊢ ∃ (r : ℝ), (closedBall c r)ᶜ ⊆ s

Tactic:
(isCobounded_iff_closedBall_compl_subset c).mp hs

Premises used: Iff.mp, Metric.isCobounded_iff_closedBall_compl_subset
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
hs : s ∈ cocompact α
c : α
⊢ ∃ (r : ℝ), (closedBall c r)ᶜ ⊆ s

Tactic:
IsCobounded.closedBall_compl_subset (cobounded_le_cocompact hs) c

Premises used: Bornology.IsCobounded.closedBall_compl_subset, Metric.cobounded_le_cocompact
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
c : α
h : ∃ (r : ℝ), (closedBall c r)ᶜ ⊆ s
rcases : ∀ (r : ℝ) (h : (closedBall c r)ᶜ ⊆ s), s ∈ cocompact α
⊢ s ∈ cocompact α

Tactic:
rcases h with ⟨r, h⟩
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
c : α
r : ℝ
h : (closedBall c r)ᶜ ⊆ s
rw : ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s
⊢ s ∈ cocompact α

Tactic:
rw [Filter.mem_cocompact]

Premises used: Filter.mem_cocompact
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
c : α
r : ℝ
h : (closedBall c r)ᶜ ⊆ s
⊢ ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s

Tactic:
⟨closedBall c r, isCompact_closedBall c r, h⟩

Premises used: And.intro, Exists.intro, ProperSpace.isCompact_closedBall, Metric.closedBall
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
c : α
r : ℝ
h : (closedBall c r)ᶜ ⊆ s
⊢ ∃ (t : Set α), IsCompact t ∧ tᶜ ⊆ s

Tactic:
exact ⟨closedBall c r, isCompact_closedBall c r, h⟩
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
c : α
⊢ s ∈ cocompact α ↔ ∃ (r : ℝ), (closedBall c r)ᶜ ⊆ s

Tactic:
⟨(closedBall_compl_subset_of_mem_cocompact · _), mem_cocompact_of_closedBall_compl_subset _⟩

Premises used: Metric.mem_cocompact_of_closedBall_compl_subset, Metric.closedBall_compl_subset_of_mem_cocompact, Iff.intro
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
f : β → α
⊢ (∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ range f → ∀ ⦃y : α⦄, y ∈ range f → dist x y ≤ C) ↔
    ∃ (C : ℝ), ∀ (x y : β), dist (f x) (f y) ≤ C

Tactic:
simp only [forall_mem_range]

Premises used: Set.forall_mem_range
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : 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:
simp only [forall_mem_image]

Premises used: Set.forall_mem_image
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (SProd.sprod (α := Filter β) (β := Filter β) Filter.cofinite Filter.cofinite) (𝓤 α)
rcases :
  ∀ (s : Set β) (hsf : s.Finite)
    (hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Membership.mem (γ := Set (α × α)) {p : α × α | dist p.1 p.2 < 1} (Prod.map f f x)),
    Bornology.IsBounded (range f)
⊢ Bornology.IsBounded (range f)

Tactic:
rcases (hasBasis_cofinite.prod_self.tendsto_iff uniformity_basis_dist).1 hf 1 zero_lt_one with
    ⟨s, hsf, hs1⟩

Premises used: Filter.HasBasis.tendsto_iff, Filter.HasBasis.prod_self, Filter.hasBasis_cofinite, Metric.uniformity_basis_dist, zero_lt_one, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (SProd.sprod (α := Filter β) (β := Filter β) Filter.cofinite Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Membership.mem (γ := Set (α × α)) {p : α × α | dist p.1 p.2 < 1} (Prod.map f f x)
rw : Bornology.IsBounded (f '' s ∪ f '' sᶜ)
rw₁ : Set β
⊢ Bornology.IsBounded (range f)

Tactic:
rw [← image_union_image_compl_eq_range]

Premises used: Set.image_union_image_compl_eq_range
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (SProd.sprod (α := Filter β) (β := Filter β) Filter.cofinite Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Membership.mem (γ := Set (α × α)) {p : α × α | dist p.1 p.2 < 1} (Prod.map f f x)
⊢ Bornology.IsBounded (f '' s ∪ f '' sᶜ)

Tactic:
(hsf.image f).isBounded.union (isBounded_image_iff.2 ⟨1, fun x hx y hy ↦ ?_⟩)

Premises used: Iff.mpr, Set.Finite.image, Set.Finite.isBounded, Metric.isBounded_image_iff, Exists.intro, OfNat.ofNat, Bornology.IsBounded.union
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (SProd.sprod (α := Filter β) (β := Filter β) Filter.cofinite Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Membership.mem (γ := Set (α × α)) {p : α × α | dist p.1 p.2 < 1} (Prod.map f f x)
x : β
hx : x ∈ sᶜ
y : β
hy : y ∈ sᶜ
⊢ dist (f x) (f y) ≤ 1

Tactic:
le_of_lt (hs1 (x, y) ⟨hx, hy⟩)

Premises used: le_of_lt, Prod.mk, And.intro
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (SProd.sprod (α := Filter β) (β := Filter β) Filter.cofinite Filter.cofinite) (𝓤 α)
s : Set β
hsf : s.Finite
hs1 : ∀ x ∈ sᶜ ×ˢ sᶜ, Membership.mem (γ := Set (α × α)) {p : α × α | dist p.1 p.2 < 1} (Prod.map f f x)
x : β
hx : x ∈ sᶜ
y : β
hy : y ∈ sᶜ
⊢ dist (f x) (f y) ≤ 1

Tactic:
exact le_of_lt (hs1 (x, y) ⟨hx, hy⟩)

Premises used: le_of_lt
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
f : β → α
hf : Cauchy (map f Filter.cofinite)
⊢ Bornology.IsBounded (range f)

Tactic:
isBounded_range_of_tendsto_cofinite_uniformity <| (cauchy_map_iff.1 hf).2

Premises used: cauchy_map_iff, And.right, Iff.mp, Metric.isBounded_range_of_tendsto_cofinite_uniformity
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℕ → α
hf : CauchySeq f
rwa rwa₁ rwa₂ rwa₃ : Cauchy (map f atTop)
⊢ Cauchy (map f Filter.cofinite)

Tactic:
rwa [Nat.cofinite_eq_atTop]

Premises used: Nat.cofinite_eq_atTop
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
f : β → α
a : α
hf : Tendsto f Filter.cofinite (𝓝 a)
⊢ Bornology.IsBounded (range f)

Tactic:
isBounded_range_of_tendsto_cofinite_uniformity <|
    (hf.prodMap hf).mono_right <| nhds_prod_eq.symm.trans_le (nhds_le_uniformity a)

Premises used: Eq.trans_le, nhds_le_uniformity, Metric.isBounded_range_of_tendsto_cofinite_uniformity, nhds_prod_eq, Filter.Tendsto.mono_right, Eq.symm, Filter.Tendsto.prodMap
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
inst_1 : CompactSpace α
⊢ Bornology.IsBounded s

Tactic:
isCompact_univ.isBounded.subset (subset_univ _)

Premises used: IsCompact.isBounded, Set.subset_univ, isCompact_univ, Bornology.IsBounded.subset
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
u : ℕ → α
x : α
hu : Tendsto u atTop (𝓝 x)
⊢ Bornology.IsBounded (range u)

Tactic:
hu.cauchySeq.isBounded_range

Premises used: Filter.Tendsto.cauchySeq, CauchySeq.isBounded_range
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ Disjoint (𝓝 x) (cobounded α)

Tactic:
disjoint_of_disjoint_of_mem disjoint_compl_right (ball_mem_nhds _ one_pos) isBounded_ball

Premises used: Metric.isBounded_ball, Filter.disjoint_of_disjoint_of_mem, Metric.ball_mem_nhds, disjoint_compl_right, one_pos
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ Disjoint (cobounded α) (𝓝 x)

Tactic:
(disjoint_nhds_cobounded x).symm

Premises used: Metric.disjoint_nhds_cobounded, Disjoint.symm
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
hs : IsCompact s
⊢ Disjoint (𝓝ˢ s) (cobounded α)

Tactic:
hs.disjoint_nhdsSet_left.2 fun _ _ ↦ disjoint_nhds_cobounded _

Premises used: Iff.mpr, Metric.disjoint_nhds_cobounded, IsCompact.disjoint_nhdsSet_left
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
hs : IsCompact s
⊢ Disjoint (cobounded α) (𝓝ˢ s)

Tactic:
(disjoint_nhdsSet_cobounded hs).symm

Premises used: Disjoint.symm, Metric.disjoint_nhdsSet_cobounded
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u_3
β : Type u_4
inst : PseudoMetricSpace β
l : Filter α
f : α → β
x : β
hf : Tendsto f l (𝓝 x)
⊢ ∃ s ∈ l, Bornology.IsBounded (f '' s)

Tactic:
(l.basis_sets.map f).disjoint_iff_left.mp <| (disjoint_nhds_cobounded x).mono_left hf

Premises used: Set.Mem, Metric.disjoint_nhds_cobounded, setOf, Bornology.IsBounded, Filter.HasBasis.map, Filter.basis_sets, Disjoint.mono_left, Filter.HasBasis.disjoint_iff_left, Iff.mp, Bornology.IsCobounded
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
rw : ∀ x ∈ k, Disjoint (𝓝 x) (comap f (cobounded α) ⊓ 𝓟 s)
⊢ Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))

Tactic:
rw [disjoint_assoc, inf_comm, hk.disjoint_nhdsSet_left]

Premises used: IsCompact.disjoint_nhdsSet_left, disjoint_assoc, inf_comm
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
⊢ ∀ x ∈ k, Disjoint (𝓝 x) (comap f (cobounded α) ⊓ 𝓟 s)

Tactic:
fun x hx ↦ disjoint_left_comm.2 <|
      tendsto_comap.disjoint (disjoint_cobounded_nhds _) (hf x hx)

Premises used: Iff.mpr, disjoint_left_comm, Filter.Tendsto.disjoint, Filter.tendsto_comap, Metric.disjoint_cobounded_nhds
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
⊢ ∀ x ∈ k, Disjoint (𝓝 x) (comap f (cobounded α) ⊓ 𝓟 s)

Tactic:
exact fun x hx ↦ disjoint_left_comm.2 <|
      tendsto_comap.disjoint (disjoint_cobounded_nhds _) (hf x hx)

Premises used: Iff.mpr, disjoint_left_comm, Filter.Tendsto.disjoint, Filter.tendsto_comap, Metric.disjoint_cobounded_nhds
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
⊢ Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))

Tactic:
have : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α)) := by
    rw [disjoint_assoc, inf_comm, hk.disjoint_nhdsSet_left]
    exact fun x hx ↦ disjoint_left_comm.2 <|
      tendsto_comap.disjoint (disjoint_cobounded_nhds _) (hf x hx)
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
rcases :
  ∀ (U : Set β) (hUo : IsOpen[inst_1] U) (hkU : k ⊆ U) (t : Set α) (ht : t ∈ cobounded α)
    (hd : Disjoint (U ∩ s) (f ⁻¹' id t)), ∃ (t : Set β), k ⊆ t ∧ IsOpen[inst_1] t ∧ Bornology.IsBounded (f '' (t ∩ s))
⊢ ∃ (t : Set β), k ⊆ t ∧ IsOpen[inst_1] t ∧ Bornology.IsBounded (f '' (t ∩ s))

Tactic:
rcases ((((hasBasis_nhdsSet _).inf_principal _)).disjoint_iff ((basis_sets _).comap _)).1 this
    with ⟨U, ⟨hUo, hkU⟩, t, ht, hd⟩

Premises used: hasBasis_nhdsSet, Filter.HasBasis.disjoint_iff, Filter.HasBasis.comap, Filter.basis_sets, Iff.mp, Filter.HasBasis.inf_principal
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
U : Set β
hUo : IsOpen[inst_1] U
hkU : k ⊆ U
t : Set α
ht : t ∈ cobounded α
hd : Disjoint (U ∩ s) (f ⁻¹' id t)
⊢ ∃ (t : Set β), k ⊆ t ∧ IsOpen[inst_1] t ∧ Bornology.IsBounded (f '' (t ∩ s))

Tactic:
⟨U, hkU, hUo, (isBounded_compl_iff.2 ht).subset ?_⟩

Premises used: Iff.mpr, Bornology.isBounded_compl_iff, Bornology.IsBounded.subset, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
U : Set β
hUo : IsOpen[inst_1] U
hkU : k ⊆ U
t : Set α
ht : t ∈ cobounded α
hd : Disjoint (U ∩ s) (f ⁻¹' id t)
refine : f '' (U ∩ s) ⊆ tᶜ
⊢ ∃ (t : Set β), k ⊆ t ∧ IsOpen[inst_1] t ∧ Bornology.IsBounded (f '' (t ∩ s))

Tactic:
refine ⟨U, hkU, hUo, (isBounded_compl_iff.2 ht).subset ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
U : Set β
hUo : IsOpen[inst_1] U
hkU : k ⊆ U
t : Set α
ht : t ∈ cobounded α
hd : Disjoint (U ∩ s) (f ⁻¹' id t)
rwa : U ∩ s ⊆ f ⁻¹' tᶜ
rwa₁ : U ∩ s ⊆ (f ⁻¹' t)ᶜ
rwa₂ rwa₃ rwa₄ rwa₅ : Disjoint (U ∩ s) (f ⁻¹' t)
⊢ f '' (U ∩ s) ⊆ tᶜ

Tactic:
rwa [image_subset_iff, preimage_compl, subset_compl_iff_disjoint_right]

Premises used: Set.subset_compl_iff_disjoint_right, Set.image_subset_iff, Set.preimage_compl
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousAt f x
⊢ ∀ x ∈ k, ContinuousWithinAt f univ x

Tactic:
simp_rw [← continuousWithinAt_univ] at hf

Premises used: continuousWithinAt_univ
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f univ x
⊢ ∃ (t : Set β), k ⊆ t ∧ IsOpen[inst_1] t ∧ Bornology.IsBounded (f '' t)

Tactic:
simpa only [inter_univ] using
    exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt hk hf

Premises used: Set.inter_univ, Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hks : k ⊆ s
hf : ContinuousOn f s
⊢ ∃ (t : Set β), k ⊆ t ∧ IsOpen[inst_1] t ∧ Bornology.IsBounded (f '' (t ∩ s))

Tactic:
exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt hk fun x hx =>
    hf x (hks hx)

Premises used: Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hs : IsOpen[inst_1] s
hks : k ⊆ s
hf : ContinuousOn f s
⊢ ∃ (t : Set β), k ⊆ t ∧ IsOpen[inst_1] t ∧ Bornology.IsBounded (f '' t)

Tactic:
exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt hk fun _x hx =>
    hf.continuousAt (hs.mem_nhds (hks hx))

Premises used: IsOpen.mem_nhds, Metric.exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt, ContinuousOn.continuousAt
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
hc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hb : Bornology.IsBounded s
inl :
  ∀ (hc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅) (hb : Bornology.IsBounded.{u} (α := α) ∅),
    IsCompact.{u} (X := α) ∅
inr : ∀ (x : α), IsCompact s
⊢ IsCompact s

Tactic:
rcases eq_empty_or_nonempty s with (rfl | ⟨x, -⟩)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
hc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
hb : Bornology.IsBounded.{u} (α := α) ∅
⊢ IsCompact.{u} (X := α) ∅

Tactic:
isCompact_empty

Premises used: isCompact_empty
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
hc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
hb : Bornology.IsBounded.{u} (α := α) ∅
⊢ IsCompact.{u} (X := α) ∅

Tactic:
exact isCompact_empty

Premises used: isCompact_empty
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
hc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hb : Bornology.IsBounded s
x : α
inr : ∀ (r : ℝ) (hr : s ⊆ closedBall x r), IsCompact s
⊢ IsCompact s

Tactic:
rcases hb.subset_closedBall x with ⟨r, hr⟩

Premises used: Bornology.IsBounded.subset_closedBall
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
hc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hb : Bornology.IsBounded s
x : α
r : ℝ
hr : s ⊆ closedBall x r
⊢ IsCompact s

Tactic:
(isCompact_closedBall x r).of_isClosed_subset hc hr

Premises used: IsCompact.of_isClosed_subset, ProperSpace.isCompact_closedBall
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
hc : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hb : Bornology.IsBounded s
x : α
r : ℝ
hr : s ⊆ closedBall x r
⊢ IsCompact s

Tactic:
exact (isCompact_closedBall x r).of_isClosed_subset hc hr

Premises used: IsCompact.of_isClosed_subset, ProperSpace.isCompact_closedBall
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
h : Bornology.IsBounded s
⊢ IsCompact (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s)

Tactic:
isCompact_of_isClosed_isBounded isClosed_closure h.closure

Premises used: Metric.isCompact_of_isClosed_isBounded, isClosed_closure, Bornology.IsBounded.closure
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
s : Set α
inst : PseudoMetricSpace α
inst_1 : T2Space α
inst_2 : ProperSpace α
⊢ IsCompact s ↔ IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s ∧ Bornology.IsBounded s

Tactic:
⟨fun h => ⟨h.isClosed, h.isBounded⟩, fun h => isCompact_of_isClosed_isBounded h.1 h.2⟩

Premises used: IsCompact.isBounded, Metric.isCompact_of_isClosed_isBounded, And.right, And.left, And.intro, Iff.intro, IsCompact.isClosed
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : ProperSpace α
⊢ CompactSpace α ↔ Bornology.IsBounded.{u} (α := α) univ

Tactic:
⟨@isBounded_of_compactSpace α _ _, fun hb => ⟨isCompact_of_isClosed_isBounded isClosed_univ hb⟩⟩

Premises used: isClosed_univ, Metric.isCompact_of_isClosed_isBounded, CompactSpace.mk, Metric.isBounded_of_compactSpace, Iff.intro
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : Preorder α
inst_2 : CompactIccSpace α
a b : α
⊢ Bornology.IsBounded (Icc a b)

Tactic:
(totallyBounded_Icc a b).isBounded

Premises used: TotallyBounded.isBounded, totallyBounded_Icc
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : Preorder α
inst_2 : CompactIccSpace α
a b : α
⊢ Bornology.IsBounded (Ico a b)

Tactic:
(totallyBounded_Ico a b).isBounded

Premises used: TotallyBounded.isBounded, totallyBounded_Ico
-- Module: Mathlib.Topology.MetricSpace.Bounded
Goal:
α : Type u
inst : PseudoMetricSpace α
inst_1 : Preorder α
inst_2 : CompactIccSpace α
a b : α
⊢ Bornology.IsBounded (Ioc a b)

Tactic:
(totallyBounded_Ioc a b).isBounded

Premises used: TotallyBounded.isBounded, totallyBounded_Ioc