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

Tactic:
exact h₁ i i_s

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
i : ι
i_s : i ∈ s
a : α
⊢ ∃ b ∈ s, F i a ≤ F b a

Tactic:
use i, i_s

Result:
no goals

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 : α) in f, F i a < b

Tactic:
intro i i_s

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 : ι
i_s : i ∈ s
⊢ ∀ᶠ (a : α) in f, F i a < b

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
i : ι
i_s : i ∈ s
a : α
⊢ F i a ≤ (fun a => s.sup' hs fun i => F i a) a

Tactic:
simp only [Finset.sup'_apply, le_sup'_iff]

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 : α
⊢ ∃ b ∈ s, F i a ≤ F b 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✝
bddsup : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a
⊢ ∃ i ∈ s, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)

Tactic:
rcases hs with ⟨i, i_s⟩

Result:
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)

Proof state:
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

Tactic:
split_ands

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

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

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:
suffices key : ∀ i ∈ s, ∀ᶠ a in f, F i a < b from fun i i_s ↦ eventually_iff.1 (key i i_s)

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 : α) in f, F i a < b