awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
b : β
hb : b > max (limsup u f) (limsup v f)
hu : ∀ᶠ (a : α) in f, u a < b
hv : ∀ᶠ (a : α) in f, v a < b
⊢ ∀ᶠ (a : α) in f, max (u a) (v a) < b

Tactic:
refine mem_of_superset (inter_mem hu hv) (fun _ ↦ by simp)

Premises used: Filter.inter_mem, Filter.mem_of_superset
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
⊢ max (limsup u f) (limsup v f) ≤ limsup (fun (a : α) ↦ max (u a) (v a)) f

Tactic:
max_le (c := limsup (fun a ↦ max (u a) (v a)) f)
      (limsup_le_limsup (Eventually.of_forall (fun a : α ↦ le_max_left (u a) (v a))) h₁ bddmax)
      (limsup_le_limsup (Eventually.of_forall (fun a : α ↦ le_max_right (u a) (v a))) h₂ bddmax)

Premises used: le_max_right, Filter.Eventually.of_forall, max_le, Filter.limsup_le_limsup, le_max_left
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h₃ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₄ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
bddmax : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
cobddmax : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ max (u a) (v a)
⊢ max (limsup u f) (limsup v f) ≤ limsup (fun (a : α) ↦ max (u a) (v a)) f

Tactic:
exact max_le (c := limsup (fun a ↦ max (u a) (v a)) f)
      (limsup_le_limsup (Eventually.of_forall (fun a : α ↦ le_max_left (u a) (v a))) h₁ bddmax)
      (limsup_le_limsup (Eventually.of_forall (fun a : α ↦ le_max_right (u a) (v a))) h₂ bddmax)

Premises used: le_max_right, Filter.Eventually.of_forall, max_le, Filter.limsup_le_limsup, le_max_left
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f v
h₃ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₄ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f v
⊢ liminf (fun (a : α) ↦ min (u a) (v a)) f = min (liminf u f) (liminf v f)

Tactic:
limsup_max (β := βᵒᵈ) h₁ h₂ h₃ h₄

Premises used: Filter.limsInf, Filter.liminf, setOf, limsup_max, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
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:
have bddsup := isBoundedUnder_le_finset_sup' hs h₂
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
a :
  LE.le.{u_2} (α := β) (limsup (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f) (s.sup' hs fun (i : ι) ↦ limsup (F i) f)
a₁ :
  LE.le.{u_2} (α := β) (s.sup' hs fun (i : ι) ↦ limsup (F i) f) (limsup (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f)
⊢ Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f)
    (s.sup' hs fun (i : ι) ↦ limsup (F i) f)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
rcases :
  ∀ (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)
⊢ ∃ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)

Tactic:
rcases hs with ⟨i, i_s⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
i : ι
i_s : i ∈ s
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' ⋯ fun (i : ι) ↦ F i a
right : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
⊢ ∃ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)

Tactic:
use i, i_s
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
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:
h₁ i i_s
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
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
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
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:
have h₃ : ∃ i ∈ s, f.IsCoboundedUnder (· ≤ ·) (F i) := by
      rcases hs with ⟨i, i_s⟩
      use i, i_s
      exact h₁ i i_s
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
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)
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a

