awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
obtain :
  ∀ (v : ℕ → α) (hvx : Tendsto v atTop (𝓝[≤] x)) (hvt : ∀ (n : ℕ), v n ∈ t),
    ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
obtain ⟨v, hvx, hvt⟩ := exists_seq_forall_of_frequently (htx.frequently_mem ht)

Premises used: Filter.exists_seq_forall_of_frequently, IsLUB.frequently_mem
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvx : Tendsto v atTop (𝓝[≤] x)
hvt : ∀ (n : ℕ), v n ∈ t
⊢ Tendsto v atTop (𝓝 x)

Tactic:
replace hvx := hvx.mono_right nhdsWithin_le_nhds
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
⊢ ∀ {n : ℕ}, v n < x

Tactic:
have hvx' : ∀ {n}, v n < x := (htx.1 (hvt _)).lt_of_ne (ne_of_mem_of_not_mem (hvt _) notMem)
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
⊢ ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l

Tactic:
have : ∀ k, ∀ᶠ l in atTop, v k < v l := fun k => hvx.eventually (lt_mem_nhds hvx')
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
choose :
  ∀ (N : (k : ℕ) → ℕ) (hN : ∀ (k : ℕ), k < N k) (hvN : ∀ (k : ℕ), v k < v (N k)),
    ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
choose N hN hvN using fun k => ((eventually_gt_atTop k).and (this k)).exists

Premises used: Filter.Eventually.and, Filter.Eventually.exists, Filter.eventually_gt_atTop
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : (k : ℕ) → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
⟨fun k => v (N^[k] 0), strictMono_nat_of_lt_succ fun _ => ?_, fun _ => hvx',
    hvx.comp (strictMono_nat_of_lt_succ fun _ => ?_).tendsto_atTop, fun _ => hvt _⟩

Premises used: strictMono_nat_of_lt_succ, StrictMono.tendsto_atTop, Nat.iterate, And.intro, Exists.intro, Filter.Tendsto.comp, OfNat.ofNat
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : (k : ℕ) → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
refine_1 : ∀ (x : ℕ), v (N^[x] 0) < v (N^[x + 1] 0)
refine_2 : ∀ (x : ℕ), N^[x] 0 < N^[x + 1] 0
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
refine ⟨fun k => v (N^[k] 0), strictMono_nat_of_lt_succ fun _ => ?_, fun _ => hvx',
    hvx.comp (strictMono_nat_of_lt_succ fun _ => ?_).tendsto_atTop, fun _ => hvt _⟩
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : (k : ℕ) → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x_1 : ℕ
refine_1 : v (N^[x_1] 0) < v (N (N^[x_1] 0))
⊢ v (N^[x_1] 0) < v (N^[x_1 + 1] 0)

Tactic:
rw [iterate_succ_apply']

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : (k : ℕ) → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x_1 : ℕ
⊢ v (N^[x_1] 0) < v (N (N^[x_1] 0))

Tactic:
hvN _
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : (k : ℕ) → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x_1 : ℕ
⊢ v (N^[x_1] 0) < v (N (N^[x_1] 0))

Tactic:
exact hvN _
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : (k : ℕ) → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x_1 : ℕ
refine_2 : N^[x_1] 0 < N (N^[x_1] 0)
⊢ N^[x_1] 0 < N^[x_1 + 1] 0

Tactic:
rw [iterate_succ_apply']

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : (k : ℕ) → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x_1 : ℕ
⊢ N^[x_1] 0 < N (N^[x_1] 0)

Tactic:
hN _
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : (k : ℕ) → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x_1 : ℕ
⊢ N^[x_1] 0 < N (N^[x_1] 0)

Tactic:
exact hN _
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
ht : t.Nonempty
pos : ∀ (h : x ∈ t), ∃ (u : ℕ → α), Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
neg : ∀ (h : x ∉ t), ∃ (u : ℕ → α), Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
⊢ ∃ (u : ℕ → α), Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
by_cases h : x ∈ t
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
ht : t.Nonempty
h : x ∈ t
⊢ ∃ (u : ℕ → α), Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
⟨fun _ => x, monotone_const, fun n => le_rfl, tendsto_const_nhds, fun _ => h⟩

Premises used: le_rfl, monotone_const, tendsto_const_nhds, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
ht : t.Nonempty
h : x ∈ t
⊢ ∃ (u : ℕ → α), Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
exact ⟨fun _ => x, monotone_const, fun n => le_rfl, tendsto_const_nhds, fun _ => h⟩
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
ht : t.Nonempty
h : x ∉ t
neg :
  ∀ (u : ℕ → α) (hu : StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t),
    ∃ (u : ℕ → α), Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
⊢ ∃ (u : ℕ → α), Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
rcases htx.exists_seq_strictMono_tendsto_of_notMem h ht with ⟨u, hu⟩

Premises used: IsLUB.exists_seq_strictMono_tendsto_of_notMem
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
ht : t.Nonempty
h : x ∉ t
u : ℕ → α
hu : StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
⊢ ∃ (u : ℕ → α), Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
⟨u, hu.1.monotone, fun n => (hu.2.1 n).le, hu.2.2⟩

Premises used: StrictMono.monotone, LT.lt.le, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
x : α
inst_3 : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
ht : t.Nonempty
h : x ∉ t
u : ℕ → α
hu : StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
⊢ ∃ (u : ℕ → α), Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
exact ⟨u, hu.1.monotone, fun n => (hu.2.1 n).le, hu.2.2⟩
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : FirstCountableTopology α
x y : α
hy : y < x
⊢ x ∉ Ioo y x

Tactic:
have hx : x ∉ Ioo y x := fun h => (lt_irrefl x h.2).elim
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : FirstCountableTopology α
x y : α
hy : y < x
hx : x ∉ Ioo y x
⊢ (Ioo y x).Nonempty

Tactic:
have ht : Set.Nonempty (Ioo y x) := nonempty_Ioo.2 hy
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : FirstCountableTopology α
x y : α
hy : y < x
hx : x ∉ Ioo y x
ht : (Ioo y x).Nonempty
rcases :
  ∀ (u : ℕ → α) (hu : StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ Ioo y x),
    ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
rcases (isLUB_Ioo hy).exists_seq_strictMono_tendsto_of_notMem hx ht with ⟨u, hu⟩

Premises used: isLUB_Ioo, IsLUB.exists_seq_strictMono_tendsto_of_notMem
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : FirstCountableTopology α
x y : α
hy : y < x
hx : x ∉ Ioo y x
ht : (Ioo y x).Nonempty
u : ℕ → α
hu : StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ Ioo y x
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
⟨u, hu.1, hu.2.2.symm⟩

Premises used: And.right, And.left, And.intro, Exists.intro, And.symm
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : FirstCountableTopology α
x y : α
hy : y < x
hx : x ∉ Ioo y x
ht : (Ioo y x).Nonempty
u : ℕ → α
hu : StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ Ioo y x
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
exact ⟨u, hu.1, hu.2.2.symm⟩
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : FirstCountableTopology α
x : α
⊢ ∃ (y : α), y < x

Tactic:
exists_lt x

Premises used: NoMinOrder.exists_lt
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : FirstCountableTopology α
x : α
obtain : ∀ (y : α) (hy : y < x), ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
obtain ⟨y, hy⟩ : ∃ y, y < x := exists_lt x

Premises used: NoMinOrder.exists_lt
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : FirstCountableTopology α
x y : α
hy : y < x
rcases :
  ∀ (u : ℕ → α) (hu_mono : StrictMono u) (hu_mem : ∀ (n : ℕ), u n ∈ Ioo y x) (hux : Tendsto u atTop (𝓝 x)),
    ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
rcases exists_seq_strictMono_tendsto' hy with ⟨u, hu_mono, hu_mem, hux⟩

Premises used: exists_seq_strictMono_tendsto'
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : FirstCountableTopology α
x y : α
hy : y < x
u : ℕ → α
hu_mono : StrictMono u
hu_mem : ∀ (n : ℕ), u n ∈ Ioo y x
hux : Tendsto u atTop (𝓝 x)
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
⟨u, hu_mono, fun n => (hu_mem n).2, hux⟩

Premises used: And.right, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : FirstCountableTopology α
x y : α
hy : y < x
u : ℕ → α
hu_mono : StrictMono u
hu_mem : ∀ (n : ℕ), u n ∈ Ioo y x
hux : Tendsto u atTop (𝓝 x)
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
exact ⟨u, hu_mono, fun n => (hu_mem n).2, hux⟩
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : FirstCountableTopology α
x : α
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝[<] x)

Tactic:
let ⟨u, hu, hx, h⟩ := exists_seq_strictMono_tendsto x
  ⟨u, hu, hx, tendsto_nhdsWithin_mono_right (range_subset_iff.2 hx) <| tendsto_nhdsWithin_range.2 h⟩

Premises used: Iff.mpr, _private.0.exists_seq_strictMono_tendsto_nhdsWithin.match_1, StrictMono, nhdsWithin, tendsto_nhdsWithin_mono_right, Exists, tendsto_nhdsWithin_range, Filter.atTop, And, Filter.Tendsto, And.intro, Exists.intro, exists_seq_strictMono_tendsto, Set.range_subset_iff, Set.Iio
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
S : Set α
hS : S.Nonempty
hS' : BddAbove S
rcases :
  ∀ (u : ℕ → α) (hu : Monotone u ∧ (∀ (n : ℕ), u n ≤ sSup S) ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S),
    ∃ (u : ℕ → α), Monotone u ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S
⊢ ∃ (u : ℕ → α), Monotone u ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S

Tactic:
rcases (isLUB_csSup hS hS').exists_seq_monotone_tendsto hS with ⟨u, hu⟩

Premises used: IsLUB.exists_seq_monotone_tendsto, isLUB_csSup
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
S : Set α
hS : S.Nonempty
hS' : BddAbove S
u : ℕ → α
hu : Monotone u ∧ (∀ (n : ℕ), u n ≤ sSup S) ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S
⊢ ∃ (u : ℕ → α), Monotone u ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S

Tactic:
⟨u, hu.1, hu.2.2⟩

Premises used: And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
S : Set α
hS : S.Nonempty
hS' : BddAbove S
u : ℕ → α
hu : Monotone u ∧ (∀ (n : ℕ), u n ≤ sSup S) ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S
⊢ ∃ (u : ℕ → α), Monotone u ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S

Tactic:
exact ⟨u, hu.1, hu.2.2⟩
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
obtain : ∀ (z : α) (hyz : z ∈ s) (hzx : z ∈ Ioo y x), (Ioo y x ∩ s).Nonempty
⊢ (Ioo y x ∩ s).Nonempty

Tactic:
obtain ⟨z, hyz, hzx⟩ := hs.exists_between hy

Premises used: Dense.exists_between
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
z : α
hyz : z ∈ s
hzx : z ∈ Ioo y x
⊢ (Ioo y x ∩ s).Nonempty

Tactic:
⟨z, mem_inter hzx hyz⟩

Premises used: Set.mem_inter, Set.Nonempty, Exists.intro
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
z : α
hyz : z ∈ s
hzx : z ∈ Ioo y x
⊢ (Ioo y x ∩ s).Nonempty

Tactic:
exact ⟨z, mem_inter hzx hyz⟩
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
⊢ (Ioo y x ∩ s).Nonempty

Tactic:
have hnonempty : (Ioo y x ∩ s).Nonempty := by
    obtain ⟨z, hyz, hzx⟩ := hs.exists_between hy
    exact ⟨z, mem_inter hzx hyz⟩
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
hnonempty : (Ioo y x ∩ s).Nonempty
⊢ IsLUB (Ioo y x ∩ s) x

Tactic:
have hx : IsLUB (Ioo y x ∩ s) x := hs.isLUB_inter_iff isOpen_Ioo |>.mpr <| isLUB_Ioo hy
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
hnonempty : (Ioo y x ∩ s).Nonempty
hx : IsLUB (Ioo y x ∩ s) x
⊢ x ∉ Ioo y x ∩ s

Tactic:
simp
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
hnonempty : (Ioo y x ∩ s).Nonempty
hx : IsLUB (Ioo y x ∩ s) x
apply :
  ∀ (a : ℕ → α),
    (StrictMono a ∧ (∀ (n : ℕ), a n < x) ∧ Tendsto a atTop (𝓝 x) ∧ ∀ (n : ℕ), a n ∈ Ioo y x ∩ s) →
      StrictMono a ∧ (∀ (n : ℕ), a n ∈ Ioo y x ∩ s) ∧ Tendsto a atTop (𝓝 x)
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x ∩ s) ∧ Tendsto u atTop (𝓝 x)

Tactic:
apply hx.exists_seq_strictMono_tendsto_of_notMem (by simp) hnonempty |>.imp

Premises used: Exists.imp, IsLUB.exists_seq_strictMono_tendsto_of_notMem
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
hnonempty : (Ioo y x ∩ s).Nonempty
hx : IsLUB (Ioo y x ∩ s) x
⊢ ∀ (a : ℕ → α),
    (StrictMono a ∧ (∀ (n : ℕ), a n < x) ∧ Tendsto a atTop (𝓝 x) ∧ ∀ (n : ℕ), a n ∈ Ioo y x ∩ s) →
      StrictMono a ∧ (∀ (n : ℕ), a n ∈ Ioo y x ∩ s) ∧ Tendsto a atTop (𝓝 x)

Tactic:
simp_all
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : FirstCountableTopology α
s : Set α
hs : Dense s
x : α
obtain : ∀ (y : α) (hy : y < x), ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Iio x ∩ s) ∧ Tendsto u atTop (𝓝 x)
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Iio x ∩ s) ∧ Tendsto u atTop (𝓝 x)

