-- Mathlib/Topology/Order/IsLUB.lean
theorem IsLUB.frequently_mem {a : α} {s : Set α} (ha : IsLUB s a) (hs : s.Nonempty) :
    ∃ᶠ x in 𝓝[≤] a, x ∈ s

Proof state:
case intro.inl
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
s : Set α
a' : α
ha' : a' ∈ s
ha : IsLUB s a'
h : ∀ᶠ (x : α) in 𝓝[≤] a', ¬(fun x => x ∈ s) x
⊢ False

Tactic:
exact h.self_of_nhdsWithin le_rfl ha'

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
⊢ ∃ᶠ (x : α) in 𝓝[≤] a, x ∈ s

Tactic:
intro h

Result:
case intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun x => x ∈ s) x
⊢ False

Proof state:
case intro.inr.intro.intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun x => x ∈ s) x
ha'a : a' < a
b : α
hba : b ∈ Iio a
hb : Ioc b a ⊆ {x | (fun x => ¬(fun x => x ∈ s) x) x}
b' : α
hb's : b' ∈ s
hb' : b < b' ∧ b' ≤ a
⊢ False

Tactic:
exact hb hb' hb's

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
hs : s.Nonempty
⊢ ∃ᶠ (x : α) in 𝓝[≤] a, x ∈ s

Tactic:
rcases hs with ⟨a', ha'⟩

Result:
case intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
⊢ ∃ᶠ (x : α) in 𝓝[≤] a, x ∈ s

Proof state:
case intro.inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun x => x ∈ s) x
ha'a : a' < a
⊢ False

Tactic:
rcases (mem_nhdsLE_iff_exists_Ioc_subset' ha'a).1 h with ⟨b, hba, hb⟩

Result:
case intro.inr.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun x => x ∈ s) x
ha'a : a' < a
b : α
hba : b ∈ Iio a
hb : Ioc b a ⊆ {x | (fun x => ¬(fun x => x ∈ s) x) x}
⊢ False

Proof state:
case intro.inr.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun x => x ∈ s) x
ha'a : a' < a
b : α
hba : b ∈ Iio a
hb : Ioc b a ⊆ {x | (fun x => ¬(fun x => x ∈ s) x) x}
⊢ False

Tactic:
rcases ha.exists_between hba with ⟨b', hb's, hb'⟩

Result:
case intro.inr.intro.intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun x => x ∈ s) x
ha'a : a' < a
b : α
hba : b ∈ Iio a
hb : Ioc b a ⊆ {x | (fun x => ¬(fun x => x ∈ s) x) x}
b' : α
hb's : b' ∈ s
hb' : b < b' ∧ b' ≤ a
⊢ False

Proof state:
case intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun x => x ∈ s) x
⊢ False

Tactic:
rcases (ha.1 ha').eq_or_lt with (rfl | ha'a)

Result:
case intro.inl
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
s : Set α
a' : α
ha' : a' ∈ s
ha : IsLUB s a'
h : ∀ᶠ (x : α) in 𝓝[≤] a', ¬(fun x => x ∈ s) x
⊢ False

case intro.inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
a' : α
ha' : a' ∈ s
h : ∀ᶠ (x : α) in 𝓝[≤] a, ¬(fun x => x ∈ s) x
ha'a : a' < a
⊢ False