-- Mathlib/Order/LiminfLimsup.lean
theorem isBoundedUnder_le_finset_sup' [LinearOrder β] [Nonempty β] {f : Filter α} {F : ι → α → β}
    {s : Finset ι} (hs : s.Nonempty) (h : ∀ i ∈ s, f.IsBoundedUnder (· ≤ ·) (F i)) :
    f.IsBoundedUnder (· ≤ ·) (fun a ↦ sup' s hs (fun i ↦ F i a))

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
a : α
h : ∀ i ∈ s, F i a ≤ m i
⊢ (s.sup' hs fun i => F i a) ≤ s.sup' hs m

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

Result:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
a : α
h : ∀ i ∈ s, F i a ≤ m i
⊢ ∀ b ∈ s, F b a ≤ s.sup' hs m

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
a : α
h : ∀ i ∈ s, F i a ≤ m i
⊢ ∀ b ∈ s, F b a ≤ s.sup' hs m

Tactic:
exact fun i i_s ↦ le_trans (h i i_s) (le_sup' m i_s)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun x1 x2 => x1 ≤ x2) x (m i)
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a

Tactic:
use sup' s hs m

Result:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun x1 x2 => x1 ≤ x2) x (m i)
⊢ ∀ᶠ (x : β) in Filter.map (fun a => s.sup' hs fun i => F i a) f, (fun x1 x2 => x1 ≤ x2) x (s.sup' hs m)

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun x1 x2 => x1 ≤ x2) x (m i)
⊢ ∀ᶠ (x : β) in Filter.map (fun a => s.sup' hs fun i => F i a) f, (fun x1 x2 => x1 ≤ x2) x (s.sup' hs m)

Tactic:
simp only [eventually_map] at hm ⊢

Result:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ i ∈ s, ∀ᶠ (a : α) in f, F i a ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup' hs fun i => F i a) ≤ s.sup' hs m

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

Tactic:
choose! m hm using h

Result:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun x1 x2 => x1 ≤ x2) x (m i)
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun a => s.sup' hs fun i => F i a

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup' hs fun i => F i a) ≤ s.sup' hs m

Tactic:
refine hm.mono fun a h ↦ ?_

Result:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
a : α
h : ∀ i ∈ s, F i a ≤ m i
⊢ (s.sup' hs fun i => F i a) ≤ s.sup' hs m

Proof state:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ i ∈ s, ∀ᶠ (a : α) in f, F i a ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup' hs fun i => F i a) ≤ s.sup' hs m

Tactic:
rw [← eventually_all_finset s] at hm

Result:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ᶠ (x : α) in f, ∀ i ∈ s, F i x ≤ m i
⊢ ∀ᶠ (a : α) in f, (s.sup' hs fun i => F i a) ≤ s.sup' hs m