awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
inr : ∀ (b : β) (hb : b < c), ∀ᶠ (b_1 : α) in atTop, b < ⨆ (i : ι), u i b_1
inr₁ : ∀ (b : β) (hb : b > c), ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b
⊢ Tendsto (fun (r : α) ↦ ⨆ (i : ι), u i r) atTop (𝓝 c)

Tactic:
refine tendsto_order.mpr ⟨fun b hb ↦ ?_, fun b hb ↦ ?_⟩

Premises used: Iff.mpr, tendsto_order, And.intro
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b < c
inr : ∀ (r : α), b < ⨆ (i : ι), u i r
⊢ ∀ᶠ (b_1 : α) in atTop, b < ⨆ (i : ι), u i b_1

Tactic:
filter_upwards with r
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b < c
r : α
⊢ c ≤ u n0 r

Tactic:
have : c ≤ u n0 r := (h_anti n0).le_of_tendsto (h_all n0) r
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b < c
r : α
this : c ≤ u n0 r
⊢ b < ⨆ (i : ι), u i r

Tactic:
hb.trans_le (this.trans (le_iSup_iff.mpr fun b a ↦ a n0))

Premises used: Iff.mpr, LT.lt.trans_le, LE.le.trans, le_iSup_iff
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b < c
r : α
this : c ≤ u n0 r
⊢ b < ⨆ (i : ι), u i r

Tactic:
exact hb.trans_le (this.trans (le_iSup_iff.mpr fun b a ↦ a n0))

Premises used: Iff.mpr, LT.lt.trans_le, LE.le.trans, le_iSup_iff
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
simp : (if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c) < b
⊢ b' < b

