awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Bornology G₀
inst_2 : MulAction G₀ α
t : Set α
ι : Type u_3
I : Set ι
hI : I.Finite
s : ι → Set α
⊢ Absorbs G₀ (⋂ i ∈ I, s i) t ↔ ∀ i ∈ I, Absorbs G₀ (s i) t

Tactic:
biInter_mem (f := absorbing G₀ t) hI

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.biInter_mem, Absorbs
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
G₀ : Type u_1
inst : GroupWithZero G₀
inst_1 : Bornology G₀
inst_2 : (cobounded G₀).NeBot
E : Type u_3
inst_3 : AddMonoid E
inst_4 : DistribMulAction G₀ E
s : Set E
⊢ Absorbs G₀ s 0 ↔ 0 ∈ s

Tactic:
simp only [absorbs_iff_eventually_cobounded_mapsTo, ← singleton_zero,
    mapsTo_singleton, smul_zero, eventually_const]

Premises used: smul_zero, absorbs_iff_eventually_cobounded_mapsTo, Filter.eventually_const, Set.singleton_zero, Set.mapsTo_singleton
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
E : Type u_2
inst : Monoid M
inst_1 : AddGroup E
inst_2 : DistribMulAction M E
inst_3 : Bornology M
s t : Set E
⊢ Absorbs M (-s) (-t) ↔ Absorbs M s t

Tactic:
simp [Absorbs]

Premises used: Absorbs
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
E : Type u_2
inst : Monoid M
inst_1 : AddGroup E
inst_2 : DistribMulAction M E
inst_3 : Bornology M
s₁ s₂ t₁ t₂ : Set E
h₁ : Absorbs M s₁ t₁
h₂ : Absorbs M s₂ t₂
⊢ Absorbs M (s₁ - s₂) (t₁ - t₂)

Tactic:
simpa only [sub_eq_add_neg] using h₁.add h₂.neg_neg

Premises used: sub_eq_add_neg, Absorbs.add, Absorbs.neg_neg
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s t : Set α
ht : Absorbent M s
hsub : s ⊆ t
⊢ Absorbent M t

Tactic:
fun x ↦
  (ht x).mono_left hsub

Premises used: Absorbs.mono_left, Absorbent
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s : Set α
⊢ Absorbent M s ↔ ∀ (x : α), Absorbs M s {x}

Tactic:
.rfl

Premises used: Iff.rfl, Absorbent
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s : Set α
hs : Absorbent M s
x : α
⊢ Absorbs M s {x}

Tactic:
hs x
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s t : Set α
hs : Absorbent M s
ht : t.Finite
rw : Absorbs M s (⋃ x ∈ t, {x})
⊢ Absorbs M s t

Tactic:
rw [← Set.biUnion_of_singleton t]

Premises used: Set.biUnion_of_singleton
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s t : Set α
hs : Absorbent M s
ht : t.Finite
⊢ Absorbs M s (⋃ x ∈ t, {x})

Tactic:
.biUnion ht fun _ _ => hs.absorbs

Premises used: Absorbent.absorbs, Absorbs.biUnion
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
α : Type u_2
inst : Bornology M
inst_1 : SMul M α
s t : Set α
hs : Absorbent M s
ht : t.Finite
⊢ Absorbs M s (⋃ x ∈ t, {x})

Tactic:
exact .biUnion ht fun _ _ => hs.absorbs
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
E : Type u_2
inst : Bornology M
inst_1 : AddZeroClass E
inst_2 : DistribSMul M E
s₁ s₂ t : Set E
x : E
h₁ : Absorbent M s₁
h₂ : Absorbs M s₂ t
rw : Absorbs M (s₁ + s₂) (HVAdd.hVAdd (α := Set E) {x} t)
⊢ Absorbs M (s₁ + s₂) (x +ᵥ t)

Tactic:
rw [← singleton_vadd]

