awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsDirectedOrder α
u : ℕ → α
hx : Tendsto u atTop atBot
⊢ BddAbove (range u)

Tactic:
hx.isBoundedUnder_le_atBot.bddAbove_range

Premises used: Filter.Tendsto.isBoundedUnder_le_atBot, Filter.IsBoundedUnder.bddAbove_range
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
inst_2 : IsCodirectedOrder α
u : ℕ → α
hx : Tendsto u atTop atTop
⊢ BddBelow (range u)

Tactic:
hx.isBoundedUnder_ge_atTop.bddBelow_range

Premises used: Filter.IsBoundedUnder.bddBelow_range, Filter.Tendsto.isBoundedUnder_ge_atTop
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderBot α
f : Filter α
⊢ IsCobounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f

Tactic:
⟨⊥, fun _ _ => bot_le⟩

Premises used: Bot.bot, Filter.IsCobounded, Exists.intro, bot_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderTop α
f : Filter α
⊢ IsCobounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f

Tactic:
⟨⊤, fun _ _ => le_top⟩

Premises used: Filter.IsCobounded, le_top, Exists.intro, Top.top
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderTop α
f : Filter α
⊢ IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f

Tactic:
⟨⊤, Eventually.of_forall fun _ => le_top⟩

Premises used: Filter.Eventually.of_forall, Filter.IsBounded, le_top, Exists.intro, Top.top
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
inst : LE α
inst_1 : OrderBot α
f : Filter α
⊢ IsBounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f

Tactic:
⟨⊥, Eventually.of_forall fun _ => bot_le⟩

Premises used: Filter.Eventually.of_forall, Bot.bot, Filter.IsBounded, Exists.intro, bot_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
l : Filter γ
u : γ → α
a : α
⊢ (∀ᶠ (x : β) in map (fun (x : γ) ↦ (e : (a : α) → β) (u x)) l, (fun (x1 x2 : β) ↦ x1 ≤ x2) x ((e : (a : α) → β) a)) ↔
    ∀ᶠ (x : α) in map u l, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a

Tactic:
simp only [eventually_map, e.le_iff_le]

Premises used: OrderIso.le_iff_le, Filter.eventually_map
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
inst_1 : LE β
e : α ≃o β
l : Filter γ
u : γ → α
⊢ (IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) l fun (x : γ) ↦ (e : (a : α) → β) (u x)) ↔
    IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) l u

Tactic:
OrderIso.isBoundedUnder_le_comp e.dual

Premises used: OrderIso.dual, OrderIso.isBoundedUnder_le_comp, OrderDual
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
l : Filter β
u : β → α
⊢ (IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) l fun (x : β) ↦ (u x)⁻¹) ↔ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) l u

Tactic:
(OrderIso.inv α).isBoundedUnder_ge_comp

Premises used: OrderIso.isBoundedUnder_ge_comp, OrderIso.inv, OrderDual
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
l : Filter β
u : β → α
⊢ (IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) l fun (x : β) ↦ (u x)⁻¹) ↔ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) l u

Tactic:
(OrderIso.inv α).isBoundedUnder_le_comp

Premises used: OrderIso.inv, OrderIso.isBoundedUnder_le_comp, OrderDual
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
f : Filter β
u v : β → α
bu : α
hu : ∀ᶠ (x : β) in f, u x ≤ bu
bv : α
hv : ∀ᶠ (x : β) in f, v x ≤ bv
a : β
⊢ u a ≤ bu → v a ≤ bv → u a ⊔ v a ≤ bu ⊔ bv

Tactic:
sup_le_sup

Premises used: sup_le_sup
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
f : Filter β
u v : β → α
bu : α
hu : ∀ᶠ (x : β) in f, u x ≤ bu
bv : α
hv : ∀ᶠ (x : β) in f, v x ≤ bv
h :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ u x ≤ bu) x} x →
          Membership.mem (γ := Set β)
            {x : β |
              Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ v x ≤ bv) x} x →
                Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ u x ⊔ v x ≤ bu ⊔ bv) x} x}
            x}
      a
h₁ h₂ : ∀ (a : β), u a ≤ bu → v a ≤ bv → u a ⊔ v a ≤ bu ⊔ bv
⊢ ∀ᶠ (x : β) in f, u x ⊔ v x ≤ bu ⊔ bv

