-- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
lemma limsup_add_le (h₁ : IsBoundedUnder (fun x1 x2 ↦ x1 ≥ x2) f u

Proof state:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : CovariantClass α α (fun a b => a + b) fun x1 x2 => x1 ≤ x2
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
⊢ limsup (u + v) f ≤ limsup u f + limsup v f

Tactic:
have h := isCoboundedUnder_le_add h₁ h₃

Result:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : CovariantClass α α (fun a b => a + b) fun x1 x2 => x1 ≤ x2
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (u + v)
⊢ limsup (u + v) f ≤ limsup u f + limsup v f

Proof state:
case h
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : CovariantClass α α (fun a b => a + b) fun x1 x2 => x1 ≤ x2
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
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

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : CovariantClass α α (fun a b => a + b) fun x1 x2 => x1 ≤ x2
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
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:
refine le_add_of_forall_lt fun a a_u b b_v ↦ ?_

Result:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : CovariantClass α α (fun a b => a + b) fun x1 x2 => x1 ≤ x2
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
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
⊢ limsup (u + v) f ≤ a + b

Proof state:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : CovariantClass α α (fun a b => a + b) fun x1 x2 => x1 ≤ x2
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
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
⊢ limsup (u + v) f ≤ a + b

Tactic:
rw [limsup_le_iff h h']

Result:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : CovariantClass α α (fun a b => a + b) fun x1 x2 => x1 ≤ x2
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
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
⊢ ∀ y > a + b, ∀ᶠ (a : ι) in f, (u + v) a < y

Proof state:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : CovariantClass α α (fun a b => a + b) fun x1 x2 => x1 ≤ x2
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
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
⊢ ∀ y > a + b, ∀ᶠ (a : ι) in f, (u + v) a < y

Tactic:
intro c c_ab

Result:
ι : Type u_1
α : Type u_2
inst✝⁴ : AddCommGroup α
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : DenselyOrdered α
inst✝¹ : CovariantClass α α (fun a b => a + b) fun x1 x2 => x1 ≤ x2
f : Filter ι
inst✝ : f.NeBot
u v : ι → α
h₁ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
h₂ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
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
⊢ ∀ᶠ (a : ι) in f, (u + v) a < c