awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
i : α
hic : i < c
j : α
hj : j ∈ s
hij : i < j
hjc : j ≤ c
⊢ Ioi i ∈ f
have h : ∀ a_1 ∈ (Icc a j)ᶜ, a_1 ∈ Icc a b → a_1 ∈ Ioi i
Tactic: filter_upwards [f.compl_mem_iff_notMem.mpr hj.2, hfab]
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
⊢ False
have this : ∀ (i : α) (hic : i < c), Ioi i ∈ f
Tactic: have (i : _) (hic : i < c) : Ioi i ∈ f := by
    have ⟨j, hj, hij, hjc⟩ := hsc.exists_between hic
    filter_upwards [f.compl_mem_iff_notMem.mpr hj.2, hfab]; grind
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this : ∀ (i : α) (hic : i < c), Ioi i ∈ f
⊢ False
have have : ∀ (x : α) (hx : c < x) (hxf : Iio x ∉ f), False
Tactic: have ⟨x, hx, hxf⟩ : ∃ x, c < x ∧ Iio x ∉ f := by simpa [nhds_eq_order, eq_true this] using hf c hc
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this : ∀ (i : α) (hic : i < c), Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
⊢ False
have this₁ : Icc a c ∉ f
Tactic: have : Icc a c ∉ f := mt (mem_of_superset · (by grind)) hxf
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this_1 : ∀ (i : α) (hic : i < c), Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this : Icc a c ∉ f
⊢ False
have this₁ : x ∈ Icc a b
Tactic: have : x ∈ Icc a b := ⟨by grind, le_of_not_gt fun h ↦ hxf (mem_of_superset hfab (by grind))⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this_1 : ∀ (i : α) (hic : i < c), Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this_2 : Icc a c ∉ f
this : x ∈ Icc a b
⊢ False
have this₁ : Icc a x ∈ f
Tactic: have : Icc a x ∈ f := by simpa [s, this.1, this.2] using notMem_of_csSup_lt hx ⟨b, hsb⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
h : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ (↑f : Filter α)
hf : ∀ (x : α) (_ : x ∈ Icc a b), ¬(↑f : Filter α) ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x : α | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this_1 : ∀ (i : α) (hic : i < c), Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this_2 : Icc a c ∉ f
this_3 : x ∈ Icc a b
this : Icc a x ∈ f
⊢ {x} ∈ f
have h : ∀ a_1 ∈ (Iio x)ᶜ, a_1 ∈ Icc a x → Membership.mem (γ := Set α) {x} a_1
Tactic: filter_upwards [f.compl_mem_iff_notMem.mpr hxf, this]
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hs : IsClosed[inst_1] s
⊢ IsClosed[inst_1] (↑(upperClosure s) : Set α)
have inl : ∀ (hs : IsClosed[inst_1] ∅), IsClosed[inst_1] (↑(upperClosure ∅) : Set α)
Tactic: obtain rfl | h₁ := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hs : IsClosed[inst_1] s
inl : ∀ (hs : IsClosed[inst_1] ∅), IsClosed[inst_1] (↑(upperClosure ∅) : Set α)
⊢ IsClosed[inst_1] (↑(upperClosure s) : Set α)
have inr : ∀ (h₁ : s.Nonempty), IsClosed[inst_1] (↑(upperClosure s) : Set α)
Tactic: obtain rfl | h₁ := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hs : IsClosed[inst_1] s
h₁ : s.Nonempty
⊢ IsClosed[inst_1] (↑(upperClosure s) : Set α)
have pos : ∀ (h₂ : BddBelow s), IsClosed[inst_1] (↑(upperClosure s) : Set α)
Tactic: by_cases h₂ : BddBelow s
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
s : Set α
hs : IsClosed[inst_1] s
h₁ : s.Nonempty
pos : ∀ (h₂ : BddBelow s), IsClosed[inst_1] (↑(upperClosure s) : Set α)
⊢ IsClosed[inst_1] (↑(upperClosure s) : Set α)
have neg : ∀ (h₂ : ¬BddBelow s), IsClosed[inst_1] (↑(upperClosure s) : Set α)
Tactic: by_cases h₂ : BddBelow s
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
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
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
have 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
Tactic: obtain ⟨v, hvx, hvt⟩ := exists_seq_forall_of_frequently (htx.frequently_mem ht)
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
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
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
have hvx₁ : Tendsto v atTop (𝓝 x)
Tactic: replace hvx := hvx.mono_right nhdsWithin_le_nhds
Cleared hypotheses: hvx
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
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)
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
have hvx' : ∀ {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)
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
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
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
have this : ∀ (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')
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
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
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
have 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
Tactic: choose N hN hvN using fun k => ((eventually_gt_atTop k).and (this k)).exists
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
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
have refine_1 : ∀ (x : ℕ), v (N^[x] 0) < v (N^[x + 1] 0)
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 _⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
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)
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
have refine_2 : ∀ (x : ℕ), N^[x] 0 < N^[x + 1] 0
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 _⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
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^[x_1 + 1] 0)
have refine_1 : v (N^[x_1] 0) < v (N (N^[x_1] 0))
Tactic: rw [iterate_succ_apply']
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
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^[x_1 + 1] 0
have refine_2 : N^[x_1] 0 < N (N^[x_1] 0)
Tactic: rw [iterate_succ_apply']
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
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
⊢ ∃ (u : ℕ → α), Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
have pos : ∀ (h : x ∈ t), ∃ (u : ℕ → α), Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
Tactic: by_cases h : x ∈ t
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
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
⊢ ∃ (u : ℕ → α), Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
have neg : ∀ (h : x ∉ t), ∃ (u : ℕ → α), Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
Tactic: by_cases h : x ∈ t
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
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
have 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
Tactic: rcases htx.exists_seq_strictMono_tendsto_of_notMem h ht with ⟨u, hu⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
Goal:
α : Type u_3
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : DenselyOrdered α
inst_3 : OrderTopology α
inst_4 : FirstCountableTopology α
x y : α
hy : y < x
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)
have hx : x ∉ Ioo y x
Tactic: have hx : x ∉ Ioo y x := fun h => (lt_irrefl x h.2).elim
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
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
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)
have ht : (Ioo y x).Nonempty
Tactic: have ht : Set.Nonempty (Ioo y x) := nonempty_Ioo.2 hy
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
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 : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)
have 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)
Tactic: rcases (isLUB_Ioo hy).exists_seq_strictMono_tendsto_of_notMem hx ht with ⟨u, hu⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
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)
have obtain : ∀ (y : α) (hy : y < x), ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)
Tactic: obtain ⟨y, hy⟩ : ∃ y, y < x := exists_lt x
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
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 : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x)
have 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)
Tactic: rcases exists_seq_strictMono_tendsto' hy with ⟨u, hu_mono, hu_mem, hux⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
Goal:
α : Type u_3
inst : ConditionallyCompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
S : Set α
hS : S.Nonempty
hS' : BddAbove S
⊢ ∃ (u : ℕ → α), Monotone u ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S
have 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
Tactic: rcases (isLUB_csSup hS hS').exists_seq_monotone_tendsto hS with ⟨u, hu⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
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
have obtain : ∀ (z : α) (hyz : z ∈ s) (hzx : z ∈ Ioo y x), (Ioo y x ∩ s).Nonempty
Tactic: obtain ⟨z, hyz, hzx⟩ := hs.exists_between hy
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
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
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x ∩ s) ∧ Tendsto u atTop (𝓝 x)
have hnonempty : (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⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
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
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x ∩ s) ∧ Tendsto u atTop (𝓝 x)
have hx : 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
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
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
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x ∩ s) ∧ Tendsto u atTop (𝓝 x)
have 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)
Tactic: apply hx.exists_seq_strictMono_tendsto_of_notMem (by simp) hnonempty |>.imp
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
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 : α
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Iio x ∩ s) ∧ Tendsto u atTop (𝓝 x)
have obtain : ∀ (y : α) (hy : y < x), ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Iio x ∩ s) ∧ Tendsto u atTop (𝓝 x)
Tactic: obtain ⟨y, hy⟩ := exists_lt x
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
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
⊢ ∃ (u : ℕ → α), StrictMono u ∧ (∀ (n : ℕ), u n ∈ Iio x ∩ s) ∧ Tendsto u atTop (𝓝 x)
have apply : ∀ (a : ℕ → α),
  StrictMono a ∧ (∀ (n : ℕ), a n ∈ Ioo (Exists.choose (p := fun (b : α) ↦ b < x) sorry) x ∩ s) ∧ Tendsto a atTop (𝓝 x) →
    StrictMono a ∧ (∀ (n : ℕ), a n ∈ Iio x ∩ s) ∧ Tendsto a atTop (𝓝 x)
