awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : NoMaxOrder β
f : α → β
l : Filter α
inst_2 : l.NeBot
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun (x1 x2 : β) ↦ x1 ≤ x2) (f a) b
b' : β
h : b < b'
hb' : ∀ᶠ (a : α) in l, b' ≤ f a
⊢ Eq.{u_1 + 1} (α := Set α) ({x : α | f x ≤ b} ∩ {x : α | b' ≤ f x}) ∅

Tactic:
have : { x : α | f x ≤ b } ∩ { x : α | b' ≤ f x } = ∅ :=
    eq_empty_of_subset_empty fun x hx => (not_le_of_gt h) (le_trans hx.2 hx.1)
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : NoMaxOrder β
f : α → β
l : Filter α
inst_2 : l.NeBot
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun (x1 x2 : β) ↦ x1 ≤ x2) (f a) b
b' : β
h : b < b'
hb' : ∀ᶠ (a : α) in l, b' ≤ f a
this : Eq.{u_1 + 1} (α := Set α) ({x : α | f x ≤ b} ∩ {x : α | b' ≤ f x}) ∅
⊢ False

Tactic:
(nonempty_of_mem (hb.and hb')).ne_empty this

Premises used: Set.Nonempty.ne_empty, Filter.Eventually.and, Filter.nonempty_of_mem
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : NoMaxOrder β
f : α → β
l : Filter α
inst_2 : l.NeBot
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun (x1 x2 : β) ↦ x1 ≤ x2) (f a) b
b' : β
h : b < b'
hb' : ∀ᶠ (a : α) in l, b' ≤ f a
this : Eq.{u_1 + 1} (α := Set α) ({x : α | f x ≤ b} ∩ {x : α | b' ≤ f x}) ∅
⊢ False

Tactic:
exact (nonempty_of_mem (hb.and hb')).ne_empty this

Premises used: Set.Nonempty.ne_empty, Filter.Eventually.and, Filter.nonempty_of_mem
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : NoMinOrder β
f : α → β
l : Filter α
inst_2 : l.NeBot
hf : Tendsto f l atBot
⊢ ¬IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) l f

Tactic:
not_isBoundedUnder_of_tendsto_atTop (β := βᵒᵈ) hf

Premises used: Filter.not_isBoundedUnder_of_tendsto_atTop, OrderDual
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : IsDirectedOrder β
f : α → β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) cofinite f
rcases : ∀ (b : β) (hb : ∀ᶠ (x : β) in map f cofinite, (fun (x1 x2 : β) ↦ x1 ≤ x2) x b), BddAbove (range f)
⊢ BddAbove (range f)

Tactic:
rcases hf with ⟨b, hb⟩
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : IsDirectedOrder β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun (x1 x2 : β) ↦ x1 ≤ x2) x b
⊢ Nonempty β

Tactic:
haveI : Nonempty β := ⟨b⟩
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : IsDirectedOrder β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun (x1 x2 : β) ↦ x1 ≤ x2) x b
this : Nonempty β
rw : BddAbove (f '' {x : α | f x ≤ b}) ∧ BddAbove (f '' {x : α | f x ≤ b}ᶜ)
⊢ BddAbove (range f)

Tactic:
rw [← image_univ, ← union_compl_self { x | f x ≤ b }, image_union, bddAbove_union]

Premises used: Set.image_univ, bddAbove_union, setOf, Set.union_compl_self, LE.le, Set.image_union
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : IsDirectedOrder β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun (x1 x2 : β) ↦ x1 ≤ x2) x b
this : Nonempty β
⊢ BddAbove (f '' {x : α | f x ≤ b}) ∧ BddAbove (f '' {x : α | f x ≤ b}ᶜ)

Tactic:
⟨⟨b, forall_mem_image.2 fun x => id⟩, (hb.image f).bddAbove⟩

Premises used: Iff.mpr, id, Set.Finite.image, And.intro, Exists.intro, Set.Finite.bddAbove, Set.forall_mem_image
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : IsDirectedOrder β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun (x1 x2 : β) ↦ x1 ≤ x2) x b
this : Nonempty β
⊢ BddAbove (f '' {x : α | f x ≤ b}) ∧ BddAbove (f '' {x : α | f x ≤ b}ᶜ)

Tactic:
exact ⟨⟨b, forall_mem_image.2 fun x => id⟩, (hb.image f).bddAbove⟩
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder β
inst_1 : IsCodirectedOrder β
f : α → β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) cofinite f
⊢ BddBelow (range f)

Tactic:
IsBoundedUnder.bddAbove_range_of_cofinite (β := βᵒᵈ) hf

Premises used: lowerBounds, Set.Mem, setOf, BddBelow, OrderDual, Filter.IsBoundedUnder.bddAbove_range_of_cofinite
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
β : Type u_2
inst : Preorder β
inst_1 : IsDirectedOrder β
f : ℕ → β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) atTop f
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) cofinite f

