-- Mathlib/Order/LiminfLimsup.lean
theorem limsup_finset_sup' [ConditionallyCompleteLinearOrder β] {f : Filter α}
    {F : ι → α → β} {s : Finset ι} (hs : s.Nonempty)
    (h₁ : ∀ i ∈ s, f.IsCoboundedUnder (· ≤ ·) (F i)

Proof state:
case a
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
bddsup : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
h₃ : ∃ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)
cobddsup : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
b : β
hb : b > s.sup' hs fun i => limsup (F i) f
⊢ ∀ᶠ (a : α) in f, (s.sup' hs fun i => F i a) < b

Tactic:
rw [eventually_iff_exists_mem]

Result:
case a
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
bddsup : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
h₃ : ∃ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)
cobddsup : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
b : β
hb : b > s.sup' hs fun i => limsup (F i) f
⊢ ∃ v ∈ f, ∀ y ∈ v, (s.sup' hs fun i => F i y) < b

Proof state:
case h.refine_1
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
bddsup : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
h₃ : ∃ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)
cobddsup : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
b : β
hb : b > s.sup' hs fun i => limsup (F i) f
i : ι
i_s : i ∈ s
⊢ ∀ᶠ (a : α) in f, F i a < b

Tactic:
apply eventually_lt_of_limsup_lt _ (h₂ i i_s)

Result:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
bddsup : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
h₃ : ∃ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)
cobddsup : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
b : β
hb : b > s.sup' hs fun i => limsup (F i) f
i : ι
i_s : i ∈ s
⊢ limsup (F i) f < b

Proof state:
case h.refine_1
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
bddsup : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
h₃ : ∃ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)
cobddsup : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
b : β
hb : b > s.sup' hs fun i => limsup (F i) f
⊢ ⋂ i ∈ s, {a | F i a < b} ∈ f

Tactic:
rw [biInter_finset_mem]

Result:
case h.refine_1
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
bddsup : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
h₃ : ∃ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)
cobddsup : IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
b : β
hb : b > s.sup' hs fun i => limsup (F i) f
⊢ ∀ i ∈ s, {a | F i a < b} ∈ f

Proof state:
case a
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
bddsup : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
⊢ ∀ b ∈ s, limsup (F b) f ≤ limsup (fun a => s.sup' hs fun i => F i a) f

Tactic:
refine fun i i_s ↦ limsup_le_limsup (Eventually.of_forall (fun a ↦ ?_)) (h₁ i i_s) bddsup

Result:
case a
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
bddsup : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
i : ι
i_s : i ∈ s
a : α
⊢ F i a ≤ (fun a => s.sup' hs fun i => F i a) a

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
⊢ limsup (fun a => s.sup' hs fun i => F i a) f = s.sup' hs fun i => limsup (F i) f

Tactic:
have bddsup := isBoundedUnder_le_finset_sup' hs h₂

Result:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
bddsup : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
⊢ limsup (fun a => s.sup' hs fun i => F i a) f = s.sup' hs fun i => limsup (F i) f

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
bddsup : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
⊢ limsup (fun a => s.sup' hs fun i => F i a) f = s.sup' hs fun i => limsup (F i) f

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
bddsup : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
⊢ limsup (fun a => s.sup' hs fun i => F i a) f ≤ s.sup' hs fun i => limsup (F i) f

case a
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : autoParam (∀ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
h₂ : autoParam (∀ i ∈ s, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
bddsup : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
⊢ (s.sup' hs fun i => limsup (F i) f) ≤ limsup (fun a => s.sup' hs fun i => F i a) f