Tactic:
filter_upwards [hu, hv] with _ using sup_le_sup

Premises used: sup_le_sup
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeSup α
f : Filter β
u v : β → α
⊢ (IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f fun (a : β) ↦ u a ⊔ v a) ↔
    IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u ∧ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v

Tactic:
⟨fun h =>
    ⟨h.mono_le <| Eventually.of_forall fun _ => le_sup_left,
      h.mono_le <| Eventually.of_forall fun _ => le_sup_right⟩,
    fun h => h.1.sup h.2⟩

Premises used: le_sup_left, Filter.IsBoundedUnder.sup, Filter.IsBoundedUnder.mono_le, le_sup_right, Filter.Eventually.of_forall, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
f : Filter β
u v : β → α
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u →
    IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v →
      IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f fun (a : β) ↦ u a ⊓ v a

Tactic:
IsBoundedUnder.sup (α := αᵒᵈ)

Premises used: Filter.IsBoundedUnder.sup, OrderDual
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : SemilatticeInf α
f : Filter β
u v : β → α
⊢ (IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f fun (a : β) ↦ u a ⊓ v a) ↔
    IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u ∧ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v

Tactic:
isBoundedUnder_le_sup (α := αᵒᵈ)

Premises used: Filter.isBoundedUnder_le_sup, OrderDual
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
f : Filter β
u : β → α
⊢ (IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f fun (a : β) ↦ |u a|) ↔
    IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u ∧ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u

Tactic:
isBoundedUnder_le_sup.trans <| and_congr Iff.rfl isBoundedUnder_le_neg

Premises used: abs, Iff.rfl, Filter.isBoundedUnder_le_sup, Filter.isBoundedUnder_le_neg, Iff.trans, and_congr
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty β
inst_1 : LinearOrder β
inst_2 : Preorder γ
inst_3 : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
⊢ IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) l (g ∘ f) ↔ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l f

Tactic:
⟨?_, fun h => h.isBoundedUnder (α := β) hg⟩

Premises used: Filter.IsBounded.isBoundedUnder, Iff.intro
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty β
inst_1 : LinearOrder β
inst_2 : Preorder γ
inst_3 : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
refine : IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) l (g ∘ f) → IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l f
⊢ IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) l (g ∘ f) ↔ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l f

Tactic:
refine ⟨?_, fun h => h.isBoundedUnder (α := β) hg⟩
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty β
inst_1 : LinearOrder β
inst_2 : Preorder γ
inst_3 : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (x : γ) in map (g ∘ f) l, (fun (x1 x2 : γ) ↦ x1 ≤ x2) x c
⊢ ∀ᶠ (a : α) in l, (fun (x1 x2 : γ) ↦ x1 ≤ x2) ((g ∘ f) a) c

Tactic:
rw [eventually_map] at hc

Premises used: Filter.eventually_map
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty β
inst_1 : LinearOrder β
inst_2 : Preorder γ
inst_3 : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun (x1 x2 : γ) ↦ x1 ≤ x2) ((g ∘ f) a) c
⊢ ∃ (b : β), ∀ a ≥ b, c < g a

Tactic:
eventually_atTop.1 (hg'.eventually_gt_atTop c)

Premises used: Iff.mp, Filter.eventually_atTop, Filter.Tendsto.eventually_gt_atTop
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty β
inst_1 : LinearOrder β
inst_2 : Preorder γ
inst_3 : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun (x1 x2 : γ) ↦ x1 ≤ x2) ((g ∘ f) a) c
obtain : ∀ (b : β) (hb : ∀ a ≥ b, c < g a), IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l f
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l f

Tactic:
obtain ⟨b, hb⟩ : ∃ b, ∀ a ≥ b, c < g a := eventually_atTop.1 (hg'.eventually_gt_atTop c)

Premises used: Iff.mp, Filter.eventually_atTop, Filter.Tendsto.eventually_gt_atTop
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty β
inst_1 : LinearOrder β
inst_2 : Preorder γ
inst_3 : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun (x1 x2 : γ) ↦ x1 ≤ x2) ((g ∘ f) a) c
b : β
hb : ∀ a ≥ b, c < g a
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l f

Tactic:
⟨b, hc.mono fun x hx => not_lt.1 fun h => (hb _ h.le).not_ge hx⟩

