-- Mathlib/Order/LiminfLimsup.lean
lemma isBoundedUnder_ge_add [Add R] [AddLeftMono R] [AddRightMono R]
    {u v : α → R} (u_bdd_ge : f.IsBoundedUnder (· ≥ ·) u) (v_bdd_ge : f.IsBoundedUnder (· ≥ ·) v) :
    f.IsBoundedUnder (· ≥ ·) (u + v)

Proof state:
case intro
α : Type u_6
f : Filter α
R : Type u_7
inst✝³ : Preorder R
inst✝² : Add R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
v_bdd_ge : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v
U : R
hU : ∀ᶠ (x : R) in map u f, (fun x1 x2 => x1 ≥ x2) x U
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f (u + v)

Tactic:
obtain ⟨V, hV⟩ := v_bdd_ge

Result:
case intro.intro
α : Type u_6
f : Filter α
R : Type u_7
inst✝³ : Preorder R
inst✝² : Add R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
U : R
hU : ∀ᶠ (x : R) in map u f, (fun x1 x2 => x1 ≥ x2) x U
V : R
hV : ∀ᶠ (x : R) in map v f, (fun x1 x2 => x1 ≥ x2) x V
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f (u + v)

Proof state:
case intro.intro
α : Type u_6
f : Filter α
R : Type u_7
inst✝³ : Preorder R
inst✝² : Add R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
U : R
hU : ∀ᶠ (x : R) in map u f, (fun x1 x2 => x1 ≥ x2) x U
V : R
hV : ∀ᶠ (x : R) in map v f, (fun x1 x2 => x1 ≥ x2) x V
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f (u + v)

Tactic:
use U + V

Result:
case h
α : Type u_6
f : Filter α
R : Type u_7
inst✝³ : Preorder R
inst✝² : Add R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
U : R
hU : ∀ᶠ (x : R) in map u f, (fun x1 x2 => x1 ≥ x2) x U
V : R
hV : ∀ᶠ (x : R) in map v f, (fun x1 x2 => x1 ≥ x2) x V
⊢ ∀ᶠ (x : R) in map (u + v) f, (fun x1 x2 => x1 ≥ x2) x (U + V)

Proof state:
case h
α : Type u_6
f : Filter α
R : Type u_7
inst✝³ : Preorder R
inst✝² : Add R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
U V : R
hU : ∀ᶠ (a : α) in f, u a ≥ U
hV : ∀ᶠ (a : α) in f, v a ≥ 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

Result:
no goals

Proof state:
case h
α : Type u_6
f : Filter α
R : Type u_7
inst✝³ : Preorder R
inst✝² : Add R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
U : R
hU : ∀ᶠ (x : R) in map u f, (fun x1 x2 => x1 ≥ x2) x U
V : R
hV : ∀ᶠ (x : R) in map v f, (fun x1 x2 => x1 ≥ x2) x V
⊢ ∀ᶠ (x : R) in map (u + v) f, (fun x1 x2 => x1 ≥ x2) x (U + V)

Tactic:
simp only [eventually_map, Pi.add_apply] at hU hV ⊢

Result:
case h
α : Type u_6
f : Filter α
R : Type u_7
inst✝³ : Preorder R
inst✝² : Add R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
U V : R
hU : ∀ᶠ (a : α) in f, u a ≥ U
hV : ∀ᶠ (a : α) in f, v a ≥ V
⊢ ∀ᶠ (a : α) in f, u a + v a ≥ U + V

Proof state:
α : Type u_6
f : Filter α
R : Type u_7
inst✝³ : Preorder R
inst✝² : Add R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
u_bdd_ge : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u
v_bdd_ge : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f (u + v)

Tactic:
obtain ⟨U, hU⟩ := u_bdd_ge

Result:
case intro
α : Type u_6
f : Filter α
R : Type u_7
inst✝³ : Preorder R
inst✝² : Add R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
u v : α → R
v_bdd_ge : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v
U : R
hU : ∀ᶠ (x : R) in map u f, (fun x1 x2 => x1 ≥ x2) x U
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f (u + v)