Tactic:
simp only [b']
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
pos : ∀ (h : (Set.Ioo c b).Nonempty), h.some (s := Set.Ioo c b) < b
neg : ∀ (h : ¬(Set.Ioo c b).Nonempty), c < b
⊢ (if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c) < b

Tactic:
split_ifs with h
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
h : (Set.Ioo c b).Nonempty
⊢ h.some (s := Set.Ioo c b) < b

Tactic:
h.some_mem.2

Premises used: Set.Nonempty.some_mem, And.right
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
h : ¬(Set.Ioo c b).Nonempty
⊢ c < b

Tactic:
hb
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
h : (Set.Ioo c b).Nonempty
⊢ h.some (s := Set.Ioo c b) < b

Tactic:
exacts [h.some_mem.2, hb]

Premises used: Set.Nonempty.some_mem, And.right
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
⊢ b' < b

Tactic:
have hb'b : b' < b := by
    simp only [b']
    split_ifs with h
    exacts [h.some_mem.2, hb]
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
simp :
  ∀ᶠ (r : α) in atTop,
    LE.le.{u_8} (α := β) (limsup (fun (x : ι) ↦ u x r) cofinite)
      (if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c)
⊢ ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'

Tactic:
simp only [b']
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
pos :
  ∀ (h : (Set.Ioo c b).Nonempty), ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ h.some (s := Set.Ioo c b)
neg : ∀ (h : ¬(Set.Ioo c b).Nonempty), ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ c
⊢ ∀ᶠ (r : α) in atTop,
    LE.le.{u_8} (α := β) (limsup (fun (x : ι) ↦ u x r) cofinite)
      (if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c)

Tactic:
split_ifs with h
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
h : (Set.Ioo c b).Nonempty
r : α
hr : limsup (fun (i : ι) ↦ u i r) cofinite < h.some (s := Set.Ioo c b)
⊢ limsup (fun (x : ι) ↦ u x r) cofinite ≤ h.some (s := Set.Ioo c b)

Tactic:
hr.le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
h : (Set.Ioo c b).Nonempty
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α | (fun (b_1 : α) ↦ limsup (fun (i : ι) ↦ u i b_1) cofinite < h.some (s := Set.Ioo c b)) x} x →
          Membership.mem (γ := Set α)
            {x : α | (fun (r : α) ↦ limsup (fun (x : ι) ↦ u x r) cofinite ≤ h.some (s := Set.Ioo c b)) x} x}
      a
h₂ h₃ :
  ∀ (r : α) (hr : limsup (fun (i : ι) ↦ u i r) cofinite < h.some (s := Set.Ioo c b)),
    limsup (fun (x : ι) ↦ u x r) cofinite ≤ h.some (s := Set.Ioo c b)
⊢ ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ h.some (s := Set.Ioo c b)

Tactic:
filter_upwards [(tendsto_order.1 h_limsup).2 _ h.some_mem.1] with r hr using hr.le

Premises used: tendsto_order, Set.Nonempty.some_mem, And.right, And.left, Iff.mp
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
h : ¬(Set.Ioo c b).Nonempty
h₁ : ∀ (r : α) (hr : limsup (fun (i : ι) ↦ u i r) cofinite < b), limsup (fun (x : ι) ↦ u x r) cofinite ≤ c
⊢ ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ c

Tactic:
filter_upwards [(tendsto_order.1 h_limsup).2 b hb] with r hr

Premises used: tendsto_order, And.right, Iff.mp
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
h : ¬(Set.Ioo c b).Nonempty
r : α
hr : limsup (fun (i : ι) ↦ u i r) cofinite < b
h₁ : ∀ (h : c < limsup (fun (x : ι) ↦ u x r) cofinite), (Set.Ioo c b).Nonempty
⊢ limsup (fun (x : ι) ↦ u x r) cofinite ≤ c

Tactic:
contrapose! h
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
r : α
hr : limsup (fun (i : ι) ↦ u i r) cofinite < b
h : c < limsup (fun (x : ι) ↦ u x r) cofinite
⊢ (Set.Ioo c b).Nonempty

Tactic:
⟨limsup (u · r) cofinite, h, hr⟩

Premises used: Filter.limsup, Set.Nonempty, And.intro, Exists.intro, Filter.cofinite
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
r : α
hr : limsup (fun (i : ι) ↦ u i r) cofinite < b
h : c < limsup (fun (x : ι) ↦ u x r) cofinite
⊢ (Set.Ioo c b).Nonempty

Tactic:
exact ⟨limsup (u · r) cofinite, h, hr⟩
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
⊢ ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'

Tactic:
have : ∀ᶠ r in atTop, limsup (u · r) cofinite ≤ b' := by
    simp only [b']
    split_ifs with h
    · filter_upwards [(tendsto_order.1 h_limsup).2 _ h.some_mem.1] with r hr using hr.le
    · filter_upwards [(tendsto_order.1 h_limsup).2 b hb] with r hr
      contrapose! h
      exact ⟨limsup (u · r) cofinite, h, hr⟩
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
⊢ ∃ (r : α), ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'

Tactic:
simpa using this
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
inr :
  ∀ (r : α) (hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'), ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b
⊢ ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b

Tactic:
obtain ⟨r, hr⟩ : ∃ r, ∀ s ≥ r, limsup (u · s) cofinite ≤ b' := by simpa using this
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
inl : ∀ (h : Set.Ioo b' b = ∅), ∃ b'' ∈ Set.Ico b' b, ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
inr : ∀ (b'' : β) (hb'b'' : b' < b'') (hb''b : b'' < b), ∃ b'' ∈ Set.Ico b' b, ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
⊢ ∃ b'' ∈ Set.Ico b' b, ∀ᶠ (n : ι) in cofinite, u n r ≤ b''

Tactic:
rcases Set.eq_empty_or_nonempty (Set.Ioo b' b) with h | ⟨b'', hb'b'', hb''b⟩

Premises used: Set.eq_empty_or_nonempty, Set.Ioo
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
h : Set.Ioo b' b = ∅
⊢ ∃ b'' ∈ Set.Ico b' b, ∀ᶠ (n : ι) in cofinite, u n r ≤ b''

Tactic:
⟨b', ⟨le_rfl, hb'b⟩, ?_⟩

Premises used: le_rfl, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
h : Set.Ioo b' b = ∅
inl : ∀ᶠ (n : ι) in cofinite, u n r ≤ b'
⊢ ∃ b'' ∈ Set.Ico b' b, ∀ᶠ (n : ι) in cofinite, u n r ≤ b''

Tactic:
refine ⟨b', ⟨le_rfl, hb'b⟩, ?_⟩
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
h : Set.Ioo b' b = ∅
⊢ ∀ᶠ (a : ι) in cofinite, u a r < b

Tactic:
have h_lt := eventually_lt_of_limsup_lt ((hr r le_rfl).trans_lt hb'b)
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
h : Set.Ioo b' b = ∅
h_lt : ∀ᶠ (a : ι) in cofinite, u a r < b
h₁ : ∀ (n : ι) (hn : u n r < b), u n r ≤ b'
⊢ ∀ᶠ (n : ι) in cofinite, u n r ≤ b'

Tactic:
filter_upwards [h_lt] with n hn
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
h : Set.Ioo b' b = ∅
h_lt : ∀ᶠ (a : ι) in cofinite, u a r < b
n : ι
hn : u n r < b
h₁ : ∀ (h : b' < u n r), (Set.Ioo b' b).Nonempty
⊢ u n r ≤ b'

Tactic:
contrapose! h
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
h_lt : ∀ᶠ (a : ι) in cofinite, u a r < b
n : ι
hn : u n r < b
h : b' < u n r
⊢ (Set.Ioo b' b).Nonempty

Tactic:
⟨u n r, h, hn⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
h_lt : ∀ᶠ (a : ι) in cofinite, u a r < b
n : ι
hn : u n r < b
h : b' < u n r
⊢ (Set.Ioo b' b).Nonempty

Tactic:
exact ⟨u n r, h, hn⟩
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb'b'' : b' < b''
hb''b : b'' < b
⊢ ∃ b'' ∈ Set.Ico b' b, ∀ᶠ (n : ι) in cofinite, u n r ≤ b''

Tactic:
⟨b'', ⟨hb'b''.le, hb''b⟩ , ?_⟩

Premises used: LT.lt.le, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_7
β : Type u_8
inst : ConditionallyCompleteLattice α
inst_1 : CompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
u : ι → α → β
c : β
h_all : ∀ (i : ι), Tendsto (u i) atTop (𝓝 c)
h_limsup : Tendsto (fun (r : α) ↦ limsup (fun (i : ι) ↦ u i r) cofinite) atTop (𝓝 c)
h_anti : ∀ (i : ι), Antitone (u i)
n0 : ι
b : β
hb : b > c
b' : β := if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
hb'b : b' < b
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb'b'' : b' < b''
hb''b : b'' < b
inr : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
⊢ ∃ b'' ∈ Set.Ico b' b, ∀ᶠ (n : ι) in cofinite, u n r ≤ b''

Tactic:
refine ⟨b'', ⟨hb'b''.le, hb''b⟩ , ?_⟩