Premises used: Set.singleton_vadd
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
E : Type u_2
inst : Bornology M
inst_1 : AddZeroClass E
inst_2 : DistribSMul M E
s₁ s₂ t : Set E
x : E
h₁ : Absorbent M s₁
h₂ : Absorbs M s₂ t
⊢ Absorbs M (s₁ + s₂) (HVAdd.hVAdd (α := Set E) {x} t)

Tactic:
(h₁ x).add h₂

Premises used: Absorbs.add
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
E : Type u_2
inst : Bornology M
inst_1 : AddZeroClass E
inst_2 : DistribSMul M E
s₁ s₂ t : Set E
x : E
h₁ : Absorbent M s₁
h₂ : Absorbs M s₂ t
⊢ Absorbs M (s₁ + s₂) (HVAdd.hVAdd (α := Set E) {x} t)

Tactic:
exact (h₁ x).add h₂

Premises used: Absorbs.add
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Bornology G₀
inst_2 : MulAction G₀ α
⊢ Absorbent.{u_1, u_2} G₀ (α := α) univ

Tactic:
fun _ ↦ .univ

Premises used: Absorbent, Absorbs.univ
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
G₀ : Type u_1
α : Type u_2
inst : GroupWithZero G₀
inst_1 : Bornology G₀
inst_2 : MulAction G₀ α
s : Set α
x : α
⊢ Absorbs G₀ s {x} ↔ ∀ᶠ (c : G₀) in cobounded G₀, c⁻¹ • x ∈ s

Tactic:
simp only [absorbs_iff_eventually_cobounded_mapsTo, mapsTo_singleton]

Premises used: absorbs_iff_eventually_cobounded_mapsTo, Set.mapsTo_singleton
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
G₀ : Type u_1
E : Type u_3
inst : GroupWithZero G₀
inst_1 : Bornology G₀
inst_2 : (cobounded G₀).NeBot
inst_3 : AddMonoid E
inst_4 : DistribMulAction G₀ E
s : Set E
hs : Absorbent G₀ s
⊢ 0 ∈ s

Tactic:
absorbs_zero_iff.1 (hs 0)

Premises used: absorbs_zero_iff, Iff.mp, OfNat.ofNat
-- Module: Mathlib.Topology.Bornology.Absorbs
Goal:
M : Type u_1
N : Type u_2
α : Type u_3
inst : Monoid N
inst_1 : SMul M N
inst_2 : SMul M α
inst_3 : MulAction N α
inst_4 : IsScalarTower M N α
inst_5 : Bornology M
inst_6 : Bornology N
s t : Set α
h : Absorbs N s t
hbdd : Tendsto (fun (x : M) ↦ HSMul.hSMul (β := N) x 1) (cobounded M) (cobounded N)
x : M
hx : t ⊆ HSMul.hSMul (β := N) x 1 • s
rwa rwa₁ rwa₂ rwa₃ : ∀ (hx : t ⊆ x • s), t ⊆ x • s
⊢ t ⊆ x • s

Tactic:
rwa [smul_one_smul N x s] at hx

Premises used: smul_one_smul
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
t t' : Bornology α
h_cobounded : cobounded α = cobounded α
mk :
  ∀ (cobounded : Filter α) (le_cofinite : cobounded ≤ cofinite)
    (h_cobounded : Bornology.cobounded α = Bornology.cobounded α),
    { cobounded := cobounded, le_cofinite := le_cofinite : Bornology α } = t'
⊢ t = t'

Tactic:
cases t
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
t' : Bornology α
cobounded : Filter α
le_cofinite : cobounded ≤ cofinite
h_cobounded : Bornology.cobounded α = Bornology.cobounded α
mk :
  ∀ (cobounded_1 : Filter α) (le_cofinite_1 : cobounded_1 ≤ cofinite)
    (h_cobounded : Bornology.cobounded α = Bornology.cobounded α),
    { cobounded := cobounded, le_cofinite := le_cofinite : Bornology α } =
      { cobounded := cobounded_1, le_cofinite := le_cofinite_1 }
⊢ { cobounded := cobounded, le_cofinite := le_cofinite : Bornology α } = t'

