-- Mathlib/Order/LiminfLimsup.lean
/-- For nontrivial filters in linear orders, coboundedness for `≤` implies frequent boundedness
from below. -/
lemma IsCobounded.frequently_ge [LinearOrder α] [NeBot f] (cobdd : IsCobounded (· ≤ ·) f) :
    ∃ l, ∃ᶠ x in f, l ≤ x

Proof state:
case intro.inr.intro
α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) t a
t' : α
ht' : t' < t
⊢ ∃ l, ∃ᶠ (x : α) in f, l ≤ x

Tactic:
refine ⟨t', fun ev ↦ ?_⟩

Result:
case intro.inr.intro
α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) t a
t' : α
ht' : t' < t
ev : ∀ᶠ (x : α) in f, ¬(fun x => t' ≤ x) x
⊢ False

Proof state:
case intro.inr.intro
α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) t a
t' : α
ht' : t' < t
ev : ∀ᶠ (x : α) in f, ¬(fun x => t' ≤ x) x
⊢ False

Tactic:
specialize ht t' (by filter_upwards [ev] with _ h using (not_le.mp h).le)

Result:
case intro.inr.intro
α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
t t' : α
ht' : t' < t
ev : ∀ᶠ (x : α) in f, ¬(fun x => t' ≤ x) x
ht : t ≤ t'
⊢ False

Proof state:
case intro.inr.intro
α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
t t' : α
ht' : t' < t
ev : ∀ᶠ (x : α) in f, ¬(fun x => t' ≤ x) x
ht : t ≤ t'
⊢ False

Tactic:
exact not_lt_of_le ht ht'

Result:
no goals

Proof state:
case intro
α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) t a
⊢ ∃ l, ∃ᶠ (x : α) in f, l ≤ x

Tactic:
rcases isBot_or_exists_lt t with tbot | ⟨t', ht'⟩

Result:
case intro.inl
α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) t a
tbot : IsBot t
⊢ ∃ l, ∃ᶠ (x : α) in f, l ≤ x

case intro.inr.intro
α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) t a
t' : α
ht' : t' < t
⊢ ∃ l, ∃ᶠ (x : α) in f, l ≤ x

Proof state:
α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
cobdd : IsCobounded (fun x1 x2 => x1 ≤ x2) f
⊢ ∃ l, ∃ᶠ (x : α) in f, l ≤ x

Tactic:
obtain ⟨t, ht⟩ := cobdd

Result:
case intro
α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) t a
⊢ ∃ l, ∃ᶠ (x : α) in f, l ≤ x

Proof state:
α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) t a
t' : α
ht' : t' < t
ev : ∀ᶠ (x : α) in f, ¬(fun x => t' ≤ x) x
⊢ ∀ᶠ (x : α) in f, (fun x1 x2 => x1 ≤ x2) x t'

Tactic:
filter_upwards [ev] with _ h using (not_le.mp h).le

Result:
no goals

Proof state:
case intro.inl
α : Type u_1
f : Filter α
inst✝¹ : LinearOrder α
inst✝ : f.NeBot
t : α
ht : ∀ (a : α), (∀ᶠ (x : α) in f, (fun x1 x2 => x1 ≤ x2) x a) → (fun x1 x2 => x1 ≤ x2) t a
tbot : IsBot t
⊢ ∃ l, ∃ᶠ (x : α) in f, l ≤ x

Tactic:
exact ⟨t, .of_forall fun r ↦ tbot r⟩

Result:
no goals