-- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
theorem tendsto_of_no_upcrossings [DenselyOrdered α] {f : Filter β} {u : β → α} {s : Set α}
    (hs : Dense s) (H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ n in f, u n < a) ∧ ∃ᶠ n in f, b < u n))
    (h : f.IsBoundedUnder (· ≤ ·) u

Proof state:
case inr
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
hbot : f.NeBot
⊢ ∃ c, Tendsto u f (𝓝 c)

Tactic:
refine ⟨limsup u f, ?_⟩

Result:
case inr
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
hbot : f.NeBot
⊢ Tendsto u f (𝓝 (limsup u f))

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
hbot : f.NeBot
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
b : α
bs : b ∈ s
ab : a < b
bu : b < limsup u f
A : ∃ᶠ (n : β) in f, u n < a
B : ∃ᶠ (n : β) in f, b < u n
⊢ False

Tactic:
exact H a as b bs ab ⟨A, B⟩

Result:
no goals

Proof state:
case inl
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in ⊥, u n < a) ∧ ∃ᶠ (n : β) in ⊥, b < u n)
h : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) ⊥ u) _auto✝
h' : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) ⊥ u) _auto✝
⊢ ∃ c, Tendsto u ⊥ (𝓝 c)

Tactic:
exact ⟨sInf ∅, tendsto_bot⟩

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
⊢ ∃ c, Tendsto u f (𝓝 c)

Tactic:
rcases f.eq_or_neBot with rfl | hbot

Result:
case inl
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in ⊥, u n < a) ∧ ∃ᶠ (n : β) in ⊥, b < u n)
h : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) ⊥ u) _auto✝
h' : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) ⊥ u) _auto✝
⊢ ∃ c, Tendsto u ⊥ (𝓝 c)

case inr
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
hbot : f.NeBot
⊢ ∃ c, Tendsto u f (𝓝 c)

Proof state:
case inr
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
hbot : f.NeBot
⊢ Tendsto u f (𝓝 (limsup u f))

Tactic:
apply tendsto_of_le_liminf_of_limsup_le _ le_rfl h h'

Result:
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
hbot : f.NeBot
⊢ limsup u f ≤ liminf u f

Proof state:
case intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
hbot : f.NeBot
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
⊢ False

Tactic:
obtain ⟨b, ⟨⟨ab, bu⟩, bs⟩⟩ : ∃ b, (a < b ∧ b < f.limsup u) ∧ b ∈ s :=
  dense_iff_inter_open.1 hs (Set.Ioo a (f.limsup u)) isOpen_Ioo (Set.nonempty_Ioo.2 au)

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
hbot : f.NeBot
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
b : α
bs : b ∈ s
ab : a < b
bu : b < limsup u f
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
hbot : f.NeBot
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
b : α
bs : b ∈ s
ab : a < b
bu : b < limsup u f
⊢ False

Tactic:
have A : ∃ᶠ n in f, u n < a := frequently_lt_of_liminf_lt (IsBounded.isCobounded_ge h) la

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ a ∈ s, ∀ b ∈ s, a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) _auto✝
hbot : f.NeBot
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
b : α
bs : b ∈ s
ab : a < b
bu : b < limsup u f
A : ∃ᶠ (n : β) in f, u n < a
⊢ False