-- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
theorem Antitone.map_limsSup_of_continuousAt {F : Filter R} [NeBot F] {f : R → S}
    (f_decr : Antitone f) (f_cont : ContinuousAt f F.limsSup)
    (bdd_above : F.IsBounded (· ≤ ·)

Proof state:
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : autoParam (IsBounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
cobdd : autoParam (IsCobounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
h' : ∀ c < F.limsSup, (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
not_bot : ¬IsBot F.limsSup
⊢ ∃ l < F.limsSup, Set.Ioc l F.limsSup ⊆ {x | f x < liminf f F}

Tactic:
apply exists_Ioc_subset_of_mem_nhds ((tendsto_order.1 f_cont.tendsto).2 _ H)

Result:
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : autoParam (IsBounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
cobdd : autoParam (IsCobounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
h' : ∀ c < F.limsSup, (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
not_bot : ¬IsBot F.limsSup
⊢ ∃ l, l < F.limsSup

Proof state:
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : autoParam (IsBounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
cobdd : autoParam (IsCobounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
⊢ f F.limsSup = liminf f F

Tactic:
apply le_antisymm

Result:
case a
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : autoParam (IsBounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
cobdd : autoParam (IsCobounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
⊢ f F.limsSup ≤ liminf f F

case a
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : autoParam (IsBounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
cobdd : autoParam (IsCobounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
⊢ liminf f F ≤ f F.limsSup

Proof state:
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : autoParam (IsBounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
cobdd : autoParam (IsCobounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
h' : ∀ c < F.limsSup, (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
not_bot : ¬IsBot F.limsSup
⊢ ∃ l, l < F.limsSup

Tactic:
simpa [IsBot] using not_bot

Result:
no goals

Proof state:
case pos
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : autoParam (IsBounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
cobdd : autoParam (IsCobounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
h' : ∃ c < F.limsSup, Set.Ioo c F.limsSup = ∅
⊢ liminf f F ≤ f F.limsSup

Tactic:
rcases h' with ⟨c, c_lt, hc⟩

Result:
case pos.intro.intro
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : autoParam (IsBounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
cobdd : autoParam (IsCobounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
⊢ liminf f F ≤ f F.limsSup

Proof state:
case a.H
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : autoParam (IsBounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
cobdd : autoParam (IsCobounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
c : S
hc : c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a})
⊢ c < liminf f F

Tactic:
simp only [liminf, limsInf, eventually_map] at hc ⊢

Result:
case a.H
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : autoParam (IsBounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
cobdd : autoParam (IsCobounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
c : S
hc : c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a})
⊢ c < sSup {a | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}

Proof state:
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : autoParam (IsBounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
cobdd : autoParam (IsCobounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
⊢ ∃ᶠ (n : R) in F, F.limsSup ≤ n

Tactic:
apply (frequently_lt_of_lt_limsSup cobdd c_lt).mono

Result:
R : Type u_4
S : Type u_5
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : autoParam (IsBounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
cobdd : autoParam (IsCobounded (fun x1 x2 => x1 ≤ x2) F) _auto✝
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
⊢ ∀ (x : R), c < x → F.limsSup ≤ x