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

Proof state:
case inr.inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
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✝
h✝ : f.NeBot
s_nemp : s.Nonempty
⊢ limsup (fun a => s.sup fun i => F i a) f = limsup (fun a => s.sup' s_nemp fun i => F i a) f

Tactic:
congr

Result:
case inr.inr.e_u
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
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✝
h✝ : f.NeBot
s_nemp : s.Nonempty
⊢ (fun a => s.sup fun i => F i a) = fun a => s.sup' s_nemp fun i => F i a

Proof state:
case inr.inr.e_u.h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
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✝
h✝ : f.NeBot
s_nemp : s.Nonempty
a : α
⊢ (s.sup fun i => F i a) = s.sup' s_nemp fun i => F i a

Tactic:
exact Eq.symm (Finset.sup'_eq_sup s_nemp (fun i ↦ F i a))

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
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✝
h✝ : f.NeBot
⊢ limsup (fun a => s.sup fun i => F i a) f = s.sup fun i => limsup (F i) f

Tactic:
rcases Finset.eq_empty_or_nonempty s with (rfl | s_nemp)

Result:
case inr.inl
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
h✝ : f.NeBot
h₁ : autoParam (∀ i ∈ ∅, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
h₂ : autoParam (∀ i ∈ ∅, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
⊢ limsup (fun a => ∅.sup fun i => F i a) f = ∅.sup fun i => limsup (F i) f

case inr.inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
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✝
h✝ : f.NeBot
s_nemp : s.Nonempty
⊢ limsup (fun a => s.sup fun i => F i a) f = s.sup fun i => limsup (F i) f

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

Tactic:
simp [limsup_eq, csInf_univ]

Result:
no goals

Proof state:
case inr.inr.e_u
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
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✝
h✝ : f.NeBot
s_nemp : s.Nonempty
⊢ (fun a => s.sup fun i => F i a) = fun a => s.sup' s_nemp fun i => F i a

Tactic:
ext a

Result:
case inr.inr.e_u.h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
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✝
h✝ : f.NeBot
s_nemp : s.Nonempty
a : α
⊢ (s.sup fun i => F i a) = s.sup' s_nemp fun i => F i a

Proof state:
case inr.inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
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✝
h✝ : f.NeBot
s_nemp : s.Nonempty
⊢ limsup (fun a => s.sup fun i => F i a) f = s.sup fun i => limsup (F i) f

Tactic:
rw [← Finset.sup'_eq_sup s_nemp fun i ↦ limsup (F i) f, ← limsup_finset_sup' s_nemp h₁ h₂]

Result:
case inr.inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
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✝
h✝ : f.NeBot
s_nemp : s.Nonempty
⊢ limsup (fun a => s.sup fun i => F i a) f = limsup (fun a => s.sup' s_nemp fun i => F i a) f

Proof state:
case inr.inl
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
f : Filter α
F : ι → α → β
h✝ : f.NeBot
h₁ : autoParam (∀ i ∈ ∅, IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
h₂ : autoParam (∀ i ∈ ∅, IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f (F i)) _auto✝
⊢ limsup (fun a => ∅.sup fun i => F i a) f = ∅.sup fun i => limsup (F i) f

Tactic:
simp only [Finset.sup_apply, sup_empty, limsup_const]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
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✝
⊢ limsup (fun a => s.sup fun i => F i a) f = s.sup fun i => limsup (F i) f

Tactic:
rcases eq_or_neBot f with (rfl | _)

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

case inr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderBot β
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✝
h✝ : f.NeBot
⊢ limsup (fun a => s.sup fun i => F i a) f = s.sup fun i => limsup (F i) f