awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
c : S
hc : c < sSup (f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a})
d : S
hd : d ∈ f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a}
h'd : c < d
apply : BddAbove.{u_5} (α := S) {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}
apply₁ : Membership.mem (γ := Set S) {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1} d
⊢ c < sSup {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}

Tactic:
apply lt_csSup_of_lt ?_ ?_ h'd

Premises used: lt_csSup_of_lt
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
c : S
hc : c < sSup (f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a})
d : S
hd : d ∈ f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a}
h'd : c < d
⊢ BddAbove.{u_5} (α := S) {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}

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

Premises used: upperBounds, BddAbove, Antitone.isCoboundedUnder_ge_of_isCobounded
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
c : S
hc : c < sSup (f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a})
d : S
hd : d ∈ f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a}
h'd : c < d
rcases :
  ∀ (e : R) (he : Membership.mem (γ := Set R) {a : R | ∀ᶠ (n : R) in F, n ≤ a} e) (fe_eq_d : f e = d),
    Membership.mem (γ := Set S) {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1} d
⊢ Membership.mem (γ := Set S) {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1} d

Tactic:
rcases hd with ⟨e, ⟨he, fe_eq_d⟩⟩
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
c : S
hc : c < sSup (f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a})
d : S
h'd : c < d
e : R
he : Membership.mem (γ := Set R) {a : R | ∀ᶠ (n : R) in F, n ≤ a} e
fe_eq_d : f e = d
x : R
hx : x ≤ e
⊢ d ≤ f x

Tactic:
(fe_eq_d.symm ▸ f_decr hx)

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
c : S
hc : c < sSup (f '' {a : R | ∀ᶠ (n : R) in F, n ≤ a})
d : S
h'd : c < d
e : R
he : Membership.mem (γ := Set R) {a : R | ∀ᶠ (n : R) in F, n ≤ a} e
fe_eq_d : f e = d
h :
  ∀ (a : R),
    Membership.mem (γ := Set R)
      {x : R |
        Membership.mem (γ := Set R) {x : R | (fun (n : R) ↦ n ≤ e) x} x →
          Membership.mem (γ := Set R) {x : R | (fun (a : R) ↦ d ≤ f a) x} x}
      a
h₁ h₂ : ∀ (x : R) (hx : x ≤ e), d ≤ f x
⊢ Membership.mem (γ := Set S) {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1} d

