awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ u a ≥ U) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ v a ≥ V) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ u a + v a ≥ U + V) x} x}
            x}
      a
h₁ h₂ : ∀ (a : α) (hu : u a ≥ U) (hv : v a ≥ V), u a + v a ≥ U + V
⊢ ∀ᶠ (a : α) in f, u a + v a ≥ U + V

Tactic:
filter_upwards [hU, hV] with a hu hv using add_le_add hu hv
-- 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_le : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f u
v_bdd_le : 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_le
-- 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_le : 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_le
-- 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
-- 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
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ u a ≤ U) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ v a ≤ V) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ u a + v a ≤ U + V) x} x}
            x}
      a
h₁ h₂ : ∀ (a : α) (hu : u a ≤ U) (hv : v a ≤ V), u a + v a ≤ U + V
⊢ ∀ᶠ (a : α) in f, u a + v a ≤ U + V

Tactic:
filter_upwards [hU, hV] with a hu hv using add_le_add hu hv
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
κ : Type u_7
inst_1 : AddCommMonoid R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u : κ → α → R
s : Finset κ
⊢ (∀ k ∈ s, IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f (u k)) →
    IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f (∑ k ∈ s, u k)

Tactic:
fun h ↦ isBoundedUnder_sum (fun _ _ ↦ isBoundedUnder_le_add) le_rfl s h

Premises used: le_rfl, Filter.isBoundedUnder_le_add, Filter.isBoundedUnder_sum
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
f : Filter α
R : Type u_6
inst : Preorder R
κ : Type u_7
inst_1 : AddCommMonoid R
inst_2 : AddLeftMono R
inst_3 : AddRightMono R
u : κ → α → R
s : Finset κ
⊢ (∀ k ∈ s, IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u k)) →
    IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (∑ k ∈ s, u k)

Tactic:
fun h ↦ isBoundedUnder_sum (fun _ _ ↦ isBoundedUnder_ge_add) le_rfl s h

Premises used: le_rfl, Filter.isBoundedUnder_sum, Filter.isBoundedUnder_ge_add
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
R : Type u_6
inst : LinearOrder R
inst_1 : Add R
f : Filter α
inst_2 : f.NeBot
inst_3 : AddLeftMono R
inst_4 : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f u
hv : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f v
obtain : ∀ (U : R) (hU : ∀ᶠ (x : α) in f, u x ≤ U), IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)
⊢ IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)

Tactic:
obtain ⟨U, hU⟩ := hu.eventually_le

Premises used: Filter.IsBoundedUnder.eventually_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
R : Type u_6
inst : LinearOrder R
inst_1 : Add R
f : Filter α
inst_2 : f.NeBot
inst_3 : AddLeftMono R
inst_4 : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f u
hv : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f v
U : R
hU : ∀ᶠ (x : α) in f, u x ≤ U
obtain : ∀ (V : R) (hV : ∃ᶠ (x : α) in f, v x ≤ V), IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)
⊢ IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)

Tactic:
obtain ⟨V, hV⟩ := hv.frequently_le

Premises used: Filter.IsCoboundedUnder.frequently_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
R : Type u_6
inst : LinearOrder R
inst_1 : Add R
f : Filter α
inst_2 : f.NeBot
inst_3 : AddLeftMono R
inst_4 : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f u
hv : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f v
U : R
hU : ∀ᶠ (x : α) in f, u x ≤ U
V : R
hV : ∃ᶠ (x : α) in f, v x ≤ V
apply : ∃ᶠ (x : α) in f, (u + v) x ≤ U + V
⊢ IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f (u + v)

Tactic:
apply IsCoboundedUnder.of_frequently_le (a := U + V)

Premises used: Filter.IsCoboundedUnder.of_frequently_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
R : Type u_6
inst : LinearOrder R
inst_1 : Add R
f : Filter α
inst_2 : f.NeBot
inst_3 : AddLeftMono R
inst_4 : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f u
hv : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f v
U : R
hU : ∀ᶠ (x : α) in f, u x ≤ U
V : R
hV : ∃ᶠ (x : α) in f, v x ≤ V
⊢ ∃ᶠ (x : α) in f, (u + v) x ≤ U + V

