awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
a : α
a_u : a < limsup u f
b : α
b_v : b < liminf v f
c : α
c_ab : c < a + b
x : ι
ab_x : a < u x ∧ b < v x
⊢ c < (u + v) x

Tactic:
c_ab.trans (add_lt_add ab_x.1 ab_x.2)

Premises used: add_lt_add, And.right, And.left, LT.lt.trans
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
a : α
a_u : a < limsup u f
b : α
b_v : b < liminf v f
c : α
c_ab : c < a + b
x : ι
ab_x : a < u x ∧ b < v x
⊢ c < (u + v) x

Tactic:
exact c_ab.trans (add_lt_add ab_x.1 ab_x.2)

Premises used: add_lt_add, And.right, And.left, LT.lt.trans
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)

Tactic:
have h := isCoboundedUnder_le_add h₁ h₃
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)

Tactic:
have h' := isBoundedUnder_le_add h₂ h₄
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
⊢ limsup (u + v) f ≤ limsup u f + limsup v f

Tactic:
le_add_of_forall_lt fun a a_u b b_v ↦ ?_

Premises used: le_add_of_forall_lt
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
refine : ∀ (a : α) (a_u : a > limsup u f) (b : α) (b_v : b > limsup v f), limsup (u + v) f ≤ a + b
⊢ limsup (u + v) f ≤ limsup u f + limsup v f

Tactic:
refine le_add_of_forall_lt fun a a_u b b_v ↦ ?_

Premises used: le_add_of_forall_lt
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
a : α
a_u : a > limsup u f
b : α
b_v : b > limsup v f
rw : ∀ y > a + b, ∀ᶠ (a : ι) in f, (u + v) a < y
⊢ limsup (u + v) f ≤ a + b

Tactic:
rw [limsup_le_iff h h']

Premises used: Filter.limsup_le_iff
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
a : α
a_u : a > limsup u f
b : α
b_v : b > limsup v f
c : α
c_ab : c > a + b
h₅ : ∀ (x : ι) (a_x : u x < a) (b_x : v x < b), (u + v) x < c
⊢ ∀ᶠ (a : ι) in f, (u + v) a < c

Tactic:
filter_upwards [eventually_lt_of_limsup_lt a_u, eventually_lt_of_limsup_lt b_v] with x a_x b_x

Premises used: Filter.eventually_lt_of_limsup_lt
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
a : α
a_u : a > limsup u f
b : α
b_v : b > limsup v f
c : α
c_ab : c > a + b
x : ι
a_x : u x < a
b_x : v x < b
⊢ (u + v) x < c

Tactic:
(add_lt_add a_x b_x).trans c_ab

Premises used: add_lt_add, LT.lt.trans
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h₄ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f (u + v)
a : α
a_u : a > limsup u f
b : α
b_v : b > limsup v f
c : α
c_ab : c > a + b
x : ι
a_x : u x < a
b_x : v x < b
⊢ (u + v) x < c

Tactic:
exact (add_lt_add a_x b_x).trans c_ab

Premises used: add_lt_add, LT.lt.trans
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)

Tactic:
have h := isCoboundedUnder_ge_add h₂ h₄
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)

Tactic:
have h' := isBoundedUnder_ge_add h₁ h₃
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
⊢ liminf u f + liminf v f ≤ liminf (u + v) f

Tactic:
add_le_of_forall_lt fun a a_u b b_v ↦ ?_

Premises used: add_le_of_forall_lt
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
refine : ∀ (a : α) (a_u : a < liminf u f) (b : α) (b_v : b < liminf v f), a + b ≤ liminf (u + v) f
⊢ liminf u f + liminf v f ≤ liminf (u + v) f

Tactic:
refine add_le_of_forall_lt fun a a_u b b_v ↦ ?_

Premises used: add_le_of_forall_lt
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
a : α
a_u : a < liminf u f
b : α
b_v : b < liminf v f
rw : ∀ y < a + b, ∀ᶠ (a : ι) in f, y < (u + v) a
⊢ a + b ≤ liminf (u + v) f

