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 : ι
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
⊢ ∀ᶠ (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'
b'' : β
hb'b'' : b' < b''
hb''b : b'' < b
h_lt : ∀ᶠ (a : ι) in cofinite, u a r < b''
n : ι
hn : u n r < b''
⊢ u n r ≤ b''

Tactic:
hn.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
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
h_lt : ∀ᶠ (a : ι) in cofinite, u a r < b''
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (a : ι) ↦ u a r < b'') x} x →
          Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ u n r ≤ b'') x} x}
      a
h₁ 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 using hn.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
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
inr :
  ∀ (b'' : β) (hb''b : b'' ∈ Set.Ico b' b) (hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''),
    ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b
⊢ ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b

Tactic:
obtain ⟨b'', hb''b, hb''⟩ : ∃ b'' ∈ Set.Ico b' b, ∀ᶠ n in cofinite, u n r ≤ b'' := by
    rcases Set.eq_empty_or_nonempty (Set.Ioo b' b) with h | ⟨b'', hb'b'', hb''b⟩
    · refine ⟨b', ⟨le_rfl, hb'b⟩, ?_⟩
      have h_lt := eventually_lt_of_limsup_lt ((hr r le_rfl).trans_lt hb'b)
      filter_upwards [h_lt] with n hn
      contrapose! h
      exact ⟨u n r, h, hn⟩
    · refine ⟨b'', ⟨hb'b''.le, hb''b⟩ , ?_⟩
      have h_lt := eventually_lt_of_limsup_lt ((hr r le_rfl).trans_lt hb'b'')
      filter_upwards [h_lt] with n hn using hn.le

Premises used: Set.Ico, 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
this_1 : ∀ᶠ (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'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
n : ι
this : ∀ᶠ (r : α) in atTop, u n r ≤ b'
⊢ ∃ (a : α), ∀ (b : α), a ≤ b → u n b ≤ b'

Tactic:
simp only [eventually_atTop, ge_iff_le] at this

Premises used: ge_iff_le, Filter.eventually_atTop
-- 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_1 : ∀ᶠ (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'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
n : ι
this : ∃ (a : α), ∀ (b : α), a ≤ b → u n b ≤ b'
rcases : ∀ (r : α) (hr : ∀ (b : α), r ≤ b → u n b ≤ b'), ∃ (r : α), ∀ s ≥ r, u n s ≤ b''
⊢ ∃ (r : α), ∀ s ≥ r, u n s ≤ b''

Tactic:
rcases this with ⟨r, 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_1 : α
hr_1 : ∀ s ≥ r_1, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r_1 ≤ b''
n : ι
r : α
hr : ∀ (b : α), r ≤ b → u n b ≤ b'
⊢ ∃ (r : α), ∀ s ≥ r, u n s ≤ b''

Tactic:
⟨r, fun s hs ↦ (hr s hs).trans hb''b.1⟩

Premises used: And.left, Exists.intro, LE.le.trans
-- 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_1 : α
hr_1 : ∀ s ≥ r_1, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r_1 ≤ b''
n : ι
r : α
hr : ∀ (b : α), r ≤ b → u n b ≤ b'
⊢ ∃ (r : α), ∀ s ≥ r, u n s ≤ b''

Tactic:
exact ⟨r, fun s hs ↦ (hr s hs).trans hb''b.1⟩
-- 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'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
n : ι
suffices : ∀ᶠ (r : α) in atTop, u n r ≤ b'
⊢ ∃ (r : α), ∀ s ≥ r, u n s ≤ b''

Tactic:
suffices ∀ᶠ r in atTop, u n r ≤ b' by
      simp only [eventually_atTop, ge_iff_le] at this
      rcases this with ⟨r, hr⟩
      exact ⟨r, fun s hs ↦ (hr s hs).trans hb''b.1⟩
-- 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'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
n : ι
simp : ∀ᶠ (r : α) in atTop, u n r ≤ if h : (Set.Ioo c b).Nonempty then h.some (s := Set.Ioo c b) else c
⊢ ∀ᶠ (r : α) in atTop, u n r ≤ 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
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'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
n : ι
pos : ∀ (h : (Set.Ioo c b).Nonempty), ∀ᶠ (r : α) in atTop, u n r ≤ h.some (s := Set.Ioo c b)
neg : ∀ (h : ¬(Set.Ioo c b).Nonempty), ∀ᶠ (r : α) in atTop, u n r ≤ c
⊢ ∀ᶠ (r : α) in atTop, u n r ≤ 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
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'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
n : ι
h : (Set.Ioo c b).Nonempty
h₁ : ∀ (r : α) (hr : u n r < h.some (s := Set.Ioo c b)), u n r ≤ h.some (s := Set.Ioo c b)
⊢ ∀ᶠ (r : α) in atTop, u n r ≤ h.some (s := Set.Ioo c b)

Tactic:
filter_upwards [(tendsto_order.1 (h_all n)).2 _ h.some_mem.1] with r hr

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
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r_1 : α
hr_1 : ∀ s ≥ r_1, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r_1 ≤ b''
n : ι
h : (Set.Ioo c b).Nonempty
r : α
hr : u n r < h.some (s := Set.Ioo c b)
⊢ u n r ≤ 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
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r_1 : α
hr_1 : ∀ s ≥ r_1, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r_1 ≤ b''
n : ι
h : (Set.Ioo c b).Nonempty
r : α
hr : u n r < h.some (s := Set.Ioo c b)
⊢ u n r ≤ h.some (s := Set.Ioo c b)

Tactic:
exact 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
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'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
n : ι
h : ¬(Set.Ioo c b).Nonempty
h₁ : ∀ (r : α) (hr : u n r < b), u n r ≤ c
⊢ ∀ᶠ (r : α) in atTop, u n r ≤ c

Tactic:
filter_upwards [(tendsto_order.1 (h_all n)).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
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r_1 : α
hr_1 : ∀ s ≥ r_1, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r_1 ≤ b''
n : ι
h : ¬(Set.Ioo c b).Nonempty
r : α
hr : u n r < b
h₁ : ∀ (h : c < u n r), (Set.Ioo c b).Nonempty
⊢ u n r ≤ 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
this : ∀ᶠ (r : α) in atTop, limsup (fun (x : ι) ↦ u x r) cofinite ≤ b'
r_1 : α
hr_1 : ∀ s ≥ r_1, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r_1 ≤ b''
n : ι
r : α
hr : u n r < b
h : c < u n r
⊢ (Set.Ioo c b).Nonempty

Tactic:
⟨u n r, h, hr⟩

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_1 : α
hr_1 : ∀ s ≥ r_1, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r_1 ≤ b''
n : ι
r : α
hr : u n r < b
h : c < u n r
⊢ (Set.Ioo c b).Nonempty

Tactic:
exact ⟨u n r, 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 : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
⊢ ∀ (n : ι), ∃ (r : α), ∀ s ≥ r, u n s ≤ b''

Tactic:
have A (n) : ∃ r, ∀ s ≥ r, u n s ≤ b'' := by
    suffices ∀ᶠ r in atTop, u n r ≤ b' by
      simp only [eventually_atTop, ge_iff_le] at this
      rcases this with ⟨r, hr⟩
      exact ⟨r, fun s hs ↦ (hr s hs).trans hb''b.1⟩
    simp only [b']
    split_ifs with h
    · filter_upwards [(tendsto_order.1 (h_all n)).2 _ h.some_mem.1] with r hr
      exact hr.le
    · filter_upwards [(tendsto_order.1 (h_all n)).2 b hb] with r hr
      contrapose! h
      exact ⟨u n r, 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 : α
hr : ∀ s ≥ r, limsup (fun (x : ι) ↦ u x s) cofinite ≤ b'
b'' : β
hb''b : b'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
A : ∀ (n : ι), ∃ (r : α), ∀ s ≥ r, u n s ≤ b''
inr : ∀ (rs : (n : ι) → α) (hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''), ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b
⊢ ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b

Tactic:
choose rs hrs using A
-- 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'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : (n : ι) → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
inr : ∃ (a : α), ∀ (b_1 : α), a ≤ b_1 → ⨆ (i : ι), u i b_1 < b
⊢ ∀ᶠ (b_1 : α) in atTop, ⨆ (i : ι), u i b_1 < b

Tactic:
simp only [eventually_atTop, ge_iff_le]

Premises used: ge_iff_le, Filter.eventually_atTop
-- 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'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : (n : ι) → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
⊢ ∃ (a : α), ∀ (b_1 : α), a ≤ b_1 → ⨆ (i : ι), u i b_1 < b

Tactic:
⟨r ⊔ ⨆ n : {n | b'' < u n r}, rs n, fun v hv ↦ ?_⟩

Premises used: iSup, Max.max, Exists.intro, Subtype.val
-- 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'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : (n : ι) → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
inr : ∀ (v : α) (hv : r ⊔ ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι) ≤ v), ⨆ (i : ι), u i v < b
⊢ ∃ (a : α), ∀ (b_1 : α), a ≤ b_1 → ⨆ (i : ι), u i b_1 < b

Tactic:
refine ⟨r ⊔ ⨆ n : {n | b'' < u n r}, rs n, fun v hv ↦ ?_⟩
-- 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'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : (n : ι) → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι) ≤ v
apply : ∀ (n : ι), u n v ≤ b''
⊢ ⨆ (i : ι), u i v < b

Tactic:
apply lt_of_le_of_lt (iSup_le fun n ↦ ?_) hb''b.2

Premises used: lt_of_le_of_lt, And.right, iSup_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
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'' ∈ Set.Ico b' b
hb'' : ∀ᶠ (n : ι) in cofinite, u n r ≤ b''
rs : (n : ι) → α
hrs : ∀ (n : ι), ∀ s ≥ rs n, u n s ≤ b''
v : α
hv : r ⊔ ⨆ (n : (↑{n : ι | b'' < u n r} : Type u_1)), rs (↑n : ι) ≤ v
n : ι
pos : ∀ (hn : b'' < u n r), u n v ≤ b''
neg : ∀ (hn : ¬b'' < u n r), u n v ≤ b''
⊢ u n v ≤ b''

Tactic:
by_cases hn : b'' < u n r