-- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
lemma liminf_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 (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v) _auto✝
h₄ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v) _auto✝
⊢ liminf (u + v) f ≤ limsup u f + liminf v f

Tactic:
have h := isCoboundedUnder_ge_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 (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v) _auto✝
h₄ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v) _auto✝
h : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u + v)
⊢ liminf (u + v) f ≤ limsup u f + liminf v f

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 (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v) _auto✝
h₄ : autoParam (IsCoboundedUnder (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)
⊢ 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 ↦ ?_

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 (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v) _auto✝
h₄ : autoParam (IsCoboundedUnder (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 > liminf v f
x✝ : α
c_ab : x✝ > a + b
⊢ ∃ᶠ (a : ι) in f, (u + v) a < x✝

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 (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v) _auto✝
h₄ : autoParam (IsCoboundedUnder (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 > liminf v f
x✝¹ : α
c_ab : x✝¹ > a + b
x✝ : ι
ab_x : v x✝ < b ∧ u x✝ < a
⊢ (u + v) x✝ < x✝¹

Tactic:
exact (add_lt_add ab_x.2 ab_x.1).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 (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v) _auto✝
h₄ : autoParam (IsCoboundedUnder (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 > liminf v f
x✝ : α
c_ab : x✝ > a + b
⊢ ∃ᶠ (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 ↦ ?_

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 (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v) _auto✝
h₄ : autoParam (IsCoboundedUnder (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 > liminf v f
x✝¹ : α
c_ab : x✝¹ > a + b
x✝ : ι
ab_x : v x✝ < b ∧ u x✝ < a
⊢ (u + v) x✝ < x✝¹

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 (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v) _auto✝
h₄ : autoParam (IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v) _auto✝
h : IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f (u + v)
⊢ liminf (u + v) f ≤ limsup u f + liminf v f

Tactic:
have h' := isBoundedUnder_ge_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 (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v) _auto✝
h₄ : autoParam (IsCoboundedUnder (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)
⊢ liminf (u + v) f ≤ limsup u f + liminf v f