Tactic:
(hV.and_eventually hU).mono fun x hx ↦ add_le_add hx.2 hx.1

Premises used: add_le_add, Filter.Frequently.mono, Filter.Frequently.and_eventually, And.right, And.left
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
R : Type u_6
inst : LinearOrder R
inst_1 : Add R
f : Filter α
inst_2 : f.NeBot
inst_3 : AddLeftMono R
inst_4 : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f u
hv : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f v
U : R
hU : ∀ᶠ (x : α) in f, u x ≤ U
V : R
hV : ∃ᶠ (x : α) in f, v x ≤ V
⊢ ∃ᶠ (x : α) in f, (u + v) x ≤ U + V

Tactic:
exact (hV.and_eventually hU).mono fun x hx ↦ add_le_add hx.2 hx.1

Premises used: add_le_add, Filter.Frequently.mono, Filter.Frequently.and_eventually, And.right, And.left
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
R : Type u_6
inst : LinearOrder R
inst_1 : Add R
f : Filter α
inst_2 : f.NeBot
inst_3 : AddLeftMono R
inst_4 : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f u
hv : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f v
obtain : ∀ (U : R) (hU : ∀ᶠ (x : α) in f, U ≤ u x), IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f (u + v)
⊢ IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f (u + v)

Tactic:
obtain ⟨U, hU⟩ := hu.eventually_ge

Premises used: Filter.IsBoundedUnder.eventually_ge
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
R : Type u_6
inst : LinearOrder R
inst_1 : Add R
f : Filter α
inst_2 : f.NeBot
inst_3 : AddLeftMono R
inst_4 : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f u
hv : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f v
U : R
hU : ∀ᶠ (x : α) in f, U ≤ u x
obtain : ∀ (V : R) (hV : ∃ᶠ (x : α) in f, V ≤ v x), IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f (u + v)
⊢ IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f (u + v)

Tactic:
obtain ⟨V, hV⟩ := hv.frequently_ge

Premises used: Filter.IsCoboundedUnder.frequently_ge
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
R : Type u_6
inst : LinearOrder R
inst_1 : Add R
f : Filter α
inst_2 : f.NeBot
inst_3 : AddLeftMono R
inst_4 : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f u
hv : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f v
U : R
hU : ∀ᶠ (x : α) in f, U ≤ u x
V : R
hV : ∃ᶠ (x : α) in f, V ≤ v x
apply : ∃ᶠ (x : α) in f, U + V ≤ (u + v) x
⊢ IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f (u + v)

Tactic:
apply IsCoboundedUnder.of_frequently_ge (a := U + V)

Premises used: Filter.IsCoboundedUnder.of_frequently_ge
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
R : Type u_6
inst : LinearOrder R
inst_1 : Add R
f : Filter α
inst_2 : f.NeBot
inst_3 : AddLeftMono R
inst_4 : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f u
hv : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f v
U : R
hU : ∀ᶠ (x : α) in f, U ≤ u x
V : R
hV : ∃ᶠ (x : α) in f, V ≤ v x
⊢ ∃ᶠ (x : α) in f, U + V ≤ (u + v) x

Tactic:
(hV.and_eventually hU).mono fun x hx ↦ add_le_add hx.2 hx.1

Premises used: add_le_add, Filter.Frequently.mono, Filter.Frequently.and_eventually, And.right, And.left
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_5
R : Type u_6
inst : LinearOrder R
inst_1 : Add R
f : Filter α
inst_2 : f.NeBot
inst_3 : AddLeftMono R
inst_4 : AddRightMono R
u v : α → R
hu : IsBoundedUnder (fun (x1 x2 : R) ↦ x1 ≥ x2) f u
hv : IsCoboundedUnder (fun (x1 x2 : R) ↦ x1 ≤ x2) f v
U : R
hU : ∀ᶠ (x : α) in f, U ≤ u x
V : R
hV : ∃ᶠ (x : α) in f, V ≤ v x
⊢ ∃ᶠ (x : α) in f, U + V ≤ (u + v) x

Tactic:
exact (hV.and_eventually hU).mono fun x hx ↦ add_le_add hx.2 hx.1

