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

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

Tactic:
use b

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

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

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

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

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

Tactic:
rw [eventually_map] at hc ⊢

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

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

Tactic:
refine fun c hc ↦ hb c ?_

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

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

Tactic:
rcases h with ⟨i, i_s, b, hb⟩

Result:
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : LinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
i : ι
i_s : i ∈ s
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) b a
⊢ IsCoboundedUnder (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 β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
i : ι
i_s : i ∈ s
b : β
hb : ∀ (a : β), (∀ᶠ (x : β) in Filter.map (F i) f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) b a
c : β
hc : ∀ᶠ (a : α) in f, (fun x1 x2 => x1 ≤ x2) (s.sup' hs fun i => F i a) c
a : α
h : (fun x1 x2 => x1 ≤ x2) (s.sup' hs fun i => F i a) c
⊢ (fun x1 x2 => x1 ≤ x2) (F i a) c

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

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

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

Tactic:
exact h i i_s

Result:
no goals