Tactic:
rw [← Nat.cofinite_eq_atTop] at hf

Premises used: Nat.cofinite_eq_atTop
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
β : Type u_2
inst : Preorder β
inst_1 : IsDirectedOrder β
f : ℕ → β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) cofinite f
⊢ BddAbove (range f)

Tactic:
hf.bddAbove_range_of_cofinite

Premises used: Filter.IsBoundedUnder.bddAbove_range_of_cofinite
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
β : Type u_2
inst : Preorder β
inst_1 : IsDirectedOrder β
f : ℕ → β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) cofinite f
⊢ BddAbove (range f)

Tactic:
exact hf.bddAbove_range_of_cofinite

Premises used: Filter.IsBoundedUnder.bddAbove_range_of_cofinite
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
β : Type u_2
inst : Preorder β
inst_1 : IsCodirectedOrder β
f : ℕ → β
hf : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) atTop f
⊢ BddBelow (range f)

Tactic:
IsBoundedUnder.bddAbove_range (β := βᵒᵈ) hf

Premises used: lowerBounds, Set.Mem, setOf, BddBelow, OrderDual, Filter.IsBoundedUnder.bddAbove_range
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
r : α → α → Prop
f : Filter α
inst : IsTrans α r
a : α
h : ∀ s ∈ f, ∃ x ∈ s, r a x
⊢ IsCobounded r f

Tactic:
⟨a, fun _ s =>
    let ⟨_, h₁, h₂⟩ := h _ s
    _root_.trans h₂ h₁⟩

Premises used: trans, setOf, Filter.IsCobounded, Exists.intro, _private.0.Filter.IsCobounded.mk.match_1
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : Preorder α
inst_1 : f.NeBot
h : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
⊢ IsCobounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f

Tactic:
h.isCobounded_flip

Premises used: Filter.IsBounded.isCobounded_flip
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : Preorder α
inst_1 : f.NeBot
h : IsBounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f
⊢ IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f

Tactic:
h.isCobounded_flip

Premises used: Filter.IsBounded.isCobounded_flip
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
γ : Type u_3
r : α → α → Prop
u : γ → α
l : Filter γ
inst : IsTrans α r
inst_1 : l.NeBot
h : IsBoundedUnder r l u
⊢ IsCoboundedUnder (flip r) l u

Tactic:
h.isCobounded_flip

Premises used: Filter.IsCoboundedUnder, Filter.IsBounded.isCobounded_flip
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
γ : Type u_3
u : γ → α
l : Filter γ
inst : Preorder α
inst_1 : l.NeBot
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) l u
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) l u

Tactic:
h.isCoboundedUnder_flip

Premises used: Filter.IsBoundedUnder.isCoboundedUnder_flip
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
γ : Type u_3
u : γ → α
l : Filter γ
inst : Preorder α
inst_1 : l.NeBot
h : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) l u
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) l u

Tactic:
h.isCoboundedUnder_flip

