awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ¬∀ y < x, ∃ (z : β), y < z ∧ z < x
⊢ ∃ y < x, ∀ (z : β), z ≤ y ∨ x ≤ z

Tactic:
push +distrib Not at h'

Premises used: Not
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∃ y < x, ∀ (z : β), z ≤ y ∨ x ≤ z
rcases : ∀ (z : β) (z_x : z < x) (hz : ∀ (z_1 : β), z_1 ≤ z ∨ x ≤ z_1), ∃ᶠ (i : α) in f, x ≤ u i
⊢ ∃ᶠ (i : α) in f, x ≤ u i

Tactic:
rcases h' with ⟨z, z_x, hz⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
z : β
z_x : z < x
hz : ∀ (z_1 : β), z_1 ≤ z ∨ x ≤ z_1
⊢ ∃ᶠ (i : α) in f, x ≤ u i

Tactic:
(h z z_x).mono <| fun w hw ↦ (or_iff_right (not_le_of_gt hw)).1 (hz (u w))

Premises used: Filter.Frequently.mono, Iff.mp, or_iff_right, not_le_of_gt
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
z : β
z_x : z < x
hz : ∀ (z_1 : β), z_1 ≤ z ∨ x ≤ z_1
⊢ ∃ᶠ (i : α) in f, x ≤ u i

Tactic:
exact (h z z_x).mono <| fun w hw ↦ (or_iff_right (not_le_of_gt hw)).1 (hz (u w))

Premises used: Filter.Frequently.mono, Iff.mp, or_iff_right, not_le_of_gt
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst_1 : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
⊢ x ≤ limsup u f ↔ ∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a

Tactic:
⟨fun h _ h' ↦ (frequently_lt_of_lt_limsup h₁ (h'.trans_le h)).mono fun _ ↦ le_of_lt, ?_⟩

Premises used: le_of_lt, Filter.Frequently.mono, LT.lt.trans_le, Iff.intro, Filter.frequently_lt_of_lt_limsup
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst_1 : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
refine : (∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a) → x ≤ limsup u f
⊢ x ≤ limsup u f ↔ ∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a

Tactic:
refine ⟨fun h _ h' ↦ (frequently_lt_of_lt_limsup h₁ (h'.trans_le h)).mono fun _ ↦ le_of_lt, ?_⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst_1 : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
rw : (∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a) → ∀ ⦃c : β⦄, c < x → c < limsup u f
⊢ (∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a) → x ≤ limsup u f

Tactic:
rw [← forall_lt_iff_le]

Premises used: forall_lt_iff_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst_1 : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a
y : β
y_x : y < x
obtain : ∀ (z : β) (y_z : y < z) (z_x : z < x), y < limsup u f
⊢ y < limsup u f

Tactic:
obtain ⟨z, y_z, z_x⟩ := exists_between y_x

Premises used: exists_between
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst_1 : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a
y : β
y_x : y < x
z : β
y_z : y < z
z_x : z < x
⊢ y < limsup u f

Tactic:
y_z.trans_le (le_limsup_of_frequently_le (h z z_x) h₂)

Premises used: Filter.le_limsup_of_frequently_le, LT.lt.trans_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst_1 : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a
y : β
y_x : y < x
z : β
y_z : y < z
z_x : z < x
⊢ y < limsup u f

Tactic:
exact y_z.trans_le (le_limsup_of_frequently_le (h z z_x) h₂)

Premises used: Filter.le_limsup_of_frequently_le, LT.lt.trans_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
⊢ x ≤ liminf u f ↔ ∀ y < x, ∀ᶠ (a : α) in f, y < u a

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

Premises used: Filter.limsInf, Filter.liminf, setOf, Filter.limsup_le_iff, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst_1 : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
⊢ x ≤ liminf u f ↔ ∀ y < x, ∀ᶠ (a : α) in f, y ≤ u a

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

Premises used: Filter.limsInf, Filter.liminf, setOf, Filter.limsup_le_iff', OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
⊢ liminf u f ≤ x ↔ ∀ y > x, ∃ᶠ (a : α) in f, u a < y

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

Premises used: Filter.limsInf, Filter.liminf, setOf, Filter.le_limsup_iff, OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst_1 : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
⊢ liminf u f ≤ x ↔ ∀ y > x, ∃ᶠ (a : α) in f, u a ≤ y

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

