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

Tactic:
apply le_of_forall_lt

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

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
⊢ IsBoundedUnder (fun x1 x2 => x1 ≥ x2) F f

Tactic:
exact IsBounded.isBoundedUnder f_decr bdd_above

Result:
no goals

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
⊢ False

Tactic:
have I : f m < F.liminf f := h'l ⟨l_m, m_lt.le⟩

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

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 < sSup {a | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}

Tactic:
obtain ⟨d, hd, h'd⟩ :=
  exists_lt_of_lt_csSup (bdd_above.recOn fun x hx ↦ ⟨f x, Set.mem_image_of_mem f hx⟩) hc

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

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

Tactic:
apply lt_csSup_of_lt ?_ ?_ h'd

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

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
⊢ d ∈ {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 = ∅
x : R
hx : c < x
this✝ : x < F.limsSup
this : (Set.Ioo c F.limsSup).Nonempty
⊢ False

Tactic:
simp only [hc, Set.not_nonempty_empty] at this

Result:
no goals