Premises used: Filter.IsBoundedUnder.isCoboundedUnder_flip
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
l : Filter ι
inst_1 : l.NeBot
f : ι → α
x : α
hf : ∀ᶠ (i : ι) in l, x ≤ f i
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) l f

Tactic:
IsBoundedUnder.isCoboundedUnder_le ⟨x, hf⟩

Premises used: Filter.IsBoundedUnder.isCoboundedUnder_le, Exists.intro
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
l : Filter ι
inst_1 : l.NeBot
f : ι → α
x : α
hf : ∀ᶠ (i : ι) in l, f i ≤ x
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) l f

Tactic:
IsBoundedUnder.isCoboundedUnder_ge ⟨x, hf⟩

Premises used: Exists.intro, Filter.IsBoundedUnder.isCoboundedUnder_ge
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
l : Filter ι
inst_1 : l.NeBot
f : ι → α
x : α
hf : ∀ (i : ι), x ≤ f i
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) l f

Tactic:
isCoboundedUnder_le_of_eventually_le l (Eventually.of_forall hf)

Premises used: Filter.Eventually.of_forall, Filter.isCoboundedUnder_le_of_eventually_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
l : Filter ι
inst_1 : l.NeBot
f : ι → α
x : α
hf : ∀ (i : ι), f i ≤ x
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) l f

Tactic:
isCoboundedUnder_ge_of_eventually_le l (Eventually.of_forall hf)

Premises used: Filter.isCoboundedUnder_ge_of_eventually_le, Filter.Eventually.of_forall
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
r : α → α → Prop
⊢ IsCobounded r ⊥ ↔ ∃ (b : α), ∀ (x : α), r b x

Tactic:
simp [IsCobounded]

Premises used: Filter.IsCobounded
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
r : α → α → Prop
⊢ IsCobounded r ⊤ ↔ Nonempty α

Tactic:
simp +contextual [IsCobounded,
    exists_true_iff_nonempty]

Premises used: exists_true_iff_nonempty, Filter.IsCobounded
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
⊢ IsCobounded r (𝓟 s) ↔ ∃ (b : α), ∀ (a : α), (∀ x ∈ s, r x a) → r b a

Tactic:
simp [IsCobounded]

Premises used: Filter.IsCobounded
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
cobdd : IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
obtain :
  ∀ (t : α) (ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : α) ↦ x1 ≤ x2) t a),
    ∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x
⊢ ∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x

Tactic:
obtain ⟨t, ht⟩ := cobdd
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : α) ↦ x1 ≤ x2) t a
inl : ∀ (tbot : IsBot t), ∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x
inr : ∀ (t' : α) (ht' : t' < t), ∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x
⊢ ∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x

Tactic:
rcases isBot_or_exists_lt t with tbot | ⟨t', ht'⟩

Premises used: isBot_or_exists_lt
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : α) ↦ x1 ≤ x2) t a
tbot : IsBot t
⊢ ∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x

Tactic:
⟨t, .of_forall fun r ↦ tbot r⟩

Premises used: Filter.Frequently.of_forall, Exists.intro
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : α) ↦ x1 ≤ x2) t a
tbot : IsBot t
⊢ ∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x

Tactic:
exact ⟨t, .of_forall fun r ↦ tbot r⟩
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : α) ↦ x1 ≤ x2) t a
t' : α
ht' : t' < t
⊢ ∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x

Tactic:
⟨t', fun ev ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : α) ↦ x1 ≤ x2) t a
t' : α
ht' : t' < t
inr : ∀ (ev : ∀ᶠ (x : α) in f, ¬(fun (x : α) ↦ t' ≤ x) x), False
⊢ ∃ (l : α), ∃ᶠ (x : α) in f, l ≤ x

Tactic:
refine ⟨t', fun ev ↦ ?_⟩
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : α) ↦ x1 ≤ x2) t a
t' : α
ht' : t' < t
ev : ∀ᶠ (x : α) in f, ¬(fun (x : α) ↦ t' ≤ x) x
a : α
h : ¬t' ≤ a
⊢ a ≤ t'

Tactic:
(not_le.mp h).le

Premises used: not_le, LT.lt.le, Iff.mp
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : α) ↦ x1 ≤ x2) t a
t' : α
ht' : t' < t
ev : ∀ᶠ (x : α) in f, ¬(fun (x : α) ↦ t' ≤ x) x
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ¬(fun (x : α) ↦ t' ≤ x) x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ((fun (x1 x2 : α) ↦ x1 ≤ x2) x t' : Prop)) x} x}
      a
