-- 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✝
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
⊢ ∀ (x : R), c < x → F.limsSup ≤ x

Tactic:
intro x hx

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
hx : c < x
⊢ F.limsSup ≤ x

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 : S
hc : c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a})
d : S
hd : d ∈ f '' {a | ∀ᶠ (n : R) in F, n ≤ a}
h'd : c < d
⊢ BddAbove {a | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}

Tactic:
simpa only [BddAbove, upperBounds]
  using Antitone.isCoboundedUnder_ge_of_isCobounded f_decr cobdd

Result:
no goals

Proof state:
case neg
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
⊢ False

Tactic:
have not_bot : ¬ IsBot F.limsSup := fun maybe_bot ↦
  lt_irrefl (F.liminf f) <| lt_of_le_of_lt
    (liminf_le_of_frequently_le (Frequently.of_forall (fun r ↦ f_decr (maybe_bot r)))
      (bdd_above.isBoundedUnder f_decr)) H

Result:
case neg
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
⊢ False

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 : R
l_lt : l < F.limsSup
h'l : Set.Ioc l F.limsSup ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < F.limsSup
⊢ ∀ (x : R), m < x → f x ≤ f m

Tactic:
exact fun x hx ↦ f_decr hx.le

Result:
no goals

Proof state:
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 = ∅
B : ∃ᶠ (n : R) in F, F.limsSup ≤ n
⊢ liminf f F ≤ f F.limsSup

Tactic:
apply liminf_le_of_frequently_le _ (bdd_above.isBoundedUnder f_decr)

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 = ∅
B : ∃ᶠ (n : R) in F, F.limsSup ≤ n
⊢ ∃ᶠ (x : R) in F, f x ≤ 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 : R
l_lt : l < F.limsSup
h'l : Set.Ioc l F.limsSup ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < F.limsSup
⊢ liminf f F ≤ f m

Tactic:
apply liminf_le_of_frequently_le _ _

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 : R
l_lt : l < F.limsSup
h'l : Set.Ioc l F.limsSup ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < F.limsSup
⊢ ∃ᶠ (x : R) in F, f x ≤ f m

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 : R
l_lt : l < F.limsSup
h'l : Set.Ioc l F.limsSup ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < F.limsSup
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) F f