Tactic:
obtain ⟨y, hy⟩ := exists_lt x

Premises used: NoMinOrder.exists_lt
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
apply :
  ∀ (a : ℕ → α),
    StrictMono a ∧ (∀ (n : ℕ), a n ∈ Ioo (Exists.choose (p := fun (b : α) ↦ b < x) ⋯) x ∩ s) ∧ Tendsto a atTop (𝓝 x) →
      StrictMono a ∧ (∀ (n : ℕ), a n ∈ Iio x ∩ s) ∧ Tendsto a atTop (𝓝 x)
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Iio x ∩ s) ∧ Tendsto u atTop (𝓝 x)

Tactic:
apply hs.exists_seq_strictMono_tendsto_of_lt (exists_lt x).choose_spec |>.imp

Premises used: Exists.choose_spec, Exists.imp, NoMinOrder.exists_lt, Dense.exists_seq_strictMono_tendsto_of_lt
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
⊢ ∀ (a : ℕ → α),
    StrictMono a ∧ (∀ (n : ℕ), a n ∈ Ioo (Exists.choose (p := fun (b : α) ↦ b < x) ⋯) x ∩ s) ∧ Tendsto a atTop (𝓝 x) →
      StrictMono a ∧ (∀ (n : ℕ), a n ∈ Iio x ∩ s) ∧ Tendsto a atTop (𝓝 x)

Tactic:
simp_all
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
β : Type u_3
inst_3 : LinearOrder β
inst_4 : DenselyOrdered α
inst_5 : FirstCountableTopology α
f : β → α
x y : α
hf : DenseRange f
hmono : Monotone f
hlt : y < x
rcases :
  ∀ (u : ℕ → α) (hu : StrictMono u) (huyxf : ∀ (n : ℕ), u n ∈ Ioo y x ∩ range f) (hlim : Tendsto u atTop (𝓝 x)),
    ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
rcases Dense.exists_seq_strictMono_tendsto_of_lt hf hlt with ⟨u, hu, huyxf, hlim⟩

Premises used: Dense.exists_seq_strictMono_tendsto_of_lt
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
β : Type u_3
inst_3 : LinearOrder β
inst_4 : DenselyOrdered α
inst_5 : FirstCountableTopology α
f : β → α
x y : α
hf : DenseRange f
hmono : Monotone f
hlt : y < x
u : ℕ → α
hu : StrictMono u
huyxf : ∀ (n : ℕ), u n ∈ Ioo y x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
⊢ ∀ (n : ℕ), u n ∈ Ioo y x

Tactic:
have huyx (n : ℕ) : u n ∈ Ioo y x := (huyxf n).1