-- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
lemma le_liminf_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 (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 < liminf u f
b : α
b_v : b < liminf v f
c : α
c_ab : c < a + b
⊢ ∀ᶠ (a : ι) in f, c < (u + v) a

Tactic:
filter_upwards [eventually_lt_of_lt_liminf a_u, eventually_lt_of_lt_liminf b_v] with x a_x b_x

Result:
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 (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 < liminf u f
b : α
b_v : b < liminf v f
c : α
c_ab : c < a + b
x : ι
a_x : a < u x
b_x : b < v x
⊢ c < (u + v) x

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 (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 < liminf u f
b : α
b_v : b < liminf v f
c : α
c_ab : c < a + b
x : ι
a_x : a < u x
b_x : b < v x
⊢ c < (u + v) x

Tactic:
exact c_ab.trans (add_lt_add a_x b_x)

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 < liminf u f
b : α
b_v : b < liminf v f
⊢ a + b ≤ liminf (u + v) f

Tactic:
rw [le_liminf_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 (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 < liminf u f
b : α
b_v : b < liminf v f
⊢ ∀ y < a + b, ∀ᶠ (a : ι) in f, y < (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 (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 f + liminf v f ≤ liminf (u + 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 f + liminf v f ≤ liminf (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 (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 f + liminf v f ≤ liminf (u + v) f

Tactic:
refine add_le_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 (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 < liminf u f
b : α
b_v : b < liminf v f
⊢ a + b ≤ liminf (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 (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 f + liminf v f ≤ liminf (u + 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 f + liminf v f ≤ liminf (u + v) f