Premises used: Filter.limsInf, Filter.liminf, setOf, Filter.le_limsup_iff', OrderDual
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
inl :
  ∀ (h : ∃ᶠ (x : α) in ⊥, u x ≤ v x) (h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) ⊥ u)
    (h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) ⊥ v), liminf u ⊥ ≤ limsup v ⊥
inr : f.NeBot → liminf u f ≤ limsup v f
⊢ liminf u f ≤ limsup v f

Tactic:
rcases f.eq_or_neBot with rfl | _

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
u v : α → β
h : ∃ᶠ (x : α) in ⊥, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) ⊥ u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) ⊥ v
⊢ liminf u ⊥ ≤ limsup v ⊥

Tactic:
(frequently_bot h).rec

Premises used: Filter.liminf, Filter.frequently_bot, Bot.bot, LE.le, Filter.limsup, False.rec
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
u v : α → β
h : ∃ᶠ (x : α) in ⊥, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) ⊥ u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) ⊥ v
⊢ liminf u ⊥ ≤ limsup v ⊥

Tactic:
exact (frequently_bot h).rec
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
obtain : ∀ (a : β) (ha : ∀ᶠ (x : α) in f, v x ≤ a), IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u

Tactic:
obtain ⟨a, ha⟩ := h₂.eventually_le

Premises used: Filter.IsBoundedUnder.eventually_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
a : β
ha : ∀ᶠ (x : α) in f, v x ≤ a
apply : ∃ᶠ (x : α) in f, u x ≤ a
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u

Tactic:
apply IsCoboundedUnder.of_frequently_le (a := a)

Premises used: Filter.IsCoboundedUnder.of_frequently_le
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
a : β
ha : ∀ᶠ (x : α) in f, v x ≤ a
⊢ ∃ᶠ (x : α) in f, u x ≤ a

Tactic:
(h.and_eventually ha).mono fun x ⟨u_x, v_x⟩ ↦ u_x.trans v_x

Premises used: LE.le, _private.0.Filter.liminf_le_limsup_of_frequently_le.match_1, Filter.Frequently.mono, Filter.Frequently.and_eventually, LE.le.trans
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
a : β
ha : ∀ᶠ (x : α) in f, v x ≤ a
⊢ ∃ᶠ (x : α) in f, u x ≤ a

Tactic:
exact (h.and_eventually ha).mono fun x ⟨u_x, v_x⟩ ↦ u_x.trans v_x

Premises used: Filter.Frequently.mono, Filter.Frequently.and_eventually
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u

Tactic:
have h₃ : f.IsCoboundedUnder (· ≥ ·) u := by
    obtain ⟨a, ha⟩ := h₂.eventually_le
    apply IsCoboundedUnder.of_frequently_le (a := a)
    exact (h.and_eventually ha).mono fun x ⟨u_x, v_x⟩ ↦ u_x.trans v_x
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
h₃ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
obtain : ∀ (a : β) (ha : ∀ᶠ (x : α) in f, a ≤ u x), IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v

Tactic:
obtain ⟨a, ha⟩ := h₁.eventually_ge

Premises used: Filter.IsBoundedUnder.eventually_ge
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
h₃ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
a : β
ha : ∀ᶠ (x : α) in f, a ≤ u x
apply : ∃ᶠ (x : α) in f, a ≤ v x
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v

Tactic:
apply IsCoboundedUnder.of_frequently_ge (a := a)

Premises used: Filter.IsCoboundedUnder.of_frequently_ge
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
h₃ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
a : β
ha : ∀ᶠ (x : α) in f, a ≤ u x
⊢ ∃ᶠ (x : α) in f, a ≤ v x

Tactic:
(ha.and_frequently h).mono fun x ⟨u_x, v_x⟩ ↦ u_x.trans v_x

Premises used: LE.le, Filter.Frequently.mono, _private.0.Filter.liminf_le_limsup_of_frequently_le.match_2, LE.le.trans, Filter.Eventually.and_frequently
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
h₃ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
a : β
ha : ∀ᶠ (x : α) in f, a ≤ u x
⊢ ∃ᶠ (x : α) in f, a ≤ v x