Tactic:
have cobddsup := isCoboundedUnder_le_finset_sup' hs h₃
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
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
⊢ LE.le.{u_2} (α := β) (limsup (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f) (s.sup' hs fun (i : ι) ↦ limsup (F i) f)

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

Premises used: Iff.mpr, Filter.limsup_le_iff
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
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
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
⊢ LE.le.{u_2} (α := β) (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 ↦ ?_)

Premises used: Iff.mpr, Filter.limsup_le_iff
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
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 : ∀ (hb : ∀ i ∈ s, limsup (F i) f < b), ∀ i ∈ s, ∀ᶠ (x : α) in f, F i x < b
⊢ ∀ᶠ (a : α) in f, (s.sup' hs fun (i : ι) ↦ F i a) < b

Tactic:
simp only [gt_iff_lt, sup'_lt_iff, eventually_all_finset] at hb ⊢

Premises used: Finset.sup'_lt_iff, Filter.eventually_all_finset, gt_iff_lt
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
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 : ∀ i ∈ s, limsup (F i) f < b
⊢ ∀ i ∈ s, ∀ᶠ (x : α) in f, F i x < b

Tactic:
fun i i_s ↦ eventually_lt_of_limsup_lt (hb i i_s) (h₂ i i_s)

Premises used: Filter.eventually_lt_of_limsup_lt
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
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 : ∀ i ∈ s, limsup (F i) f < b
⊢ ∀ i ∈ s, ∀ᶠ (x : α) in f, F i x < b

Tactic:
exact fun i i_s ↦ eventually_lt_of_limsup_lt (hb i i_s) (h₂ i i_s)

Premises used: Filter.eventually_lt_of_limsup_lt
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
a : ∀ b ∈ s, limsup (F b) f ≤ limsup (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f
⊢ LE.le.{u_2} (α := β) (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)

Premises used: Filter.limsup, Finset.sup'_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
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

Tactic:
fun i i_s ↦ limsup_le_limsup (Eventually.of_forall (fun a ↦ ?_)) (h₁ i i_s) bddsup

Premises used: Filter.Eventually.of_forall, Filter.limsup_le_limsup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
a : ∀ (i : ι) (i_s : i ∈ s) (a : α), F i a ≤ (fun (a : α) ↦ (s.sup' hs fun (i : ι) ↦ F i a : β)) a
⊢ ∀ b ∈ s, limsup (F b) f ≤ limsup (fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a) f

Tactic:
refine fun i i_s ↦ limsup_le_limsup (Eventually.of_forall (fun a ↦ ?_)) (h₁ i i_s) bddsup

Premises used: Filter.Eventually.of_forall, Filter.limsup_le_limsup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
i : ι
i_s : i ∈ s
a : α
a₁ : ∃ b ∈ s, F i a ≤ F b a
⊢ F i a ≤ (fun (a : α) ↦ (s.sup' hs fun (i : ι) ↦ F i a : β)) a

Tactic:
simp only [le_sup'_iff]

Premises used: Finset.le_sup'_iff
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
bddsup : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f fun (a : α) ↦ s.sup' hs fun (i : ι) ↦ F i a
i : ι
i_s : i ∈ s
a : α
w : ι
left : i ∈ s
right : F i a ≤ F i a
⊢ ∃ b ∈ s, F i a ≤ F b a

Tactic:
use i, i_s
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
inl :
  ∀ (h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) ⊥ (F i))
    (h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) ⊥ (F i)),
    Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) ⊥) (s.sup fun (i : ι) ↦ limsup (F i) ⊥)
inr :
  f.NeBot →
    Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) f) (s.sup fun (i : ι) ↦ limsup (F i) f)
⊢ Eq.{u_2 + 1} (α := β) (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 | _)

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
inst_1 : OrderBot β
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) ⊥ (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) ⊥ (F i)
⊢ Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) ⊥) (s.sup fun (i : ι) ↦ limsup (F i) ⊥)

Tactic:
simp [limsup_eq, csInf_univ]

Premises used: Filter.limsup_eq, csInf_univ
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h : f.NeBot
inr :
  ∀ (h₁ : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i))
    (h₂ : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)),
    Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ sup ∅ fun (i : ι) ↦ F i a) f) (sup ∅ fun (i : ι) ↦ limsup (F i) f)
inr₁ :
  ∀ (s_nemp : s.Nonempty),
    Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) f) (s.sup fun (i : ι) ↦ limsup (F i) f)
⊢ Eq.{u_2 + 1} (α := β) (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)

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
h : f.NeBot
h₁ : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
⊢ Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ sup ∅ fun (i : ι) ↦ F i a) f) (sup ∅ fun (i : ι) ↦ limsup (F i) f)

Tactic:
simp only [sup_empty, limsup_const]