Tactic: apply hs.exists_seq_strictMono_tendsto_of_lt (exists_lt x).choose_spec |>.imp
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
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 : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
have 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)
Tactic: rcases Dense.exists_seq_strictMono_tendsto_of_lt hf hlt with ⟨u, hu, huyxf, hlim⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
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)
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
have huyx : ∀ (n : ℕ), u n ∈ Ioo y x
Tactic: have huyx (n : ℕ) : u n ∈ Ioo y x := (huyxf n).1
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
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)
huyx : ∀ (n : ℕ), u n ∈ Ioo y x
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
have huf : ∀ (n : ℕ), u n ∈ range f
Tactic: have huf (n : ℕ) : u n ∈ range f := (huyxf n).2
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (goal)
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)
huyx : ∀ (n : ℕ), u n ∈ Ioo y x
huf : ∀ (n : ℕ), u n ∈ range f
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
have choose : ∀ (v : (n : ℕ) → β) (hv : ∀ (n : ℕ), f (v n) = u n),
  ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
Tactic: choose v hv using huf
Cleared hypotheses: huf
-- Lean 4 proof step from Mathlib.Topology.Order.IsLUB (hypothesis)
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)
huyx : ∀ (n : ℕ), u n ∈ Ioo y x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
have hu₁ : StrictMono (f ∘ v)
Tactic: obtain rfl : f ∘ v = u := funext hv
Cleared hypotheses: u, hu, huyxf, hlim, huyx, hv