Tactic:
exact (ha.and_frequently h).mono fun x ⟨u_x, v_x⟩ ↦ u_x.trans v_x

Premises used: Filter.Frequently.mono, Filter.Eventually.and_frequently
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
h₃ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
⊢ IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v

Tactic:
have h₄ : f.IsCoboundedUnder (· ≤ ·) v := by
    obtain ⟨a, ha⟩ := h₁.eventually_ge
    apply IsCoboundedUnder.of_frequently_ge (a := a)
    exact (ha.and_frequently h).mono fun x ⟨u_x, v_x⟩ ↦ u_x.trans v_x
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
h₃ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₄ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
⊢ liminf u f ≤ limsup v f

Tactic:
(le_limsup_iff h₄ h₂).2 fun y y_v ↦ ?_

Premises used: Iff.mpr, Filter.le_limsup_iff
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
h₃ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₄ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
inr : ∀ (y : β) (y_v : y < liminf u f), ∃ᶠ (a : α) in f, y < v a
⊢ liminf u f ≤ limsup v f

Tactic:
refine (le_limsup_iff h₄ h₂).2 fun y y_v ↦ ?_

Premises used: Iff.mpr, Filter.le_limsup_iff
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
h₃ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₄ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
y : β
y_v : y < liminf u f
⊢ ∀ᶠ (a : α) in f, y < u a

Tactic:
have := (le_liminf_iff h₃ h₁).1 (le_refl (liminf u f)) y y_v
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
h₃ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₄ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
y : β
y_v : y < liminf u f
this : ∀ᶠ (a : α) in f, y < u a
⊢ ∃ᶠ (a : α) in f, y < v a

Tactic:
(h.and_eventually this).mono fun x ⟨ux_vx, y_ux⟩ ↦ y_ux.trans_le ux_vx

Premises used: Filter.Frequently.mono, Filter.Frequently.and_eventually, LT.lt.trans_le, LT.lt, _private.0.Filter.liminf_le_limsup_of_frequently_le.match_3
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompleteLinearOrder β
f : Filter α
u v : α → β
h : ∃ᶠ (x : α) in f, u x ≤ v x
h₁ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₂ : IsBoundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
h_1 : f.NeBot
h₃ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≥ x2) f u
h₄ : IsCoboundedUnder (fun (x1 x2 : β) ↦ x1 ≤ x2) f v
y : β
y_v : y < liminf u f
this : ∀ᶠ (a : α) in f, y < u a
⊢ ∃ᶠ (a : α) in f, y < v a

Tactic:
exact (h.and_eventually this).mono fun x ⟨ux_vx, y_ux⟩ ↦ y_ux.trans_le ux_vx

Premises used: Filter.Frequently.mono, Filter.Frequently.and_eventually
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
f : Filter α
b : α
h : IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) f
l : f.limsSup < b
⊢ ∀ᶠ (a : α) in f, a < b

Tactic:
let ⟨c, (h : ∀ᶠ a in f, a ≤ c), hcb⟩ := exists_lt_of_csInf_lt h l
  mem_of_superset h fun _a => hcb.trans_le'

Premises used: Filter.Eventually, LT.lt.trans_le', LT.lt, _private.0.Filter.lt_mem_sets_of_limsSup_lt.match_1, Filter.mem_of_superset, exists_lt_of_csInf_lt
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
f : Filter α
b : α
⊢ IsBounded (fun (x1 x2 : α) ↦ x1 ≥ x2) f → b < f.limsInf → ∀ᶠ (a : α) in f, b < a

Tactic:
@lt_mem_sets_of_limsSup_lt αᵒᵈ _ _ _

Premises used: Filter.limsInf, setOf, OrderDual, Filter.lt_mem_sets_of_limsSup_lt
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder β
f_1 : Filter α
u : α → β
inst_1 : ConditionallyCompleteLinearOrder α
f_2 : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst_2 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_3 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
j : Subtype p
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
g : ℕ → Subtype p := Exists.choose (p := Surjective) ⋯
pos : ∀ (H : ∃ (j : Subtype p), j ∈ m), ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m
neg : ∀ (H : ∀ (j : Subtype p), j ∉ m), ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m
⊢ ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m