Premises used: Filter.limsup_const, Finset.sup_empty
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h : f.NeBot
s_nemp : s.Nonempty
inr :
  Eq.{u_2 + 1} (α := β) (limsup (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) f)
    (limsup (fun (a : α) ↦ s.sup' s_nemp fun (i : ι) ↦ F i a) f)
⊢ Eq.{u_2 + 1} (α := β) (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₂]

Premises used: Filter.limsup, limsup_finset_sup', Finset.sup'_eq_sup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h : f.NeBot
s_nemp : s.Nonempty
inr : Eq (α := α → β) (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) fun (a : α) ↦ s.sup' s_nemp fun (i : ι) ↦ F i a
⊢ Eq.{u_2 + 1} (α := β) (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
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h : f.NeBot
s_nemp : s.Nonempty
inr : ∀ (a : α), Eq.{u_2 + 1} (α := β) (s.sup fun (i : ι) ↦ F i a) (s.sup' s_nemp fun (i : ι) ↦ F i a)
⊢ Eq (α := α → β) (fun (a : α) ↦ s.sup fun (i : ι) ↦ F i a) fun (a : α) ↦ s.sup' s_nemp fun (i : ι) ↦ F i a

Tactic:
ext a
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h : f.NeBot
s_nemp : s.Nonempty
a : α
⊢ Eq.{u_2 + 1} (α := β) (s.sup fun (i : ι) ↦ F i a) (s.sup' s_nemp fun (i : ι) ↦ F i a)

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

Premises used: Eq.symm, Finset.sup'_eq_sup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
inst_1 : OrderBot β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f (F i)
h : f.NeBot
s_nemp : s.Nonempty
a : α
⊢ Eq.{u_2 + 1} (α := β) (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))

Premises used: Eq.symm, Finset.sup'_eq_sup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f (F i)
⊢ Eq.{u_2 + 1} (α := β) (liminf (fun (a : α) ↦ s.inf' hs fun (i : ι) ↦ F i a) f)
    (s.inf' hs fun (i : ι) ↦ liminf (F i) f)

Tactic:
limsup_finset_sup' (β := βᵒᵈ) hs h₁ h₂

Premises used: Filter.limsInf, Filter.liminf, Finset.inf', setOf, WithTop.some, WithTop.untop, OrderDual, Finset.inf, limsup_finset_sup', WithTop
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : ConditionallyCompleteLinearOrder β
inst_1 : OrderTop β
f : Filter α
F : ι → α → β
s : Finset ι
h₁ : ∀ i ∈ s, IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f (F i)
h₂ : ∀ i ∈ s, IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f (F i)
⊢ Eq.{u_2 + 1} (α := β) (liminf (fun (a : α) ↦ s.inf fun (i : ι) ↦ F i a) f) (s.inf fun (i : ι) ↦ liminf (F i) f)

Tactic:
limsup_finset_sup (β := βᵒᵈ) h₁ h₂

Premises used: Filter.limsInf, Filter.liminf, setOf, limsup_finset_sup, OrderDual, Finset.inf
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : NoMinOrder α
a : α
⊢ Nonempty.{max 1 (u_1 + 1)} { x : α // x < a }

Tactic:
nonempty_subtype.2 (exists_lt a)

Premises used: Iff.mpr, nonempty_subtype, NoMinOrder.exists_lt
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : IsEmpty α
⊢ NoMinOrder α

Tactic:
⟨isEmptyElim⟩

Premises used: isEmptyElim, NoMinOrder.mk
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : NoTopOrder α
⊢ NoBotOrder.{u_1} αᵒᵈ

Tactic:
⟨fun a => exists_not_le (α := α) a⟩

Premises used: NoBotOrder.mk, NoTopOrder.exists_not_le
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : LT α
inst_1 : NoMaxOrder α
⊢ NoMinOrder.{u_1} αᵒᵈ

Tactic:
⟨fun a => exists_gt (α := α) a⟩

Premises used: NoMaxOrder.exists_gt, NoMinOrder.mk
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : NoMinOrder α
⊢ NoBotOrder α

Tactic:
⟨fun a => (exists_lt a).imp fun _ => not_le_of_gt⟩

Premises used: Exists.imp, NoBotOrder.mk, NoMinOrder.exists_lt, not_le_of_gt
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMinOrder α
x : α × β
a : α
b : β
obtain : ∀ (c : α) (h : c < a), ∃ (b_1 : α × β), b_1 < (a, b)
⊢ ∃ (b_1 : α × β), b_1 < (a, b)

Tactic:
obtain ⟨c, h⟩ := exists_lt a

Premises used: NoMinOrder.exists_lt