Premises used: LT.lt.le, Filter.IsBounded, Filter.Eventually.mono, not_lt, Exists.intro, Iff.mp, LT.lt.not_ge, Filter.IsBoundedUnder
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty β
inst_1 : LinearOrder β
inst_2 : Preorder γ
inst_3 : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun (x1 x2 : γ) ↦ x1 ≤ x2) ((g ∘ f) a) c
b : β
hb : ∀ a ≥ b, c < g a
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l f

Tactic:
exact ⟨b, hc.mono fun x hx => not_lt.1 fun h => (hb _ h.le).not_ge hx⟩
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty β
inst_1 : LinearOrder β
inst_2 : Preorder γ
inst_3 : NoMinOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atBot atBot
⊢ IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≥ x2) l (g ∘ f) ↔ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) l f

Tactic:
hg.dual.isBoundedUnder_le_comp_iff hg'

Premises used: Monotone.dual, Monotone.isBoundedUnder_le_comp_iff, OrderDual
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty β
inst_1 : LinearOrder β
inst_2 : Preorder γ
inst_3 : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Antitone g
hg' : Tendsto g atBot atTop
⊢ IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≤ x2) l (g ∘ f) ↔ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) l f

Tactic:
hg.dual_right.isBoundedUnder_ge_comp_iff hg'

Premises used: Antitone.dual_right, OrderDual, Monotone.isBoundedUnder_ge_comp_iff
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Nonempty β
inst_1 : LinearOrder β
inst_2 : Preorder γ
inst_3 : NoMinOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Antitone g
hg' : Tendsto g atTop atBot
⊢ IsBoundedUnder (fun (x1 x2 : γ) ↦ x1 ≥ x2) l (g ∘ f) ↔ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) l f

Tactic:
hg.dual_right.isBoundedUnder_le_comp_iff hg'

Premises used: Antitone.dual_right, Monotone.isBoundedUnder_le_comp_iff, OrderDual
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
h : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u ∨ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
inl :
  ∀ (h' : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u),
    IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
inr :
  ∀ (h' : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v),
    IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)

Tactic:
rcases h with (h' | h')
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
inl :
  ∀ (b : β)
    (hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a),
    IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)

Tactic:
rcases h' with ⟨b, hb⟩
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
h :
  ∀ (a : β),
    (∀ᶠ (x : β) in map (fun (a : α) ↦ max (u a) (v a)) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) →
      (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)

Tactic:
use b
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun (a : α) ↦ max (u a) (v a)) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c
h : ∀ᶠ (x : β) in map u f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c
⊢ b ≤ c

Tactic:
apply hb c
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun (a : α) ↦ max (u a) (v a)) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c
h :
  ∀ (hc : ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (max (u a) (v a)) c),
    ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (u a) c
⊢ ∀ᶠ (x : β) in map u f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c

Tactic:
rw [eventually_map] at hc ⊢

Premises used: Filter.eventually_map
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (max (u a) (v a)) c
⊢ ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (u a) c

Tactic:
hc.mono (fun _ ↦ ?_)

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (max (u a) (v a)) c
h : ∀ (x : α), (fun (x1 x2 : β) ↦ x1 ≤ x2) (max (u x) (v x)) c → (fun (x1 x2 : β) ↦ x1 ≤ x2) (u x) c
⊢ ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (u a) c

Tactic:
refine hc.mono (fun _ ↦ ?_)

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map u f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (max (u a) (v a)) c
x : α
⊢ (fun (x1 x2 : β) ↦ x1 ≤ x2) (max (u x) (v x)) c → (fun (x1 x2 : β) ↦ x1 ≤ x2) (u x) c

Tactic:
simp +contextual only [implies_true, max_le_iff]

Premises used: max_le_iff, implies_true
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
h' : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
inr :
  ∀ (b : β)
    (hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a),
    IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)

Tactic:
rcases h' with ⟨b, hb⟩
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
h :
  ∀ (a : β),
    (∀ᶠ (x : β) in map (fun (a : α) ↦ max (u a) (v a)) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) →
      (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)

Tactic:
use b
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun (a : α) ↦ max (u a) (v a)) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c
h : ∀ᶠ (x : β) in map v f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c
⊢ b ≤ c