Tactic:
cases t'
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
cobounded : Filter α
le_cofinite : cobounded ≤ cofinite
cobounded_1 : Filter α
le_cofinite_1 : cobounded_1 ≤ cofinite
h_cobounded : Bornology.cobounded α = Bornology.cobounded α
⊢ { cobounded := cobounded, le_cofinite := le_cofinite : Bornology α } =
    { cobounded := cobounded_1, le_cofinite := le_cofinite_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
singleton_mem : ∀ (x : α), {x} ∈ B
⊢ comk (fun (x : Set α) ↦ x ∈ B) empty_mem subset_mem union_mem ≤ cofinite

Tactic:
simpa [le_cofinite_iff_compl_singleton_mem]

Premises used: Filter.le_cofinite_iff_compl_singleton_mem
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ⋃₀ B = univ
x : α
rw : ∀ (sUnion_univ : ∀ (a : α), ∃ b ∈ B, a ∈ b) (x : α), {x} ∈ B
⊢ {x} ∈ B

Tactic:
rw [sUnion_eq_univ_iff] at sUnion_univ

Premises used: Set.sUnion_eq_univ_iff
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (a : α), ∃ b ∈ B, a ∈ b
x : α
rcases : ∀ (s : Set α) (hs : s ∈ B) (hxs : x ∈ s), {x} ∈ B
⊢ {x} ∈ B

Tactic:
rcases sUnion_univ x with ⟨s, hs, hxs⟩
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (a : α), ∃ b ∈ B, a ∈ b
x : α
s : Set α
hs : s ∈ B
hxs : x ∈ s
⊢ {x} ∈ B

Tactic:
subset_mem s hs {x} (singleton_subset_iff.mpr hxs)

Premises used: Iff.mpr, Set.singleton_subset_iff, Singleton.singleton
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
ι : Type u_1
α_1 : Type u_2
β : Type u_3
α : Type u_4
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (a : α), ∃ b ∈ B, a ∈ b
x : α
s : Set α
hs : s ∈ B
hxs : x ∈ s
⊢ {x} ∈ B

Tactic:
exact subset_mem s hs {x} (singleton_subset_iff.mpr hxs)

Premises used: Iff.mpr, Set.singleton_subset_iff, Singleton.singleton
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
s : Set α
⊢ IsCobounded s ↔ s ∈ cobounded α

Tactic:
Iff.rfl

Premises used: Iff.rfl, Bornology.IsCobounded
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
s : Set α
⊢ IsBounded s ↔ sᶜ ∈ cobounded α

Tactic:
Iff.rfl

Premises used: Iff.rfl, Bornology.IsBounded, Bornology.IsCobounded
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
s : Set α
rw : sᶜᶜ ∈ cobounded α ↔ IsCobounded s
rw₁ : sᶜᶜ ∈ cobounded α ↔ s ∈ cobounded α
rw₂ rw₃ : s ∈ cobounded α ↔ s ∈ cobounded α
⊢ IsBounded sᶜ ↔ IsCobounded s

Tactic:
rw [isBounded_def, isCobounded_def, compl_compl]

Premises used: compl_compl, Bornology.isBounded_def, Bornology.isCobounded_def
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
s : Set α
⊢ IsCobounded sᶜ ↔ IsBounded s

Tactic:
Iff.rfl

Premises used: Iff.rfl, Bornology.IsBounded
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
rw : univ ∈ cobounded α
⊢ IsBounded.{u_2} (α := α) ∅

Tactic:
rw [isBounded_def, compl_empty]

Premises used: Bornology.isBounded_def, Set.compl_empty
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
⊢ univ ∈ cobounded α

Tactic:
univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
⊢ univ ∈ cobounded α

Tactic:
exact univ_mem

Premises used: Filter.univ_mem
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
s : Set α
h : ¬IsBounded s
rw : s ≠ ∅
⊢ s.Nonempty

Tactic:
rw [nonempty_iff_ne_empty]

Premises used: Set.nonempty_iff_ne_empty
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
h : ¬IsBounded.{u_2} (α := α) ∅
⊢ False

Tactic:
h isBounded_empty

Premises used: Bornology.isBounded_empty
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
h : ¬IsBounded.{u_2} (α := α) ∅
⊢ False

Tactic:
exact h isBounded_empty

Premises used: Bornology.isBounded_empty
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x_1 : Bornology α
x : α
⊢ {x}ᶜ ∈ cobounded α

Tactic:
le_cofinite _ (finite_singleton x).compl_mem_cofinite

Premises used: Bornology.le_cofinite, Set.Finite.compl_mem_cofinite, Set.finite_singleton
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x_1 : Bornology α
x : α
⊢ {x}ᶜ ∈ cobounded α

Tactic:
exact le_cofinite _ (finite_singleton x).compl_mem_cofinite

Premises used: Bornology.le_cofinite, Set.Finite.compl_mem_cofinite, Set.finite_singleton
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
s : Set α
h : ∀ x_1 ∈ s, IsBounded s
inl : ∀ (h : ∀ (x_1 : α), Membership.mem (γ := Set α) ∅ x_1 → IsBounded.{u_2} (α := α) ∅), IsBounded.{u_2} (α := α) ∅
inr : ∀ (x_1 : α) (hx : x_1 ∈ s), IsBounded s
⊢ IsBounded s

Tactic:
rcases s.eq_empty_or_nonempty with rfl | ⟨x, hx⟩

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
h : ∀ (x_1 : α), Membership.mem (γ := Set α) ∅ x_1 → IsBounded.{u_2} (α := α) ∅
⊢ IsBounded.{u_2} (α := α) ∅

Tactic:
isBounded_empty

Premises used: Bornology.isBounded_empty
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x_1 : Bornology α
s : Set α
h : ∀ x ∈ s, IsBounded s
x : α
hx : x ∈ s
⊢ IsBounded s

Tactic:
h x hx
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
h : ∀ (x_1 : α), Membership.mem (γ := Set α) ∅ x_1 → IsBounded.{u_2} (α := α) ∅
⊢ IsBounded.{u_2} (α := α) ∅

Tactic:
exacts [isBounded_empty, h x hx]

Premises used: Bornology.isBounded_empty
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
⊢ IsCobounded.{u_2} (α := α) univ

Tactic:
univ_mem

Premises used: Bornology.IsCobounded, Filter.univ_mem
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
s t : Set α
⊢ IsCobounded (s ∩ t) ↔ IsCobounded s ∧ IsCobounded t

Tactic:
inter_mem_iff

Premises used: Bornology.IsCobounded, Filter.inter_mem_iff
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
s t : Set α
hs : IsCobounded s
ht : IsCobounded t
⊢ IsCobounded (s ∩ t)

Tactic:
isCobounded_inter.2 ⟨hs, ht⟩

Premises used: Iff.mpr, Bornology.isCobounded_inter, And.intro
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
s t : Set α
⊢ IsBounded (s ∪ t) ↔ IsBounded s ∧ IsBounded t

Tactic:
simp only [← isCobounded_compl_iff, compl_union, isCobounded_inter]

Premises used: Set.compl_union, Bornology.isCobounded_inter, Bornology.isCobounded_compl_iff
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
s t : Set α
hs : IsBounded s
ht : IsBounded t
⊢ IsBounded (s ∪ t)

Tactic:
isBounded_union.2 ⟨hs, ht⟩

Premises used: Iff.mpr, Bornology.isBounded_union, And.intro
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
s t : Set α
hs : IsCobounded s
ht : s ⊆ t
⊢ IsCobounded t

Tactic:
mem_of_superset hs ht

Premises used: Bornology.IsCobounded, Filter.mem_of_superset
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
s t : Set α
ht : IsBounded t
hs : s ⊆ t
⊢ IsBounded s

Tactic:
ht.superset (compl_subset_compl.mpr hs)

Premises used: Iff.mpr, Bornology.IsCobounded.superset, Bornology.IsBounded, Set.compl_subset_compl
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x : Bornology α
⊢ Eq.{u_2 + 1} (α := Set α) (⋃₀ {s : Set α | IsBounded s}) univ

Tactic:
sUnion_eq_univ_iff.2 fun a => ⟨{a}, isBounded_singleton, mem_singleton a⟩

Premises used: Iff.mpr, Set.mem_singleton, And.intro, Exists.intro, Singleton.singleton, Set.sUnion_eq_univ_iff, Bornology.isBounded_singleton
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x_1 : Bornology α
s : Set α
h : IsBounded s
x : α
⊢ IsBounded (Insert.insert x s)

Tactic:
isBounded_singleton.union h

Premises used: Set.insert, Set.Mem, setOf, Set.singleton, Bornology.isBounded_singleton, Bornology.IsBounded.union
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
x_1 : Bornology α
s : Set α
x : α
⊢ IsBounded (insert x s) ↔ IsBounded s

Tactic:
⟨fun h ↦ h.subset (subset_insert _ _), (.insert · x)⟩

Premises used: Bornology.IsBounded.insert, Bornology.IsBounded.subset, Iff.intro, Set.subset_insert
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
β : Type u_3
x : Bornology α
inst : Bornology β
f : α → β
⊢ comap f (cobounded β) ≤ cobounded α ↔ ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)

