-- 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 intro
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
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✝
i : ι
i_s : i ∈ s
bddsup : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' ⋯ fun i => F i a
⊢ ∃ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)

Tactic:
use i, i_s

Result:
case right
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
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✝
i : ι
i_s : i ∈ s
bddsup : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' ⋯ fun i => F i a
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (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
⊢ limsup (fun a => s.sup' hs fun i => F i a) f ≤ s.sup' hs fun i => limsup (F i) f

Tactic:
refine (limsup_le_iff cobddsup bddsup).2 (fun b hb ↦ ?_)

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
⊢ ∀ᶠ (a : α) in f, (s.sup' hs fun i => F i a) < b

Proof state:
case h.refine_2
α : 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
⊢ ∀ y ∈ ⋂ i ∈ s, {a | F i a < b}, (s.sup' hs fun i => F i y) < b

Tactic:
simp only [mem_iInter, mem_setOf_eq, Finset.sup'_apply, sup'_lt_iff, imp_self, implies_true]

Result:
no goals

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
⊢ (s.sup' hs fun i => limsup (F i) f) ≤ limsup (fun a => s.sup' hs fun i => F i a) f

Tactic:
apply Finset.sup'_le hs (fun i ↦ limsup (F i) f)

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
⊢ ∀ b ∈ s, limsup (F b) f ≤ limsup (fun a => s.sup' hs fun i => F i a) 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
h₃ : ∃ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)
⊢ limsup (fun a => s.sup' hs fun i => F i a) f ≤ s.sup' hs fun i => limsup (F i) f

Tactic:
have cobddsup := isCoboundedUnder_le_finset_sup' hs h₃

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
⊢ 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
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

Tactic:
exact lt_of_le_of_lt (Finset.le_sup' (f := fun i ↦ limsup (F i) f) i_s) hb

Result:
no goals

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
⊢ ∃ v ∈ f, ∀ y ∈ v, (s.sup' hs fun i => F i y) < b

Tactic:
use ⋂ i ∈ s, {a | F i a < b}

Result:
case h
α : 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 ∧ ∀ y ∈ ⋂ i ∈ s, {a | F i a < b}, (s.sup' hs fun i => F i y) < b