Tactic:
apply hb c
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (x : β) in map (fun (a : α) ↦ max (u a) (v a)) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c
h :
  ∀ (hc : ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (max (u a) (v a)) c),
    ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (v a) c
⊢ ∀ᶠ (x : β) in map v f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x c

Tactic:
rw [eventually_map] at hc ⊢

Premises used: Filter.eventually_map
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (max (u a) (v a)) c
⊢ ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (v a) c

Tactic:
hc.mono (fun _ ↦ ?_)

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (max (u a) (v a)) c
h : ∀ (x : α), (fun (x1 x2 : β) ↦ x1 ≤ x2) (max (u x) (v x)) c → (fun (x1 x2 : β) ↦ x1 ≤ x2) (v x) c
⊢ ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (v a) c

Tactic:
refine hc.mono (fun _ ↦ ?_)

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder β
f : Filter α
u v : α → β
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in map v f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun (x1 x2 : β) ↦ x1 ≤ x2) (max (u a) (v a)) c
x : α
⊢ (fun (x1 x2 : β) ↦ x1 ≤ x2) (max (u x) (v x)) c → (fun (x1 x2 : β) ↦ x1 ≤ x2) (v x) c

Tactic:
simp +contextual only [implies_true, max_le_iff]

Premises used: max_le_iff, implies_true
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
choose! :
  ∀ (m : (i : ι) → β) (hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x (m i)),
    IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a

Tactic:
choose! m hm using h
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : (i : ι) → β
hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x (m i)
h :
  ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x (s.sup' hs m)
⊢ IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a

Tactic:
use sup' s hs m

Premises used: Finset.sup'
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : (i : ι) → β
hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x (m i)
h : ∀ (hm : ∀ i ∈ s, ∀ᶠ (a : α) in f, F i a ≤ m i), ∀ᶠ (a : α) in f, (s.sup' hs fun (i : ι) ↦ F i a) ≤ s.sup' hs m
⊢ ∀ᶠ (x : β) in Filter.map (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x (s.sup' hs m)

Tactic:
simp only [eventually_map] at hm ⊢

Premises used: Filter.eventually_map
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : (i : ι) → β
hm : ∀ i ∈ s, ∀ᶠ (a : α) in f, F i a ≤ m i
⊢ ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i

Tactic:
rw [← eventually_all_finset s] at hm

Premises used: Filter.eventually_all_finset
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : (i : ι) → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup' hs fun (i : ι) ↦ F i a) ≤ s.sup' hs m

Tactic:
hm.mono fun a h ↦ ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : (i : ι) → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
h : ∀ (a : α) (h : ∀ i ∈ s, F i a ≤ m i), (s.sup' hs fun (i : ι) ↦ F i a) ≤ s.sup' hs m
⊢ ∀ᶠ (a : α) in f, (s.sup' hs fun (i : ι) ↦ F i a) ≤ s.sup' hs m

Tactic:
refine hm.mono fun a h ↦ ?_

Premises used: Filter.Eventually.mono
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : (i : ι) → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
a : α
h : ∀ i ∈ s, F i a ≤ m i
h₁ : ∀ b ∈ s, F b a ≤ s.sup' hs m
⊢ (s.sup' hs fun (i : ι) ↦ F i a) ≤ s.sup' hs m

Tactic:
simp only [sup'_le_iff]

Premises used: Finset.sup'_le_iff
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : (i : ι) → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
a : α
h : ∀ i ∈ s, F i a ≤ m i
⊢ ∀ b ∈ s, F b a ≤ s.sup' hs m

Tactic:
fun i i_s ↦ le_trans (h i i_s) (le_sup' m i_s)

Premises used: Finset.le_sup', le_trans
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
inst_1 : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : (i : ι) → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
a : α
h : ∀ i ∈ s, F i a ≤ m i
⊢ ∀ b ∈ s, F b a ≤ s.sup' hs m

Tactic:
exact fun i i_s ↦ le_trans (h i i_s) (le_sup' m i_s)

Premises used: Finset.le_sup', le_trans
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h : ∃ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
rcases :
  ∀ (i : ι) (i_s : i ∈ s) (b : β)
    (hb :
      ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun (x1 x2 : β) ↦ x1 ≤ x2) x a) → (fun (x1 x2 : β) ↦ x1 ≤ x2) b a),
    IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a

Tactic:
rcases h with ⟨i, i_s, b, hb⟩