Premises used: add_le_add, Filter.Frequently.mono, Filter.Frequently.and_eventually, And.right, And.left
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
obtain : ∀ (U : α) (hU : ∀ᶠ (x : ι) in f, u x ≤ U), IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u * v)
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u * v)

Tactic:
obtain ⟨U, hU⟩ := h₂.eventually_le

Premises used: Filter.IsBoundedUnder.eventually_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
obtain : ∀ (V : α) (hV : ∀ᶠ (x : ι) in f, v x ≤ V), IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u * v)
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u * v)

Tactic:
obtain ⟨V, hV⟩ := h₄.eventually_le

Premises used: Filter.IsBoundedUnder.eventually_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u * v)

Tactic:
isBoundedUnder_of_eventually_le (a := U * V) ?_

Premises used: Filter.isBoundedUnder_of_eventually_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
refine : ∀ᶠ (x : ι) in f, (u * v) x ≤ U * V
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u * v)

Tactic:
refine isBoundedUnder_of_eventually_le (a := U * V) ?_

Premises used: Filter.isBoundedUnder_of_eventually_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
h : ∀ (x : ι) (x_U : u x ≤ U) (x_V : v x ≤ V) (v_0 : 0 x ≤ v x), (u * v) x ≤ U * V
⊢ ∀ᶠ (x : ι) in f, (u * v) x ≤ U * V

Tactic:
filter_upwards [hU, hV, h₃] with x x_U x_V v_0
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
v_0 : 0 x ≤ v x
obtain : ∀ (y : ι) (y_0 : 0 ≤ u y) (y_U : u y ≤ U), 0 ≤ U
⊢ 0 ≤ U

Tactic:
obtain ⟨y, y_0, y_U⟩ := (h₁.and_eventually hU).exists

Premises used: Filter.Frequently.and_eventually, Filter.Frequently.exists
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
v_0 : 0 x ≤ v x
y : ι
y_0 : 0 ≤ u y
y_U : u y ≤ U
⊢ 0 ≤ U

Tactic:
y_0.trans y_U

Premises used: LE.le.trans
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
v_0 : 0 x ≤ v x
y : ι
y_0 : 0 ≤ u y
y_U : u y ≤ U
⊢ 0 ≤ U

Tactic:
exact y_0.trans y_U

Premises used: LE.le.trans
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
v_0 : 0 x ≤ v x
⊢ 0 ≤ U

Tactic:
have U_0 : 0 ≤ U := by
    obtain ⟨y, y_0, y_U⟩ := (h₁.and_eventually hU).exists
    exact y_0.trans y_U
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
v_0 : 0 x ≤ v x
U_0 : 0 ≤ U
⊢ (u * v) x ≤ U * V

Tactic:
(mul_le_mul_of_nonneg_right x_U v_0).trans (mul_le_mul_of_nonneg_left x_V U_0)

Premises used: mul_le_mul_of_nonneg_right, LE.le.trans, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : Preorder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
u v : ι → α
h₁ : ∃ᶠ (x : ι) in f, 0 ≤ u x
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∀ᶠ (x : ι) in f, v x ≤ V
x : ι
x_U : u x ≤ U
x_V : v x ≤ V
v_0 : 0 x ≤ v x
U_0 : 0 ≤ U
⊢ (u * v) x ≤ U * V

Tactic:
exact (mul_le_mul_of_nonneg_right x_U v_0).trans (mul_le_mul_of_nonneg_left x_V U_0)

Premises used: mul_le_mul_of_nonneg_right, LE.le.trans, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
inst_5 : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
obtain : ∀ (U : α) (hU : ∀ᶠ (x : ι) in f, u x ≤ U), IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u * v)
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u * v)

Tactic:
obtain ⟨U, hU⟩ := h₂.eventually_le

Premises used: Filter.IsBoundedUnder.eventually_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
inst_5 : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
obtain : ∀ (V : α) (hV : ∃ᶠ (x : ι) in f, v x ≤ V), IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u * v)
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u * v)

Tactic:
obtain ⟨V, hV⟩ := h₄.frequently_le

Premises used: Filter.IsCoboundedUnder.frequently_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
inst_5 : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∃ᶠ (x : ι) in f, v x ≤ V
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u * v)

