-- Mathlib/Order/LiminfLimsup.lean
lemma isCoboundedUnder_le_add (hu : f.IsBoundedUnder (· ≥ ·) u)
    (hv : f.IsCoboundedUnder (· ≤ ·) v) :
    f.IsCoboundedUnder (· ≤ ·) (u + v)

Proof state:
case intro
α : Type u_6
R : Type u_7
inst✝⁴ : LinearOrder R
inst✝³ : Add R
f : Filter α
inst✝² : f.NeBot
inst✝¹ : CovariantClass R R (fun a b => a + b) fun x1 x2 => x1 ≤ x2
inst✝ : CovariantClass R R (fun a b => b + a) fun x1 x2 => x1 ≤ x2
u v : α → R
hu : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u
hv : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v
U : R
hU : ∀ᶠ (x : α) in f, U ≤ u x
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (u + v)

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

Result:
case intro.intro
α : Type u_6
R : Type u_7
inst✝⁴ : LinearOrder R
inst✝³ : Add R
f : Filter α
inst✝² : f.NeBot
inst✝¹ : CovariantClass R R (fun a b => a + b) fun x1 x2 => x1 ≤ x2
inst✝ : CovariantClass R R (fun a b => b + a) fun x1 x2 => x1 ≤ x2
u v : α → R
hu : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u
hv : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v
U : R
hU : ∀ᶠ (x : α) in f, U ≤ u x
V : R
hV : ∃ᶠ (x : α) in f, V ≤ v x
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (u + v)

Proof state:
case intro.intro
α : Type u_6
R : Type u_7
inst✝⁴ : LinearOrder R
inst✝³ : Add R
f : Filter α
inst✝² : f.NeBot
inst✝¹ : CovariantClass R R (fun a b => a + b) fun x1 x2 => x1 ≤ x2
inst✝ : CovariantClass R R (fun a b => b + a) fun x1 x2 => x1 ≤ x2
u v : α → R
hu : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u
hv : IsCoboundedUnder (fun x1 x2 => 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

Result:
no goals

Proof state:
case intro.intro
α : Type u_6
R : Type u_7
inst✝⁴ : LinearOrder R
inst✝³ : Add R
f : Filter α
inst✝² : f.NeBot
inst✝¹ : CovariantClass R R (fun a b => a + b) fun x1 x2 => x1 ≤ x2
inst✝ : CovariantClass R R (fun a b => b + a) fun x1 x2 => x1 ≤ x2
u v : α → R
hu : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u
hv : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v
U : R
hU : ∀ᶠ (x : α) in f, U ≤ u x
V : R
hV : ∃ᶠ (x : α) in f, V ≤ v x
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (u + v)

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

Result:
case intro.intro
α : Type u_6
R : Type u_7
inst✝⁴ : LinearOrder R
inst✝³ : Add R
f : Filter α
inst✝² : f.NeBot
inst✝¹ : CovariantClass R R (fun a b => a + b) fun x1 x2 => x1 ≤ x2
inst✝ : CovariantClass R R (fun a b => b + a) fun x1 x2 => x1 ≤ x2
u v : α → R
hu : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u
hv : IsCoboundedUnder (fun x1 x2 => 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

Proof state:
α : Type u_6
R : Type u_7
inst✝⁴ : LinearOrder R
inst✝³ : Add R
f : Filter α
inst✝² : f.NeBot
inst✝¹ : CovariantClass R R (fun a b => a + b) fun x1 x2 => x1 ≤ x2
inst✝ : CovariantClass R R (fun a b => b + a) fun x1 x2 => x1 ≤ x2
u v : α → R
hu : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u
hv : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (u + v)

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

Result:
case intro
α : Type u_6
R : Type u_7
inst✝⁴ : LinearOrder R
inst✝³ : Add R
f : Filter α
inst✝² : f.NeBot
inst✝¹ : CovariantClass R R (fun a b => a + b) fun x1 x2 => x1 ≤ x2
inst✝ : CovariantClass R R (fun a b => b + a) fun x1 x2 => x1 ≤ x2
u v : α → R
hu : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u
hv : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v
U : R
hU : ∀ᶠ (x : α) in f, U ≤ u x
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (u + v)