-- Mathlib/Order/LiminfLimsup.lean
lemma isCoboundedUnder_ge_add (hu : f.IsBoundedUnder (· ≤ ·) u)
    (hv : f.IsCoboundedUnder (· ≥ ·) v) :
    f.IsCoboundedUnder (· ≥ ·) (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 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

Result:
no goals

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 x ≤ U
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u + v)

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

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 x ≤ U
V : R
hV : ∃ᶠ (x : α) in f, v x ≤ V
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u + v)

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_le

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 x ≤ U
⊢ 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 x ≤ U
V : R
hV : ∃ᶠ (x : α) in f, v x ≤ V
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u + v)

Tactic:
apply IsCoboundedUnder.of_frequently_le (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 x ≤ U
V : R
hV : ∃ᶠ (x : α) in f, v x ≤ V
⊢ ∃ᶠ (x : α) in f, (u + v) x ≤ U + V