-- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
lemma le_limsup_add (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 (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsBoundedUnder (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 < liminf v f
c : α
c_ab : c < a + b
⊢ ∃ᶠ (a : ι) in f, c < (u + v) a

Tactic:
refine ((frequently_lt_of_lt_limsup h₂ a_u).and_eventually
  (eventually_lt_of_lt_liminf b_v 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 (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsBoundedUnder (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 < liminf v f
c : α
c_ab : c < a + b
x✝ : ι
ab_x : a < u x✝ ∧ b < v x✝
⊢ c < (u + v) 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 (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsBoundedUnder (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 (v + u)
h' : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (v + u)
⊢ limsup u f + liminf v f ≤ limsup (u + v) f

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

Tactic:
refine add_le_of_forall_lt fun a a_u b b_v ↦ (le_limsup_iff h h').2 fun 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 (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsBoundedUnder (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 < liminf v f
c : α
c_ab : c < a + b
⊢ ∃ᶠ (a : ι) in f, c < (u + v) a

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

Tactic:
have h' := isBoundedUnder_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 (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsBoundedUnder (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 (v + u)
h' : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (v + u)
⊢ limsup u f + liminf v f ≤ limsup (u + 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 (IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h₃ : autoParam (IsBoundedUnder (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 < liminf v f
c : α
c_ab : c < a + b
x✝ : ι
ab_x : a < u x✝ ∧ b < v x✝
⊢ c < (u + v) x✝

Tactic:
exact c_ab.trans (add_lt_add ab_x.1 ab_x.2)

Result:
no goals