Tactic:
IsCoboundedUnder.of_frequently_le (a := U * V) ?_

Premises used: Filter.IsCoboundedUnder.of_frequently_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
inst_5 : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∃ᶠ (x : ι) in f, v x ≤ V
refine : ∃ᶠ (x : ι) in f, (u * v) x ≤ U * V
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u * v)

Tactic:
refine IsCoboundedUnder.of_frequently_le (a := U * V) ?_

Premises used: Filter.IsCoboundedUnder.of_frequently_le
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
inst_5 : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∃ᶠ (x : ι) in f, v x ≤ V
apply : ∀ (x : ι), v x ≤ V ∧ u x ≤ U ∧ 0 x ≤ u x ∧ 0 x ≤ v x → (u * v) x ≤ U * V
⊢ ∃ᶠ (x : ι) in f, (u * v) x ≤ U * V

Tactic:
apply (hV.and_eventually (hU.and (h₁.and h₃))).mono

Premises used: Filter.Eventually.and, Filter.Frequently.mono, Filter.Frequently.and_eventually
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
inst_5 : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∃ᶠ (x : ι) in f, v x ≤ V
x : ι
this : ∀ (x_V : v x ≤ V) (x_U : u x ≤ U) (u_0 : 0 x ≤ u x) (v_0 : 0 x ≤ v x), (u * v) x ≤ U * V
⊢ v x ≤ V ∧ u x ≤ U ∧ 0 x ≤ u x ∧ 0 x ≤ v x → (u * v) x ≤ U * V

Tactic:
⟨x_V, x_U, u_0, v_0⟩
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
inst_5 : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∃ᶠ (x : ι) in f, v x ≤ V
x : ι
x_V : v x ≤ V
x_U : u x ≤ U
u_0 : 0 x ≤ u x
v_0 : 0 x ≤ v x
⊢ (u * v) x ≤ U * V

Tactic:
(mul_le_mul_of_nonneg_right x_U v_0).trans (mul_le_mul_of_nonneg_left x_V (u_0.trans x_U))

Premises used: mul_le_mul_of_nonneg_right, LE.le.trans, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
ι : Type u_4
inst : LinearOrder α
inst_1 : Mul α
inst_2 : Zero α
inst_3 : PosMulMono α
inst_4 : MulPosMono α
f : Filter ι
inst_5 : f.NeBot
u v : ι → α
h₁ : 0 ≤ᶠ[f] u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : 0 ≤ᶠ[f] v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
U : α
hU : ∀ᶠ (x : ι) in f, u x ≤ U
V : α
hV : ∃ᶠ (x : ι) in f, v x ≤ V
x : ι
x_V : v x ≤ V
x_U : u x ≤ U
u_0 : 0 x ≤ u x
v_0 : 0 x ≤ v x
⊢ (u * v) x ≤ U * V

Tactic:
exact (mul_le_mul_of_nonneg_right x_U v_0).trans (mul_le_mul_of_nonneg_left x_V (u_0.trans x_U))

Premises used: mul_le_mul_of_nonneg_right, LE.le.trans, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) atBot

Tactic:
‹Nonempty α›.elim fun a => ⟨a, eventually_le_atBot _⟩

Premises used: Nonempty.elim, Exists.intro, Filter.eventually_le_atBot
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ IsBounded (fun (x1 x2 : α) ↦ x1 ≥ x2) atTop

Tactic:
‹Nonempty α›.elim fun a => ⟨a, eventually_ge_atTop _⟩

Premises used: Nonempty.elim, Exists.intro, Filter.eventually_ge_atTop
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
f : Filter β
u : β → α
h : Tendsto u f atBot
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u

Tactic:
isBounded_le_atBot.mono h

Premises used: Filter.isBounded_le_atBot, Filter.IsBounded.mono, Filter.IsBoundedUnder
-- Module: Mathlib.Order.Filter.IsBounded
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Nonempty α
f : Filter β
u : β → α
h : Tendsto u f atTop
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u

Tactic:
isBounded_ge_atTop.mono h

Premises used: Filter.IsBounded.mono, Filter.isBounded_ge_atTop, Filter.IsBoundedUnder