-- 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:
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

Tactic:
obtain ⟨l, l_lt, h'l⟩ :
    ∃ l < F.limsSup, Set.Ioc l F.limsSup ⊆ { x : R | f x < F.liminf f } := by
  apply exists_Ioc_subset_of_mem_nhds ((tendsto_order.1 f_cont.tendsto).2 _ H)
  simpa [IsBot] using not_bot

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

Proof state:
case 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 : S
hc : c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a})
d : S
h'd : c < d
e : R
he : e ∈ {a | ∀ᶠ (n : R) in F, n ≤ a}
fe_eq_d : f e = d
⊢ d ∈ {a | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}

Tactic:
filter_upwards [he] with x hx using (fe_eq_d.symm ▸ f_decr hx)

Result:
no goals

Proof state:
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

Tactic:
rw [limsSup, f_decr.map_csInf_of_continuousAt f_cont bdd_above cobdd]

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✝
⊢ sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a}) ≤ liminf f F

Proof state:
case neg.intro.intro.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✝
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
B : liminf f F ≤ f m
I : f m < liminf f F
⊢ False

Tactic:
exact lt_irrefl _ (B.trans_lt I)

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
⊢ liminf f F ≤ f F.limsSup

Tactic:
by_contra! 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
⊢ 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✝
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
x : R
hx : c < x
this : x < F.limsSup
⊢ False

Tactic:
have : (Set.Ioo c F.limsSup).Nonempty := ⟨x, ⟨hx, this⟩⟩

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
this✝ : x < F.limsSup
this : (Set.Ioo c F.limsSup).Nonempty
⊢ False