Tactic:
⟨fun h s hs => ?_, fun h t ht =>
      ⟨(f '' tᶜ)ᶜ, h <| IsCobounded.compl ht, compl_subset_comm.1 <| subset_preimage_image _ _⟩⟩

Premises used: Compl.compl, Set.compl_subset_comm, Bornology.IsCobounded.compl, And.intro, Iff.intro, Exists.intro, Iff.mp, Set.image, Set.subset_preimage_image
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
β : Type u_3
x : Bornology α
inst : Bornology β
f : α → β
h : ∀ (h : comap f (cobounded β) ≤ cobounded α) (s : Set α) (hs : IsBounded s), IsBounded (f '' s)
⊢ comap f (cobounded β) ≤ cobounded α ↔ ∀ ⦃s : Set α⦄, IsBounded s → IsBounded (f '' s)

Tactic:
refine
    ⟨fun h s hs => ?_, fun h t ht =>
      ⟨(f '' tᶜ)ᶜ, h <| IsCobounded.compl ht, compl_subset_comm.1 <| subset_preimage_image _ _⟩⟩
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
β : Type u_3
x : Bornology α
inst : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
obtain : ∀ (t : Set β) (ht : t ∈ cobounded β) (hts : f ⁻¹' t ⊆ sᶜ), IsBounded (f '' s)
⊢ IsBounded (f '' s)

Tactic:
obtain ⟨t, ht, hts⟩ := h hs.compl

Premises used: Bornology.IsBounded.compl
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
β : Type u_3
x : Bornology α
inst : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : f ⁻¹' t ⊆ sᶜ
⊢ s ⊆ f ⁻¹' tᶜ

Tactic:
rw [subset_compl_comm, ← preimage_compl] at hts

Premises used: Set.subset_compl_comm, Set.preimage_compl
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
β : Type u_3
x : Bornology α
inst : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : s ⊆ f ⁻¹' tᶜ
⊢ IsBounded (f '' s)

Tactic:
(IsCobounded.compl ht).subset ((image_mono hts).trans <| image_preimage_subset _ _)

Premises used: Set.image_mono, HasSubset.Subset.trans, Bornology.IsCobounded.compl, Bornology.IsBounded.subset, Set.image_preimage_subset
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
β : Type u_3
x : Bornology α
inst : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : s ⊆ f ⁻¹' tᶜ
⊢ IsBounded (f '' s)

Tactic:
exact (IsCobounded.compl ht).subset ((image_mono hts).trans <| image_preimage_subset _ _)

Premises used: Set.image_mono, HasSubset.Subset.trans, Bornology.IsCobounded.compl, Bornology.IsBounded.subset, Set.image_preimage_subset
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
t t' : Bornology α
⊢ t = t' ↔ ∀ (s : Set α), s ∈ cobounded α ↔ s ∈ cobounded α

Tactic:
Bornology.ext_iff.trans Filter.ext_iff

Premises used: Bornology.ext_iff, Filter.ext_iff, Iff.trans
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
t t' : Bornology α
⊢ t = t' ↔ ∀ (s : Set α), IsBounded s ↔ IsBounded s

Tactic:
ext_iff'.trans compl_surjective.forall

Premises used: Function.Surjective.forall, Bornology.ext_iff', compl_surjective, Iff.trans
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
s : Set α
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (x : α), {x} ∈ B
⊢ IsCobounded s ↔ sᶜ ∈ B

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Bornology.IsCobounded
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
s : Set α
B : Set (Set α)
empty_mem : ∅ ∈ B
subset_mem : ∀ s₁ ∈ B, ∀ s₂ ⊆ s₁, s₂ ∈ B
union_mem : ∀ s₁ ∈ B, ∀ s₂ ∈ B, s₁ ∪ s₂ ∈ B
sUnion_univ : ∀ (x : α), {x} ∈ B
rw : sᶜ ∈ cobounded α ↔ s ∈ B
rw₁ : sᶜ ∈ comk (fun (x : Set α) ↦ x ∈ B) empty_mem subset_mem union_mem ↔ s ∈ B
rw₂ rw₃ : s ∈ B ↔ s ∈ B
⊢ IsBounded s ↔ s ∈ B

Tactic:
rw [isBounded_def, ofBounded_cobounded, compl_mem_comk]

Premises used: Bornology.isBounded_def, Filter.compl_mem_comk, Bornology.ofBounded_cobounded
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : Bornology α
s : Set ι
f : ι → Set α
hs : s.Finite
⊢ IsCobounded.{u_2} (α := α) (⋂ i ∈ s, f i) ↔ ∀ i ∈ s, IsCobounded (f i)

Tactic:
biInter_mem hs

Premises used: Filter.biInter_mem, Bornology.IsCobounded
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : Bornology α
s : Finset ι
f : ι → Set α
⊢ IsCobounded.{u_2} (α := α) (⋂ i ∈ s, f i) ↔ ∀ i ∈ s, IsCobounded (f i)

Tactic:
biInter_finset_mem s

Premises used: Filter.biInter_finset_mem, Bornology.IsCobounded
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : Bornology α
inst_1 : Finite ι
f : ι → Set α
⊢ IsCobounded.{u_2} (α := α) (⋂ (i : ι), f i) ↔ ∀ (i : ι), IsCobounded (f i)

Tactic:
iInter_mem

Premises used: Filter.iInter_mem, Bornology.IsCobounded
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
inst : Bornology α
S : Set (Set α)
hs : S.Finite
⊢ IsCobounded (⋂₀ S) ↔ ∀ s ∈ S, IsCobounded s

Tactic:
sInter_mem hs

Premises used: Filter.sInter_mem, Bornology.IsCobounded
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : Bornology α
s : Set ι
f : ι → Set α
hs : s.Finite
⊢ IsBounded.{u_2} (α := α) (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, IsBounded (f i)

Tactic:
simp only [← isCobounded_compl_iff, compl_iUnion, isCobounded_biInter hs]

Premises used: Set.compl_iUnion, Bornology.isCobounded_compl_iff, Bornology.isCobounded_biInter
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : Bornology α
s : Finset ι
f : ι → Set α
⊢ IsBounded.{u_2} (α := α) (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, IsBounded (f i)

Tactic:
isBounded_biUnion s.finite_toSet

Premises used: Bornology.isBounded_biUnion, Finset.finite_toSet
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
inst : Bornology α
S : Set (Set α)
hs : S.Finite
rw : IsBounded.{u_2} (α := α) (⋃ i ∈ S, i) ↔ ∀ s ∈ S, IsBounded s
rw₁ rw₂ : (∀ i ∈ S, IsBounded i) ↔ ∀ s ∈ S, IsBounded s
⊢ IsBounded (⋃₀ S) ↔ ∀ s ∈ S, IsBounded s

Tactic:
rw [sUnion_eq_biUnion, isBounded_biUnion hs]

Premises used: Bornology.isBounded_biUnion, Set.sUnion_eq_biUnion
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : Bornology α
inst_1 : Finite ι
s : ι → Set α
rw : IsBounded (⋃₀ range s) ↔ ∀ (i : ι), IsBounded (s i)
rw₁ : (∀ s_1 ∈ range s, IsBounded s_1) ↔ ∀ (i : ι), IsBounded (s i)
rw₂ rw₃ : (∀ (i : ι), IsBounded (s i)) ↔ ∀ (i : ι), IsBounded (s i)
⊢ IsBounded.{u_2} (α := α) (⋃ (i : ι), s i) ↔ ∀ (i : ι), IsBounded (s i)

Tactic:
rw [← sUnion_range, isBounded_sUnion (finite_range s), forall_mem_range]

Premises used: Set.sUnion_range, Set.forall_mem_range, Set.finite_range, Bornology.isBounded_sUnion
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
inst : Bornology α
a : α
⊢ ∀ᶠ (x : α) in cobounded α, x ≠ a

Tactic:
le_cofinite_iff_eventually_ne.1 (le_cofinite _) a

Premises used: Bornology.le_cofinite, Filter.le_cofinite_iff_eventually_ne, Iff.mp
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
inst : Bornology α
ι : Sort u_4
p : ι → Prop
s : ι → Set α
l : Filter α
h : l.HasBasis p s
⊢ Disjoint l (cobounded α) ↔ ∃ (i : ι), p i ∧ Bornology.IsBounded (s i)

Tactic:
h.disjoint_iff_left

Premises used: Bornology.IsBounded, Filter.HasBasis.disjoint_iff_left, Bornology.IsCobounded
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
inst : Bornology α
s : Set α
hs : s.Finite
⊢ Bornology.IsBounded s

Tactic:
Bornology.le_cofinite α hs.compl_mem_cofinite

Premises used: Bornology.le_cofinite, Bornology.IsBounded, Set.Finite.compl_mem_cofinite, Bornology.IsCobounded
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Bornology α
f : β → α
l : Filter β
h : Tendsto f l (cobounded α)
a : α
⊢ ∀ᶠ (x : β) in l, f x ≠ a

Tactic:
h.eventually <| eventually_ne_cobounded a

Premises used: Bornology.eventually_ne_cobounded, Filter.Tendsto.eventually
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
inst : Bornology α
⊢ IsBounded.{u_2} (α := α) univ ↔ BoundedSpace α

Tactic:
⟨fun h => ⟨h⟩, fun h => h.1⟩

Premises used: BoundedSpace.mk, BoundedSpace.bounded_univ, Iff.intro
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
inst : Bornology α
rw : cobounded α = ⊥ ↔ IsBounded.{u_2} (α := α) univ
rw₁ : cobounded α = ⊥ ↔ univᶜ ∈ cobounded α
rw₂ : cobounded α = ⊥ ↔ ∅ ∈ cobounded α
rw₃ rw₄ : cobounded α = ⊥ ↔ cobounded α = ⊥
⊢ cobounded α = ⊥ ↔ BoundedSpace α

Tactic:
rw [← isBounded_univ, isBounded_def, compl_univ, empty_mem_iff_bot]

Premises used: Bornology.isBounded_def, Set.compl_univ, Bornology.isBounded_univ, Filter.empty_mem_iff_bot
-- Module: Mathlib.Topology.Bornology.Basic
Goal:
α : Type u_2
inst : Bornology α
inst_1 : BoundedSpace α
s : Set α
⊢ IsBounded s

Tactic:
BoundedSpace.bounded_univ.subset s.subset_univ

Premises used: Set.subset_univ, BoundedSpace.bounded_univ, Bornology.IsBounded.subset