-- Mathlib/Order/LiminfLimsup.lean
theorem limsup_max [ConditionallyCompleteLinearOrder β] {f : Filter α} {u v : α → β}
    (h₁ : f.IsCoboundedUnder (· ≤ ·) u

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : autoParam (IsCoboundedUnder (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 u) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
bddmax : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
cobddmax : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
b : β
hb : b > limsup u f ⊔ limsup v f
⊢ ∀ᶠ (a : α) in f, u a ⊔ v a < b

Tactic:
have hu := eventually_lt_of_limsup_lt (lt_of_le_of_lt (le_max_left _ _) hb) h₃

Result:
case a
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : autoParam (IsCoboundedUnder (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 u) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
bddmax : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
cobddmax : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
b : β
hb : b > limsup u f ⊔ limsup v f
hu : ∀ᶠ (a : α) in f, u a < b
⊢ ∀ᶠ (a : α) in f, u a ⊔ v a < b

Proof state:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : autoParam (IsCoboundedUnder (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 u) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
bddmax : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
⊢ limsup (fun a => u a ⊔ v a) f = limsup u f ⊔ limsup v f

Tactic:
have cobddmax := isCoboundedUnder_le_max (v := v) (Or.inl h₁)

Result:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : autoParam (IsCoboundedUnder (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 u) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
bddmax : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
cobddmax : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
⊢ limsup (fun a => u a ⊔ v a) f = limsup u f ⊔ limsup v f

Proof state:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : autoParam (IsCoboundedUnder (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 u) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
bddmax : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
cobddmax : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
⊢ limsup (fun a => u a ⊔ v a) f = limsup u f ⊔ limsup v f

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : autoParam (IsCoboundedUnder (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 u) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
bddmax : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
cobddmax : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
⊢ limsup (fun a => u a ⊔ v a) f ≤ limsup u f ⊔ limsup v f

case a
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : autoParam (IsCoboundedUnder (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 u) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
bddmax : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
cobddmax : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
⊢ limsup u f ⊔ limsup v f ≤ limsup (fun a => u a ⊔ v a) f

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : autoParam (IsCoboundedUnder (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 u) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
bddmax : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
cobddmax : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
b : β
hb : b > limsup u f ⊔ limsup v f
hu : ∀ᶠ (a : α) in f, u a < b
⊢ ∀ᶠ (a : α) in f, u a ⊔ v a < b

Tactic:
have hv := eventually_lt_of_limsup_lt (lt_of_le_of_lt (le_max_right _ _) hb) h₄

Result:
case a
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : autoParam (IsCoboundedUnder (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 u) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
bddmax : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
cobddmax : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
b : β
hb : b > limsup u f ⊔ limsup v f
hu : ∀ᶠ (a : α) in f, u a < b
hv : ∀ᶠ (a : α) in f, v a < b
⊢ ∀ᶠ (a : α) in f, u a ⊔ v a < b

Proof state:
case a
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : autoParam (IsCoboundedUnder (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 u) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
bddmax : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
cobddmax : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
⊢ limsup (fun a => u a ⊔ v a) f ≤ limsup u f ⊔ limsup v f

Tactic:
refine (limsup_le_iff cobddmax bddmax).2 (fun b hb ↦ ?_)

Result:
case a
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : autoParam (IsCoboundedUnder (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 u) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
bddmax : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
cobddmax : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
b : β
hb : b > limsup u f ⊔ limsup v f
⊢ ∀ᶠ (a : α) in f, u a ⊔ v a < b

Proof state:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : autoParam (IsCoboundedUnder (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 u) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
⊢ limsup (fun a => u a ⊔ v a) f = limsup u f ⊔ limsup v f

Tactic:
have bddmax := IsBoundedUnder.sup h₃ h₄

Result:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : autoParam (IsCoboundedUnder (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 u) _auto✝
h₄ : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) _auto✝
bddmax : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => u a ⊔ v a
⊢ limsup (fun a => u a ⊔ v a) f = limsup u f ⊔ limsup v f