h₁ h₂ : ∀ (a : α) (h : ¬t' ≤ a), a ≤ t'
⊢ ∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x t'

Tactic:
filter_upwards [ev] with _ h using (not_le.mp h).le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : α) ↦ x1 ≤ x2) t a
t' : α
ht' : t' < t
ev : ∀ᶠ (x : α) in f, ¬(fun (x : α) ↦ t' ≤ x) x
⊢ t ≤ t'

Tactic:
specialize ht t' (by filter_upwards [ev] with _ h using (not_le.mp h).le)
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
t t' : α
ht' : t' < t
ev : ∀ᶠ (x : α) in f, ¬(fun (x : α) ↦ t' ≤ x) x
ht : t ≤ t'
⊢ False

Tactic:
not_lt_of_ge ht ht'

Premises used: not_lt_of_ge
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
t t' : α
ht' : t' < t
ev : ∀ᶠ (x : α) in f, ¬(fun (x : α) ↦ t' ≤ x) x
ht : t ≤ t'
⊢ False

Tactic:
exact not_lt_of_ge ht ht'

Premises used: not_lt_of_ge
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
inst_1 : f.NeBot
cobdd : IsCobounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f
⊢ ∃ (u : α), ∃ᶠ (x : α) in f, x ≤ u

Tactic:
cobdd.frequently_ge (α := αᵒᵈ)

Premises used: OrderDual, Filter.IsCobounded.frequently_ge
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
inl : ∀ (lbot : IsBot l), IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
inr : ∀ (l' : α) (hl' : l' < l), IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
⊢ IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f

Tactic:
rcases isBot_or_exists_lt l with lbot | ⟨l', hl'⟩

Premises used: isBot_or_exists_lt
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
lbot : IsBot l
⊢ IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f

Tactic:
⟨l, fun x _ ↦ lbot x⟩

Premises used: Filter.IsCobounded, Exists.intro
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
lbot : IsBot l
⊢ IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f

Tactic:
exact ⟨l, fun x _ ↦ lbot x⟩
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
l' : α
hl' : l' < l
⊢ IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f

Tactic:
⟨l', fun u hu ↦ ?_⟩

Premises used: Filter.IsCobounded, Exists.intro
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
l' : α
hl' : l' < l
inr : ∀ (u : α) (hu : ∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x u), (fun (x1 x2 : α) ↦ x1 ≤ x2) l' u
⊢ IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f

Tactic:
refine ⟨l', fun u hu ↦ ?_⟩
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
l' : α
hl' : l' < l
u : α
hu : ∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x u
inr : ∀ (w : α) (l_le_w : l ≤ w) (w_le_u : w ≤ u), l' ≤ u
⊢ l' ≤ u

Tactic:
obtain ⟨w, l_le_w, w_le_u⟩ := (freq_ge.and_eventually hu).exists

Premises used: Filter.Frequently.and_eventually, Filter.Frequently.exists
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
l' : α
hl' : l' < l
u : α
hu : ∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x u
w : α
l_le_w : l ≤ w
w_le_u : w ≤ u
⊢ l' ≤ u

Tactic:
hl'.le.trans (l_le_w.trans w_le_u)

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
l' : α
hl' : l' < l
u : α
hu : ∀ᶠ (x : α) in f, (fun (x1 x2 : α) ↦ x1 ≤ x2) x u
w : α
l_le_w : l ≤ w
w_le_u : w ≤ u
⊢ l' ≤ u

Tactic:
exact hl'.le.trans (l_le_w.trans w_le_u)

Premises used: LT.lt.le, LE.le.trans
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
f : Filter α
inst : LinearOrder α
u : α
freq_le : ∃ᶠ (r : α) in f, r ≤ u
⊢ IsCobounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f

Tactic:
IsCobounded.of_frequently_ge (α := αᵒᵈ) freq_le

Premises used: Filter.IsCobounded.of_frequently_ge, OrderDual
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder α
f : Filter ι
inst_1 : f.NeBot
u : ι → α
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
⊢ ∃ (a : α), ∃ᶠ (x : ι) in f, a ≤ u x

Tactic:
IsCobounded.frequently_ge h

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.Frequently, Set.preimage, Not, Filter.IsCobounded.frequently_ge
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder α
f : Filter ι
inst_1 : f.NeBot
u : ι → α
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
⊢ ∃ (a : α), ∃ᶠ (x : ι) in f, u x ≤ a

Tactic:
IsCobounded.frequently_le h

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.Frequently, Set.preimage, Not, Filter.IsCobounded.frequently_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder α
f : Filter ι
u : ι → α
a : α
freq_ge : ∃ᶠ (x : ι) in f, a ≤ u x
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u

Tactic:
IsCobounded.of_frequently_ge freq_ge

Premises used: Filter.IsCobounded.of_frequently_ge, Filter.IsCoboundedUnder
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder α
f : Filter ι
u : ι → α
a : α
freq_le : ∃ᶠ (x : ι) in f, u x ≤ a
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u

Tactic:
IsCobounded.of_frequently_le freq_le

Premises used: Filter.IsCoboundedUnder, Filter.IsCobounded.of_frequently_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
s : Finset κ
h : ∀ k ∈ s, IsBoundedUnder r f (u k)
induction :
  ∀ (h : ∀ (k : κ), Membership.mem (γ := Finset κ) ∅ k → IsBoundedUnder r f (u k)), IsBoundedUnder r f (∑ k ∈ ∅, u k)
cons :
  ∀ (a : κ) (s : Finset κ) (h : a ∉ s),
    (∀ (h : ∀ k ∈ s, IsBoundedUnder r f (u k)), IsBoundedUnder r f (∑ k ∈ s, u k)) →
      ∀ (h_1 : ∀ k ∈ Finset.cons a s h, IsBoundedUnder r f (u k)), IsBoundedUnder r f (∑ k ∈ Finset.cons a s h, u k)
⊢ IsBoundedUnder r f (∑ k ∈ s, u k)

Tactic:
induction s using Finset.cons_induction
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
h : ∀ (k : κ), Membership.mem (γ := Finset κ) ∅ k → IsBoundedUnder r f (u k)
⊢ ∀ᶠ (x : R) in map 0 f, r x 0

Tactic:
simp_all only [eventually_map, Pi.zero_apply, eventually_true]

Premises used: Pi.zero_apply, Filter.eventually_map, Filter.eventually_true
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
h : ∀ (k : κ), Membership.mem (γ := Finset κ) ∅ k → IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f 0

Tactic:
exact ⟨0, by simp_all only [eventually_map, Pi.zero_apply, eventually_true]⟩
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
h : ∀ (k : κ), Membership.mem (γ := Finset κ) ∅ k → IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (∑ k ∈ ∅, u k)

Tactic:
case empty =>
    rw [Finset.sum_empty]
    exact ⟨0, by simp_all only [eventually_map, Pi.zero_apply, eventually_true]⟩

Premises used: Finset.sum_empty
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
k₀ : κ
s : Finset κ
k₀_notin_s : k₀ ∉ s
ih : ∀ (h : ∀ k ∈ s, IsBoundedUnder r f (u k)), IsBoundedUnder r f (∑ k ∈ s, u k)
h : ∀ k ∈ Finset.cons k₀ s k₀_notin_s, IsBoundedUnder r f (u k)
⊢ IsBoundedUnder r f (u k₀) ∧ ∀ x ∈ s, IsBoundedUnder r f (u x)

Tactic:
simp only [Finset.forall_mem_cons] at *

Premises used: Finset.forall_mem_cons
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
f : Filter α
R : Type u_6
κ : Type u_7
inst : AddCommMonoid R
r : R → R → Prop
hr : ∀ (v₁ v₂ : α → R), IsBoundedUnder r f v₁ → IsBoundedUnder r f v₂ → IsBoundedUnder r f (v₁ + v₂)
hr₀ : r 0 0
u : κ → α → R
k₀ : κ
s : Finset κ
k₀_notin_s : k₀ ∉ s
ih : ∀ (h : ∀ k ∈ s, IsBoundedUnder r f (u k)), IsBoundedUnder r f (∑ k ∈ s, u k)
h : IsBoundedUnder r f (u k₀) ∧ ∀ x ∈ s, IsBoundedUnder r f (u x)
⊢ IsBoundedUnder r f (∑ k ∈ Finset.cons k₀ s k₀_notin_s, u k)

Tactic:
simpa only [Finset.sum_cons] using hr _ _ h.1 (ih h.2)

Premises used: Finset.sum_cons, And.right, And.left
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
inst_1 : Add R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u v : α → R
u_bdd_ge : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f u
v_bdd_ge : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f v
obtain :
  ∀ (U : R) (hU : ∀ᶠ (x : R) in map u f, (fun (x1 x2 : R) ↦ x1 ≥ x2) x U),
    IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)
⊢ IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)

Tactic:
obtain ⟨U, hU⟩ := u_bdd_ge
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
inst_1 : Add R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u v : α → R
v_bdd_ge : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f v
U : R
hU : ∀ᶠ (x : R) in map u f, (fun (x1 x2 : R) ↦ x1 ≥ x2) x U
obtain :
  ∀ (V : R) (hV : ∀ᶠ (x : R) in map v f, (fun (x1 x2 : R) ↦ x1 ≥ x2) x V),
    IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)
⊢ IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)