Tactic:
rw [le_liminf_iff h h']

Premises used: Filter.le_liminf_iff
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
a : α
a_u : a < liminf u f
b : α
b_v : b < liminf v f
c : α
c_ab : c < a + b
h₅ : ∀ (x : ι) (a_x : a < u x) (b_x : b < v x), c < (u + v) x
⊢ ∀ᶠ (a : ι) in f, c < (u + v) a

Tactic:
filter_upwards [eventually_lt_of_lt_liminf a_u, eventually_lt_of_lt_liminf b_v] with x a_x b_x

Premises used: Filter.eventually_lt_of_lt_liminf
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
a : α
a_u : a < liminf u f
b : α
b_v : b < liminf v f
c : α
c_ab : c < a + b
x : ι
a_x : a < u x
b_x : b < v x
⊢ c < (u + v) x

Tactic:
c_ab.trans (add_lt_add a_x b_x)

Premises used: add_lt_add, LT.lt.trans
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
a : α
a_u : a < liminf u f
b : α
b_v : b < liminf v f
c : α
c_ab : c < a + b
x : ι
a_x : a < u x
b_x : b < v x
⊢ c < (u + v) x

Tactic:
exact c_ab.trans (add_lt_add a_x b_x)

Premises used: add_lt_add, LT.lt.trans
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
⊢ liminf (u + v) f ≤ limsup u f + liminf v f

Tactic:
le_add_of_forall_lt fun a a_u b b_v ↦ (liminf_le_iff h h').2 fun _ c_ab ↦ ?_

Premises used: Iff.mpr, le_add_of_forall_lt, Filter.liminf_le_iff
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
refine :
  ∀ (a : α) (a_u : a > limsup u f) (b : α) (b_v : b > liminf v f) (x : α) (c_ab : x > a + b),
    ∃ᶠ (a : ι) in f, (u + v) a < x
⊢ liminf (u + v) f ≤ limsup u f + liminf v f

Tactic:
refine le_add_of_forall_lt fun a a_u b b_v ↦ (liminf_le_iff h h').2 fun _ c_ab ↦ ?_

Premises used: Iff.mpr, le_add_of_forall_lt, Filter.liminf_le_iff
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
a : α
a_u : a > limsup u f
b : α
b_v : b > liminf v f
x : α
c_ab : x > a + b
⊢ ∃ᶠ (a : ι) in f, (u + v) a < x

Tactic:
((frequently_lt_of_liminf_lt h₄ b_v).and_eventually
    (eventually_lt_of_limsup_lt a_u h₂)).mono fun _ ab_x ↦ ?_

Premises used: Filter.eventually_lt_of_limsup_lt, Filter.Frequently.mono, Filter.Frequently.and_eventually, Filter.frequently_lt_of_liminf_lt
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
a : α
a_u : a > limsup u f
b : α
b_v : b > liminf v f
x : α
c_ab : x > a + b
refine : ∀ (x_1 : ι) (ab_x : v x_1 < b ∧ u x_1 < a), (u + v) x_1 < x
⊢ ∃ᶠ (a : ι) in f, (u + v) a < x

Tactic:
refine ((frequently_lt_of_liminf_lt h₄ b_v).and_eventually
    (eventually_lt_of_limsup_lt a_u h₂)).mono fun _ ab_x ↦ ?_

Premises used: Filter.eventually_lt_of_limsup_lt, Filter.Frequently.mono, Filter.Frequently.and_eventually, Filter.frequently_lt_of_liminf_lt
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
a : α
a_u : a > limsup u f
b : α
b_v : b > liminf v f
x : α
c_ab : x > a + b
x_1 : ι
ab_x : v x_1 < b ∧ u x_1 < a
⊢ (u + v) x_1 < x

Tactic:
(add_lt_add ab_x.2 ab_x.1).trans c_ab

Premises used: add_lt_add, And.right, And.left, LT.lt.trans
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommGroup α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : DenselyOrdered α
inst_3 : AddLeftMono α
f : Filter ι
inst_4 : f.NeBot
u v : ι → α
h₁ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u
h₃ : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h₄ : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f v
h : IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
h' : IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f (u + v)
a : α
a_u : a > limsup u f
b : α
b_v : b > liminf v f
x : α
c_ab : x > a + b
x_1 : ι
ab_x : v x_1 < b ∧ u x_1 < a
⊢ (u + v) x_1 < x

Tactic:
exact (add_lt_add ab_x.2 ab_x.1).trans c_ab

Premises used: add_lt_add, And.right, And.left, LT.lt.trans
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
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
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x

Tactic:
have h := IsCoboundedUnder.of_frequently_ge (a := 0)
    <| (h₁.and_eventually h₃).mono fun x ⟨ux_0, vx_0⟩ ↦ mul_nonneg ux_0 vx_0
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
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
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)

Tactic:
have h' := isBoundedUnder_le_mul_of_nonneg h₁ h₂ h₃ h₄
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
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
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
⊢ 0 ≤ limsup u f

Tactic:
have u0 : 0 ≤ limsup u f := le_limsup_of_frequently_le h₁ h₂
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
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
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
u0 : 0 ≤ limsup u f
⊢ 0 ≤ limsup (u * v) f

Tactic:
have uv : 0 ≤ limsup (u * v) f :=
    le_limsup_of_frequently_le ((h₁.and_eventually h₃).mono fun _ ⟨hu, hv⟩ ↦ mul_nonneg hu hv) h'
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
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
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
u0 : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
mul_le_of_forall_lt_of_nonneg u0 uv fun a a0 au b b0 bv ↦ ?_

Premises used: mul_le_of_forall_lt_of_nonneg
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
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
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
u0 : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
refine :
  ∀ (a : ℝ) (a0 : a ≥ 0) (au : a < limsup u f) (b : ℝ) (b0 : b ≥ 0) (bv : b < liminf v f), a * b ≤ limsup (u * v) f
⊢ limsup u f * liminf v f ≤ limsup (u * v) f

Tactic:
refine mul_le_of_forall_lt_of_nonneg u0 uv fun a a0 au b b0 bv ↦ ?_

Premises used: mul_le_of_forall_lt_of_nonneg
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
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
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
u0 : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
a : ℝ
a0 : a ≥ 0
au : a < limsup u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
⊢ a * b ≤ limsup (u * v) f

Tactic:
(le_limsup_iff h h').2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, Filter.le_limsup_iff
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
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
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
u0 : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
a : ℝ
a0 : a ≥ 0
au : a < limsup u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
refine : ∀ (c : ℝ) (c_ab : c < a * b), ∃ᶠ (a : ι) in f, c < u a * v a
⊢ a * b ≤ limsup (u * v) f

Tactic:
refine (le_limsup_iff h h').2 fun c c_ab ↦ ?_

Premises used: Iff.mpr, Filter.le_limsup_iff
-- Module: Mathlib.Topology.Algebra.Order.LiminfLimsup
Goal:
ι : Type u_1
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
h : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f fun (x : ι) ↦ u x * v x
h' : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f (u * v)
u0 : 0 ≤ limsup u f
uv : 0 ≤ limsup (u * v) f
a : ℝ
a0 : a ≥ 0
au : a < limsup u f
b : ℝ
b0 : b ≥ 0
bv : b < liminf v f
c : ℝ
c_ab : c < a * b
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) f u

Tactic:
replace h₁ := IsCoboundedUnder.of_frequently_ge h₁