Tactic:
filter_upwards [he] with x hx using (fe_eq_d.symm ▸ f_decr hx)
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
pos : ∀ (h' : ∃ c < F.limsSup, Set.Ioo c F.limsSup = ∅), liminf f F ≤ f F.limsSup
neg : ∀ (h' : ∀ (c : R) (_ : c < F.limsSup), (Set.Ioo c F.limsSup).Nonempty), liminf f F ≤ f F.limsSup
⊢ liminf f F ≤ f F.limsSup

Tactic:
by_cases! h' : ∃ c, c < F.limsSup ∧ Set.Ioo c F.limsSup = ∅

Premises used: Filter.limsSup
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
h' : ∃ c < F.limsSup, Set.Ioo c F.limsSup = ∅
pos : ∀ (c : R) (c_lt : c < F.limsSup) (hc : Set.Ioo c F.limsSup = ∅), liminf f F ≤ f F.limsSup
⊢ liminf f F ≤ f F.limsSup

Tactic:
rcases h' with ⟨c, c_lt, hc⟩
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
apply : ∀ (x : R), c < x → F.limsSup ≤ x
⊢ ∃ᶠ (n : R) in F, F.limsSup ≤ n

Tactic:
apply (frequently_lt_of_lt_limsSup cobdd c_lt).mono

Premises used: Filter.Frequently.mono, Filter.frequently_lt_of_lt_limsSup
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
x : R
hx : c < x
by_contra! : ∀ (this : x < F.limsSup), False
⊢ F.limsSup ≤ x

Tactic:
by_contra!
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
x : R
hx : c < x
this : x < F.limsSup
⊢ (Set.Ioo c F.limsSup).Nonempty

Tactic:
have : (Set.Ioo c F.limsSup).Nonempty := ⟨x, ⟨hx, this⟩⟩
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
x : R
hx : c < x
this_1 : x < F.limsSup
this : (Set.Ioo c F.limsSup).Nonempty
⊢ False

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

Premises used: Set.not_nonempty_empty
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
⊢ ∃ᶠ (n : R) in F, F.limsSup ≤ n

Tactic:
have B : ∃ᶠ n in F, F.limsSup ≤ n := by
        apply (frequently_lt_of_lt_limsSup cobdd c_lt).mono
        intro x hx
        by_contra!
        have : (Set.Ioo c F.limsSup).Nonempty := ⟨x, ⟨hx, this⟩⟩
        simp only [hc, Set.not_nonempty_empty] at this
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
B : ∃ᶠ (n : R) in F, F.limsSup ≤ n
apply : ∃ᶠ (i : R) in F, f i ≤ f F.limsSup
⊢ liminf f F ≤ f F.limsSup

Tactic:
apply liminf_le_of_frequently_le _ (bdd_above.isBoundedUnder f_decr)

Premises used: Filter.IsBounded.isBoundedUnder, Filter.liminf_le_of_frequently_le
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
B : ∃ᶠ (n : R) in F, F.limsSup ≤ n
⊢ ∃ᶠ (i : R) in F, f i ≤ f F.limsSup

Tactic:
B.mono fun x hx ↦ f_decr hx

Premises used: Filter.Frequently.mono
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
c : R
c_lt : c < F.limsSup
hc : Set.Ioo c F.limsSup = ∅
B : ∃ᶠ (n : R) in F, F.limsSup ≤ n
⊢ ∃ᶠ (i : R) in F, f i ≤ f F.limsSup

Tactic:
exact B.mono fun x hx ↦ f_decr hx

Premises used: Filter.Frequently.mono
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
h' : ∀ (c : R) (_ : c < F.limsSup), (Set.Ioo c F.limsSup).Nonempty
neg : ∀ (H : f F.limsSup < liminf f F), False
⊢ liminf f F ≤ f F.limsSup

Tactic:
by_contra! H
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
h' : ∀ (c : R) (_ : c < F.limsSup), (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
⊢ ¬IsBot F.limsSup

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
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
h' : ∀ (c : R) (_ : c < F.limsSup), (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
not_bot : ¬IsBot F.limsSup
apply : ∃ (l : R), l < F.limsSup
⊢ ∃ l < F.limsSup, Set.Ioc l F.limsSup ⊆ {x : R | f x < liminf f F}

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

Premises used: tendsto_order, exists_Ioc_subset_of_mem_nhds, And.right, ContinuousAt.tendsto, Iff.mp
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
h' : ∀ (c : R) (_ : c < F.limsSup), (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
not_bot : ¬IsBot F.limsSup
⊢ ∃ (l : R), l < F.limsSup

Tactic:
simpa [IsBot] using not_bot

Premises used: IsBot
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
h' : ∀ (c : R) (_ : c < F.limsSup), (Set.Ioo c F.limsSup).Nonempty
H : f F.limsSup < liminf f F
not_bot : ¬IsBot F.limsSup
neg : ∀ (l : R) (l_lt : l < F.limsSup) (h'l : Set.Ioc l F.limsSup ⊆ {x : R | f x < liminf f F}), False
⊢ 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

Premises used: Filter.limsSup, Filter.liminf
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
h' : ∀ (c : R) (_ : 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 : R | f x < liminf f F}
contrapose! : ∀ (h' : Set.Ioo l F.limsSup = ∅), ∃ c < F.limsSup, Set.Ioo c F.limsSup = ∅
⊢ (Set.Ioo l F.limsSup).Nonempty

Tactic:
contrapose! h'
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
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 : R | f x < liminf f F}
h' : Set.Ioo l F.limsSup = ∅
⊢ ∃ c < F.limsSup, Set.Ioo c F.limsSup = ∅

Tactic:
⟨l, l_lt, h'⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
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 : R | f x < liminf f F}
h' : Set.Ioo l F.limsSup = ∅
⊢ ∃ c < F.limsSup, Set.Ioo c F.limsSup = ∅

Tactic:
exact ⟨l, l_lt, h'⟩
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
h' : ∀ (c : R) (_ : 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 : R | f x < liminf f F}
neg : ∀ (m : R) (l_m : l < m) (m_lt : m < F.limsSup), False
⊢ False

Tactic:
obtain ⟨m, l_m, m_lt⟩ : (Set.Ioo l F.limsSup).Nonempty := by
      contrapose! h'
      exact ⟨l, l_lt, h'⟩

Premises used: Filter.limsSup, Set.Nonempty, Set.Ioo
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
h' : ∀ (c : R) (_ : 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 : R | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < F.limsSup
apply : ∃ᶠ (i : R) in F, f i ≤ f m
apply₁ : IsBoundedUnder (fun (x1 x2 : S) ↦ x1 ≥ x2) F f
⊢ liminf f F ≤ f m

Tactic:
apply liminf_le_of_frequently_le _ _

Premises used: Filter.liminf_le_of_frequently_le
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
h' : ∀ (c : R) (_ : 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 : R | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < F.limsSup
apply : ∀ (x : R), m < x → f x ≤ f m
⊢ ∃ᶠ (i : R) in F, f i ≤ f m

Tactic:
apply (frequently_lt_of_lt_limsSup cobdd m_lt).mono

Premises used: Filter.Frequently.mono, Filter.frequently_lt_of_lt_limsSup
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
h' : ∀ (c : R) (_ : 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 : R | 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:
fun x hx ↦ f_decr hx.le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
h' : ∀ (c : R) (_ : 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 : R | 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
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
h' : ∀ (c : R) (_ : 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 : R | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < F.limsSup
⊢ IsBoundedUnder (fun (x1 x2 : S) ↦ x1 ≥ x2) F f

Tactic:
IsBounded.isBoundedUnder f_decr bdd_above

Premises used: Filter.IsBounded.isBoundedUnder
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
R : Type u_4
S : Type u_5
inst : ConditionallyCompleteLinearOrder R
inst_1 : TopologicalSpace R
inst_2 : OrderTopology R
inst_3 : ConditionallyCompleteLinearOrder S
inst_4 : TopologicalSpace S
inst_5 : OrderTopology S
F : Filter R
inst_6 : F.NeBot
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f F.limsSup
bdd_above : IsBounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
cobdd : IsCobounded (fun (x1 x2 : R) ↦ x1 ≤ x2) F
h' : ∀ (c : R) (_ : 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 : R | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < F.limsSup
⊢ IsBoundedUnder (fun (x1 x2 : S) ↦ x1 ≥ x2) F f

Tactic:
exact IsBounded.isBoundedUnder f_decr bdd_above