∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {f : Filter α} {u v : α → β},
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) limsup_max._auto_1 →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) limsup_max._auto_3 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) limsup_max._auto_5 →
        autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) limsup_max._auto_7 →
          Filter.limsup (fun a => max (u a) (v a)) f = max (Filter.limsup u f) (Filter.limsup v f)