Tactic:
by_cases! H : ∃ j, j ∈ m
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder β
f_1 : Filter α
u : α → β
inst_1 : ConditionallyCompleteLinearOrder α
f_2 : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst_2 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_3 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
j : Subtype p
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
g : ℕ → Subtype p := Exists.choose (p := Surjective) ⋯
H : ∃ (j : Subtype p), j ∈ m
pos : ∀ (j : Subtype p) (hj : j ∈ m), ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m
⊢ ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m

Tactic:
rcases H with ⟨j, hj⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder β
f_1 : Filter α
u : α → β
inst_1 : ConditionallyCompleteLinearOrder α
f_2 : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst_2 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_3 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
j_1 : Subtype p
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
g : ℕ → Subtype p := Exists.choose (p := Surjective) ⋯
j : Subtype p
hj : j ∈ m
pos :
  ∀ (n : ℕ) (hj : Membership.mem (α := Subtype p) m (Exists.choose (p := Surjective) ⋯ n : Subtype p)),
    ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m
⊢ ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m

Tactic:
rcases (exists_surjective_nat (Subtype p)).choose_spec j with ⟨n, rfl⟩

Premises used: Exists.choose_spec, Subtype, exists_surjective_nat, rfl
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder β
f_1 : Filter α
u : α → β
inst_1 : ConditionallyCompleteLinearOrder α
f_2 : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst_2 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_3 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
j : Subtype p
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
g : ℕ → Subtype p := Exists.choose (p := Surjective) ⋯
n : ℕ
hj : Membership.mem (α := Subtype p) m (Exists.choose (p := Surjective) ⋯ n : Subtype p)
⊢ ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m

Tactic:
⟨n, Or.inl hj⟩

Premises used: Exists.intro, Or.inl
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder β
f_1 : Filter α
u : α → β
inst_1 : ConditionallyCompleteLinearOrder α
f_2 : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst_2 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_3 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
j : Subtype p
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
g : ℕ → Subtype p := Exists.choose (p := Surjective) ⋯
n : ℕ
hj : Membership.mem (α := Subtype p) m (Exists.choose (p := Surjective) ⋯ n : Subtype p)
⊢ ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m

Tactic:
exact ⟨n, Or.inl hj⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder β
f_1 : Filter α
u : α → β
inst_1 : ConditionallyCompleteLinearOrder α
f_2 : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst_2 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_3 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
j : Subtype p
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
g : ℕ → Subtype p := Exists.choose (p := Surjective) ⋯
H : ∀ (j : Subtype p), j ∉ m
⊢ ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m

Tactic:
⟨0, Or.inr H⟩

Premises used: Exists.intro, OfNat.ofNat, Or.inr
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder β
f_1 : Filter α
u : α → β
inst_1 : ConditionallyCompleteLinearOrder α
f_2 : Filter α
b : α
f : ι → α
s : ι' → Set ι
p : ι' → Prop
inst_2 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_3 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
j : Subtype p
m : Set (Subtype p) :=
  {j : Subtype p | BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))}
g : ℕ → Subtype p := Exists.choose (p := Surjective) ⋯
H : ∀ (j : Subtype p), j ∉ m
⊢ ∃ (n : ℕ), g n ∈ m ∨ ∀ (j : Subtype p), j ∉ m

Tactic:
exact ⟨0, Or.inr H⟩
-- Module: Mathlib.Order.LiminfLimsup
Goal:
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst_1 : Countable.{max 1 (u_5 + 1)} (Subtype p)
inst_2 : Nonempty.{max 1 (u_5 + 1)} (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s (↑j : ι')).Nonempty
H : ∃ (j : Subtype p), BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j : ι')) : Type u_4)) ↦ f (↑i : ι))
rcases :
  ∀ (j0 : Subtype p) (hj0 : BddBelow.{u_1} (α := α) (range fun (i : (↑(s (↑j0 : ι')) : Type u_4)) ↦ f (↑i : ι))),
    liminf f v = ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)
⊢ liminf f v = ⨆ (j : Subtype p), ⨅ (i : (↑(s (↑(liminf_reparam f s p j) : ι')) : Type u_4)), f (↑i : ι)

Tactic:
rcases H with ⟨j0, hj0⟩