awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ Membership.mem (γ := Set S) {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1} d
have 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
Tactic: filter_upwards [he] with x hx using (fe_eq_d.symm ▸ f_decr hx)
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ Membership.mem (γ := Set S) {a : S | ∀ᶠ (a_1 : R) in F, a ≤ f a_1} d
have h₁ : ∀ a ≤ e, d ≤ f a
Tactic: filter_upwards [he] with x hx using (fe_eq_d.symm ▸ f_decr hx)
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ liminf f F ≤ f F.limsSup
have pos : ∀ (h' : ∃ c < F.limsSup, Set.Ioo c F.limsSup = ∅), liminf f F ≤ f F.limsSup
Tactic: by_cases! h' : ∃ c, c < F.limsSup ∧ Set.Ioo c F.limsSup = ∅
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ liminf f F ≤ f F.limsSup
have neg : ∀ (h' : ∀ (c : R) (_ : c < F.limsSup), (Set.Ioo c F.limsSup).Nonempty), liminf f F ≤ f F.limsSup
Tactic: by_cases! h' : ∃ c, c < F.limsSup ∧ Set.Ioo c F.limsSup = ∅
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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 = ∅
⊢ liminf f F ≤ f F.limsSup
have pos : ∀ (c : R) (c_lt : c < F.limsSup) (hc : Set.Ioo c F.limsSup = ∅), liminf f F ≤ f F.limsSup
Tactic: rcases h' with ⟨c, c_lt, hc⟩
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
have apply : ∀ (x : R), c < x → F.limsSup ≤ x
Tactic: apply (frequently_lt_of_lt_limsSup cobdd c_lt).mono
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ F.limsSup ≤ x
have by_contra! : ∀ (this : x < F.limsSup), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (hypothesis)
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
⊢ False
have this₁ : (Set.Ioo c F.limsSup).Nonempty
Tactic: have : (Set.Ioo c F.limsSup).Nonempty := ⟨x, ⟨hx, this⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (hypothesis)
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 = ∅
⊢ liminf f F ≤ f F.limsSup
have B : ∃ᶠ (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
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ liminf f F ≤ f F.limsSup
have apply : ∃ᶠ (i : R) in F, f i ≤ f F.limsSup
Tactic: apply liminf_le_of_frequently_le _ (bdd_above.isBoundedUnder f_decr)
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ liminf f F ≤ f F.limsSup
have neg : ∀ (H : f F.limsSup < liminf f F), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (hypothesis)
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
⊢ False
have not_bot : ¬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
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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 < F.limsSup, Set.Ioc l F.limsSup ⊆ {x : R | f x < liminf f F}
have apply : ∃ (l : R), l < F.limsSup
Tactic: apply exists_Ioc_subset_of_mem_nhds ((tendsto_order.1 f_cont.tendsto).2 _ H)
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ False
have neg : ∀ (l : R) (l_lt : l < F.limsSup) (h'l : Set.Ioc l F.limsSup ⊆ {x : R | f x < liminf f F}), 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
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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}
⊢ (Set.Ioo l F.limsSup).Nonempty
have contrapose! : ∀ (h' : Set.Ioo l F.limsSup = ∅), ∃ c < F.limsSup, Set.Ioo c F.limsSup = ∅
Tactic: contrapose! h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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}
⊢ False
have neg : ∀ (m : R) (l_m : l < m) (m_lt : m < F.limsSup), False
Tactic: obtain ⟨m, l_m, m_lt⟩ : (Set.Ioo l F.limsSup).Nonempty := by
      contrapose! h'
      exact ⟨l, l_lt, h'⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ liminf f F ≤ f m
have apply : ∃ᶠ (i : R) in F, f i ≤ f m
Tactic: apply liminf_le_of_frequently_le _ _
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ liminf f F ≤ f m
have apply₁ : IsBoundedUnder (fun (x1 x2 : S) ↦ x1 ≥ x2) F f
Tactic: apply liminf_le_of_frequently_le _ _
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
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
⊢ ∃ᶠ (i : R) in F, f i ≤ f m
have apply : ∀ (x : R), m < x → f x ≤ f m
Tactic: apply (frequently_lt_of_lt_limsSup cobdd m_lt).mono
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (hypothesis)
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
⊢ False
have B : liminf f F ≤ f m
Tactic: have B : F.liminf f ≤ f m := by
      apply liminf_le_of_frequently_le _ _
      · apply (frequently_lt_of_lt_limsSup cobdd m_lt).mono
        exact fun x hx ↦ f_decr hx.le
      · exact IsBounded.isBoundedUnder f_decr bdd_above
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (hypothesis)
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
B : liminf f F ≤ f m
⊢ False
have I : f m < liminf f F
Tactic: have I : f m < F.liminf f := h'l ⟨l_m, m_lt.le⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ (b : α), a < b
⊢ liminf f (𝓝[>] a) = ⨆ (r : α), ⨆ (_ : r > a), f r
have rw : Eq.{u_3 + 1} (α := β) (⨆ (i : α), ⨆ (_ : a < i), ⨅ a_1 ∈ Set.Ioo a i, f a_1) (⨆ (r : α), ⨆ (_ : r > a), f r)
Tactic: rw [(nhdsGT_basis_of_exists_gt hb).liminf_eq_iSup_iInf]
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ (b : α), a < b
⊢ Eq.{u_3 + 1} (α := β) (⨆ (i : α), ⨆ (_ : a < i), ⨅ a_1 ∈ Set.Ioo a i, f a_1) (⨆ (r : α), ⨆ (_ : r > a), f r)
have refine : ∀ (r : α) (hr : a < r), ∃ (i' : α) (_ : i' > a), ⨅ a_1 ∈ Set.Ioo a r, f a_1 ≤ f i'
Tactic: refine le_antisymm (iSup₂_mono' fun r hr ↦ ?_)
    (iSup₂_mono' fun r hr ↦ ⟨r, hr, le_iInf₂ fun i hi ↦ hf (Set.mem_Ioo.1 hi).2.le⟩)
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ (b : α), a < b
r : α
hr : a < r
⊢ ∃ (i' : α) (_ : i' > a), ⨅ a_1 ∈ Set.Ioo a r, f a_1 ≤ f i'
have obtain : ∀ (b : α) (hb : a < b ∧ b < r), ∃ (i' : α) (_ : i' > a), ⨅ a_1 ∈ Set.Ioo a r, f a_1 ≤ f i'
Tactic: obtain ⟨b, hb⟩ := exists_between hr
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ (b : α), b < a
⊢ liminf f (𝓝[<] a) = ⨆ (r : α), ⨆ (_ : r < a), f r
have rw : Eq.{u_3 + 1} (α := β) (⨆ (i : α), ⨆ (_ : i < a), ⨅ a_1 ∈ Set.Ioo i a, f a_1) (⨆ (r : α), ⨆ (_ : r < a), f r)
Tactic: rw [(nhdsLT_basis_of_exists_lt hb).liminf_eq_iSup_iInf]
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ (b : α), b < a
⊢ Eq.{u_3 + 1} (α := β) (⨆ (i : α), ⨆ (_ : i < a), ⨅ a_1 ∈ Set.Ioo i a, f a_1) (⨆ (r : α), ⨆ (_ : r < a), f r)
have refine : ∀ (r : α) (hr : r < a), ∃ (i' : α) (_ : i' < a), ⨅ a_1 ∈ Set.Ioo r a, f a_1 ≤ f i'
Tactic: refine le_antisymm (iSup₂_mono' fun r hr ↦ ?_)
    (iSup₂_mono' fun r hr ↦ ⟨r, hr, le_iInf₂ fun i hi ↦ hf (Set.mem_Ioo.1 hi).1.le⟩)
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ (b : α), b < a
r : α
hr : r < a
⊢ ∃ (i' : α) (_ : i' < a), ⨅ a_1 ∈ Set.Ioo r a, f a_1 ≤ f i'
have obtain : ∀ (b : α) (hb : r < b ∧ b < a), ∃ (i' : α) (_ : i' < a), ⨅ a_1 ∈ Set.Ioo r a, f a_1 ≤ f i'
Tactic: obtain ⟨b, hb⟩ := exists_between hr
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ (b : α), a < b
⊢ limsup f (𝓝[>] a) = ⨅ (r : α), ⨅ (_ : r > a), f r
have rw : Eq.{u_3 + 1} (α := β) (⨅ (i : α), ⨅ (_ : a < i), ⨆ a_1 ∈ Set.Ioo a i, f a_1) (⨅ (r : α), ⨅ (_ : r > a), f r)
Tactic: rw [(nhdsGT_basis_of_exists_gt hb).limsup_eq_iInf_iSup]
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ (b : α), a < b
⊢ Eq.{u_3 + 1} (α := β) (⨅ (i : α), ⨅ (_ : a < i), ⨆ a_1 ∈ Set.Ioo a i, f a_1) (⨅ (r : α), ⨅ (_ : r > a), f r)
have refine : ∀ (r : α) (hr : a < r), ∃ (i' : α) (_ : i' > a), f i' ≤ ⨆ a_1 ∈ Set.Ioo a r, f a_1
Tactic: refine le_antisymm
    (iInf₂_mono' fun r hr ↦ ⟨r, hr, iSup₂_le fun i hi ↦ hf (Set.mem_Ioo.1 hi).2.le⟩)
    (iInf₂_mono' fun r hr ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Monotone f
a : α
hb : ∃ (b : α), a < b
r : α
hr : a < r
⊢ ∃ (i' : α) (_ : i' > a), f i' ≤ ⨆ a_1 ∈ Set.Ioo a r, f a_1
have obtain : ∀ (b : α) (hb : a < b ∧ b < r), ∃ (i' : α) (_ : i' > a), f i' ≤ ⨆ a_1 ∈ Set.Ioo a r, f a_1
Tactic: obtain ⟨b, hb⟩ := exists_between hr
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ (b : α), b < a
⊢ limsup f (𝓝[<] a) = ⨅ (r : α), ⨅ (_ : r < a), f r
have rw : Eq.{u_3 + 1} (α := β) (⨅ (i : α), ⨅ (_ : i < a), ⨆ a_1 ∈ Set.Ioo i a, f a_1) (⨅ (r : α), ⨅ (_ : r < a), f r)
Tactic: rw [(nhdsLT_basis_of_exists_lt hb).limsup_eq_iInf_iSup]
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ (b : α), b < a
⊢ Eq.{u_3 + 1} (α := β) (⨅ (i : α), ⨅ (_ : i < a), ⨆ a_1 ∈ Set.Ioo i a, f a_1) (⨅ (r : α), ⨅ (_ : r < a), f r)
have refine : ∀ (r : α) (hr : r < a), ∃ (i' : α) (_ : i' < a), f i' ≤ ⨆ a_1 ∈ Set.Ioo r a, f a_1
Tactic: refine le_antisymm
    (iInf₂_mono' fun r hr ↦ ⟨r, hr, iSup₂_le fun i hi ↦ hf (Set.mem_Ioo.1 hi).1.le⟩)
    (iInf₂_mono' fun r hr ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.LiminfLimsup (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ (b : α), b < a
r : α
hr : r < a
⊢ ∃ (i' : α) (_ : i' < a), f i' ≤ ⨆ a_1 ∈ Set.Ioo r a, f a_1
have obtain : ∀ (b : α) (hb : r < b ∧ b < a), ∃ (i' : α) (_ : i' < a), f i' ≤ ⨆ a_1 ∈ Set.Ioo r a, f a_1
Tactic: obtain ⟨b, hb⟩ := exists_between hr