Tactic:
obtain ⟨V, hV⟩ := v_bdd_ge
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
inst_1 : Add R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u v : α → R
U : R
hU : ∀ᶠ (x : R) in map u f, (fun (x1 x2 : R) ↦ x1 ≥ x2) x U
V : R
hV : ∀ᶠ (x : R) in map v f, (fun (x1 x2 : R) ↦ x1 ≥ x2) x V
h : ∀ᶠ (x : R) in map (u + v) f, (fun (x1 x2 : R) ↦ x1 ≥ x2) x (U + V)
⊢ IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)

Tactic:
use U + V
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
inst_1 : Add R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u v : α → R
U : R
hU : ∀ᶠ (x : R) in map u f, (fun (x1 x2 : R) ↦ x1 ≥ x2) x U
V : R
hV : ∀ᶠ (x : R) in map v f, (fun (x1 x2 : R) ↦ x1 ≥ x2) x V
h : ∀ (hU : ∀ᶠ (a : α) in f, u a ≥ U) (hV : ∀ᶠ (a : α) in f, v a ≥ V), ∀ᶠ (a : α) in f, u a + v a ≥ U + V
⊢ ∀ᶠ (x : R) in map (u + v) f, (fun (x1 x2 : R) ↦ x1 ≥ x2) x (U + V)

Tactic:
simp only [eventually_map, Pi.add_apply] at hU hV ⊢

Premises used: Filter.eventually_map, Pi.add_apply
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
inst_1 : Add R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u v : α → R
U V : R
hU : ∀ᶠ (a : α) in f, u a ≥ U
hV : ∀ᶠ (a : α) in f, v a ≥ V
a : α
hu : u a ≥ U
hv : v a ≥ V
⊢ u a + v a ≥ U + V

Tactic:
add_le_add hu hv

Premises used: add_le_add