awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
huyx : ∀ (n : ℕ), u n ∈ Ioo y x
⊢ ∀ (n : ℕ), u n ∈ range f

Tactic:
have huf (n : ℕ) : u n ∈ range f := (huyxf n).2
-- 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)
huyx : ∀ (n : ℕ), u n ∈ Ioo y x
huf : ∀ (n : ℕ), u n ∈ range f
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)
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
choose v hv using huf
-- 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)
huyx : ∀ (n : ℕ), u n ∈ Ioo y x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
⊢ f ∘ v = u

Tactic:
funext hv

Premises used: funext
-- 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)
huyx : ∀ (n : ℕ), u n ∈ Ioo y x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
⊢ StrictMono (f ∘ v)

Tactic:
obtain rfl : f ∘ v = u := funext hv

Premises used: funext, rfl
-- 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)
huyx : ∀ (n : ℕ), u n ∈ Ioo y x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
hu₁ : StrictMono (f ∘ v)
⊢ ∀ (n : ℕ), (f ∘ v) n ∈ Ioo y x ∩ range f

Tactic:
obtain rfl : f ∘ v = u := funext hv

Premises used: funext, rfl
-- 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)
huyx : ∀ (n : ℕ), u n ∈ Ioo y x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
hu₁ : StrictMono (f ∘ v)
huyxf₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Ioo y x ∩ range f
⊢ Tendsto (f ∘ v) atTop (𝓝 x)

Tactic:
obtain rfl : f ∘ v = u := funext hv

Premises used: funext, rfl
-- 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)
huyx : ∀ (n : ℕ), u n ∈ Ioo y x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
hu₁ : StrictMono (f ∘ v)
huyxf₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Ioo y x ∩ range f
hlim₁ : Tendsto (f ∘ v) atTop (𝓝 x)
⊢ ∀ (n : ℕ), (f ∘ v) n ∈ Ioo y x

Tactic:
obtain rfl : f ∘ v = u := funext hv

Premises used: funext, rfl
-- 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)
huyx : ∀ (n : ℕ), u n ∈ Ioo y x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
hu₁ : StrictMono (f ∘ v)
huyxf₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Ioo y x ∩ range f
hlim₁ : Tendsto (f ∘ v) atTop (𝓝 x)
huyx₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Ioo y x
⊢ ∀ (n : ℕ), f (v n) = (f ∘ v) n

Tactic:
obtain rfl : f ∘ v = u := funext hv

Premises used: funext, rfl
-- 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
v : (n : ℕ) → β
hu : StrictMono (f ∘ v)
huyxf : ∀ (n : ℕ), (f ∘ v) n ∈ Ioo y x ∩ range f
hlim : Tendsto (f ∘ v) atTop (𝓝 x)
huyx : ∀ (n : ℕ), (f ∘ v) n ∈ Ioo y x
hv : ∀ (n : ℕ), f (v n) = (f ∘ v) n
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
⟨v, fun a b hlt ↦ hmono.reflect_lt <| hu hlt, huyx, hlim⟩

Premises used: Monotone.reflect_lt, And.intro, Exists.intro
-- 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
v : (n : ℕ) → β
hu : StrictMono (f ∘ v)
huyxf : ∀ (n : ℕ), (f ∘ v) n ∈ Ioo y x ∩ range f
hlim : Tendsto (f ∘ v) atTop (𝓝 x)
huyx : ∀ (n : ℕ), (f ∘ v) n ∈ Ioo y x
hv : ∀ (n : ℕ), f (v n) = (f ∘ v) n
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo y x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
exact ⟨v, fun a b hlt ↦ hmono.reflect_lt <| hu hlt, huyx, hlim⟩
-- 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 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
rcases :
  ∀ (u : ℕ → α) (hu : StrictMono u) (huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f) (hlim : Tendsto u atTop (𝓝 x)),
    ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
rcases Dense.exists_seq_strictMono_tendsto hf x with ⟨u, hu, huxf, hlim⟩

Premises used: Dense.exists_seq_strictMono_tendsto
-- 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 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
⊢ ∀ (n : ℕ), u n ∈ Iio x

Tactic:
have hux (n : ℕ) : u n ∈ Iio x := (huxf n).1
-- 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 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
hux : ∀ (n : ℕ), u n ∈ Iio x
⊢ ∀ (n : ℕ), u n ∈ range f

Tactic:
have huf (n : ℕ) : u n ∈ range f := (huxf n).2
-- 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 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
hux : ∀ (n : ℕ), u n ∈ Iio x
huf : ∀ (n : ℕ), u n ∈ range f
choose :
  ∀ (v : (n : ℕ) → β) (hv : ∀ (n : ℕ), f (v n) = u n),
    ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
choose v hv using huf
-- 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 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
hux : ∀ (n : ℕ), u n ∈ Iio x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
⊢ f ∘ v = u

Tactic:
funext hv

Premises used: funext
-- 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 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
hux : ∀ (n : ℕ), u n ∈ Iio x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
⊢ StrictMono (f ∘ v)

Tactic:
obtain rfl : f ∘ v = u := funext hv

Premises used: funext, rfl
-- 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 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
hux : ∀ (n : ℕ), u n ∈ Iio x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
hu₁ : StrictMono (f ∘ v)
⊢ ∀ (n : ℕ), (f ∘ v) n ∈ Iio x ∩ range f

Tactic:
obtain rfl : f ∘ v = u := funext hv

Premises used: funext, rfl
-- 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 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
hux : ∀ (n : ℕ), u n ∈ Iio x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
hu₁ : StrictMono (f ∘ v)
huxf₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Iio x ∩ range f
⊢ Tendsto (f ∘ v) atTop (𝓝 x)

Tactic:
obtain rfl : f ∘ v = u := funext hv

Premises used: funext, rfl
-- 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 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
hux : ∀ (n : ℕ), u n ∈ Iio x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
hu₁ : StrictMono (f ∘ v)
huxf₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Iio x ∩ range f
hlim₁ : Tendsto (f ∘ v) atTop (𝓝 x)
⊢ ∀ (n : ℕ), (f ∘ v) n ∈ Iio x

Tactic:
obtain rfl : f ∘ v = u := funext hv

Premises used: funext, rfl
-- 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 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
u : ℕ → α
hu : StrictMono u
huxf : ∀ (n : ℕ), u n ∈ Iio x ∩ range f
hlim : Tendsto u atTop (𝓝 x)
hux : ∀ (n : ℕ), u n ∈ Iio x
v : (n : ℕ) → β
hv : ∀ (n : ℕ), f (v n) = u n
hu₁ : StrictMono (f ∘ v)
huxf₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Iio x ∩ range f
hlim₁ : Tendsto (f ∘ v) atTop (𝓝 x)
hux₁ : ∀ (n : ℕ), (f ∘ v) n ∈ Iio x
⊢ ∀ (n : ℕ), f (v n) = (f ∘ v) n

Tactic:
obtain rfl : f ∘ v = u := funext hv

Premises used: funext, rfl
-- 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 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
v : (n : ℕ) → β
hu : StrictMono (f ∘ v)
huxf : ∀ (n : ℕ), (f ∘ v) n ∈ Iio x ∩ range f
hlim : Tendsto (f ∘ v) atTop (𝓝 x)
hux : ∀ (n : ℕ), (f ∘ v) n ∈ Iio x
hv : ∀ (n : ℕ), f (v n) = (f ∘ v) n
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
⟨v, fun a b hlt ↦ hmono.reflect_lt <| hu hlt, hux, hlim⟩

Premises used: Monotone.reflect_lt, And.intro, Exists.intro
-- 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 : NoMinOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
v : (n : ℕ) → β
hu : StrictMono (f ∘ v)
huxf : ∀ (n : ℕ), (f ∘ v) n ∈ Iio x ∩ range f
hlim : Tendsto (f ∘ v) atTop (𝓝 x)
hux : ∀ (n : ℕ), (f ∘ v) n ∈ Iio x
hv : ∀ (n : ℕ), f (v n) = (f ∘ v) n
⊢ ∃ (u : ℕ → β), StrictMono u ∧ (∀ (n : ℕ), f (u n) ∈ Iio x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
exact ⟨v, fun a b hlt ↦ hmono.reflect_lt <| hu hlt, hux, hlim⟩
-- 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 : IsGLB t x
notMem : x ∉ t
ht : t.Nonempty
⊢ ∃ (u : ℕ → α), StrictAnti u ∧ (∀ (n : ℕ), x < u n) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
IsLUB.exists_seq_strictMono_tendsto_of_notMem (α := αᵒᵈ) htx notMem ht

Premises used: Set.Mem, StrictAnti, IsLUB.exists_seq_strictMono_tendsto_of_notMem, OrderDual
-- 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 : IsGLB t x
ht : t.Nonempty
⊢ ∃ (u : ℕ → α), Antitone u ∧ (∀ (n : ℕ), x ≤ u n) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
IsLUB.exists_seq_monotone_tendsto (α := αᵒᵈ) htx ht

Premises used: Set.Mem, Antitone, IsLUB.exists_seq_monotone_tendsto, OrderDual
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : FirstCountableTopology α
x y : α
hy : x < y
⊢ ∃ (u : ℕ → α), StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo x y) ∧ Tendsto u atTop (𝓝 x)

Tactic:
simpa using exists_seq_strictMono_tendsto' (α := αᵒᵈ) (OrderDual.toDual_lt_toDual.2 hy)

Premises used: Iff.mpr, OrderDual.toDual_lt_toDual, 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 : NoMaxOrder α
inst_5 : FirstCountableTopology α
x : α
⊢ ∃ (u : ℕ → α), StrictAnti u ∧ (∀ (n : ℕ), x < u n) ∧ Tendsto u atTop (𝓝 x)

Tactic:
exists_seq_strictMono_tendsto (α := αᵒᵈ) x

Premises used: StrictAnti, exists_seq_strictMono_tendsto, OrderDual
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMaxOrder α
inst_5 : FirstCountableTopology α
x : α
⊢ ∃ (u : ℕ → α), StrictAnti u ∧ (∀ (n : ℕ), x < u n) ∧ Tendsto u atTop (𝓝[>] x)

Tactic:
exists_seq_strictMono_tendsto_nhdsWithin (α := αᵒᵈ) _

Premises used: Set.Ioi, exists_seq_strictMono_tendsto_nhdsWithin, setOf, StrictAnti, OrderDual
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : FirstCountableTopology α
x y : α
h : x < y
rcases :
  ∀ (u : ℕ → α) (hu_anti : StrictAnti u) (hu_mem : ∀ (n : ℕ), u n ∈ Ioo x y) (hux : Tendsto u atTop (𝓝 x)),
    ∃ (u : ℕ → α) (v : ℕ → α),
      StrictAnti u ∧
        StrictMono v ∧
          (∀ (k : ℕ), u k ∈ Ioo x y) ∧
            (∀ (l : ℕ), v l ∈ Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y)
⊢ ∃ (u : ℕ → α) (v : ℕ → α),
    StrictAnti u ∧
      StrictMono v ∧
        (∀ (k : ℕ), u k ∈ Ioo x y) ∧
          (∀ (l : ℕ), v l ∈ Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y)

Tactic:
rcases exists_seq_strictAnti_tendsto' h with ⟨u, hu_anti, hu_mem, hux⟩

Premises used: exists_seq_strictAnti_tendsto'
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : FirstCountableTopology α
x y : α
h : x < y
u : ℕ → α
hu_anti : StrictAnti u
hu_mem : ∀ (n : ℕ), u n ∈ Ioo x y
hux : Tendsto u atTop (𝓝 x)
rcases :
  ∀ (v : ℕ → α) (hv_mono : StrictMono v) (hv_mem : ∀ (n : ℕ), v n ∈ Ioo (u 0) y) (hvy : Tendsto v atTop (𝓝 y)),
    ∃ (u : ℕ → α) (v : ℕ → α),
      StrictAnti u ∧
        StrictMono v ∧
          (∀ (k : ℕ), u k ∈ Ioo x y) ∧
            (∀ (l : ℕ), v l ∈ Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y)
⊢ ∃ (u : ℕ → α) (v : ℕ → α),
    StrictAnti u ∧
      StrictMono v ∧
        (∀ (k : ℕ), u k ∈ Ioo x y) ∧
          (∀ (l : ℕ), v l ∈ Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y)

Tactic:
rcases exists_seq_strictMono_tendsto' (hu_mem 0).2 with ⟨v, hv_mono, hv_mem, hvy⟩

Premises used: And.right, OfNat.ofNat, 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 : FirstCountableTopology α
x y : α
h : x < y
u : ℕ → α
hu_anti : StrictAnti u
hu_mem : ∀ (n : ℕ), u n ∈ Ioo x y
hux : Tendsto u atTop (𝓝 x)
v : ℕ → α
hv_mono : StrictMono v
hv_mem : ∀ (n : ℕ), v n ∈ Ioo (u 0) y
hvy : Tendsto v atTop (𝓝 y)
⊢ ∃ (u : ℕ → α) (v : ℕ → α),
    StrictAnti u ∧
      StrictMono v ∧
        (∀ (k : ℕ), u k ∈ Ioo x y) ∧
          (∀ (l : ℕ), v l ∈ Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y)

Tactic:
⟨u, v, hu_anti, hv_mono, hu_mem, fun l => ⟨(hu_mem 0).1.trans (hv_mem l).1, (hv_mem l).2⟩,
      fun k l => (hu_anti.antitone zero_le).trans_lt (hv_mem l).1, hux, hvy⟩

Premises used: zero_le, And.right, And.left, And.intro, Exists.intro, LT.lt.trans, OfNat.ofNat, LE.le.trans_lt, StrictAnti.antitone
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : FirstCountableTopology α
x y : α
h : x < y
u : ℕ → α
hu_anti : StrictAnti u
hu_mem : ∀ (n : ℕ), u n ∈ Ioo x y
hux : Tendsto u atTop (𝓝 x)
v : ℕ → α
hv_mono : StrictMono v
hv_mem : ∀ (n : ℕ), v n ∈ Ioo (u 0) y
hvy : Tendsto v atTop (𝓝 y)
⊢ ∃ (u : ℕ → α) (v : ℕ → α),
    StrictAnti u ∧
      StrictMono v ∧
        (∀ (k : ℕ), u k ∈ Ioo x y) ∧
          (∀ (l : ℕ), v l ∈ Ioo x y) ∧ (∀ (k l : ℕ), u k < v l) ∧ Tendsto u atTop (𝓝 x) ∧ Tendsto v atTop (𝓝 y)

Tactic:
exact
    ⟨u, v, hu_anti, hv_mono, hu_mem, fun l => ⟨(hu_mem 0).1.trans (hv_mem l).1, (hv_mem l).2⟩,
      fun k l => (hu_anti.antitone zero_le).trans_lt (hv_mem l).1, hux, hvy⟩
-- 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' : BddBelow S
⊢ ∃ (u : ℕ → α), Antitone u ∧ Tendsto u atTop (𝓝 (sInf S)) ∧ ∀ (n : ℕ), u n ∈ S

Tactic:
exists_seq_tendsto_sSup (α := αᵒᵈ) hS hS'

Premises used: Set.Mem, exists_seq_tendsto_sSup, Antitone, OrderDual
-- 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 : x < y
⊢ ∃ (u : ℕ → α), StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioo x y ∩ s) ∧ Tendsto u atTop (𝓝 x)

Tactic:
simpa using hs.exists_seq_strictMono_tendsto_of_lt (α := αᵒᵈ) (OrderDual.toDual_lt_toDual.2 hy)

Premises used: Iff.mpr, OrderDual.toDual_lt_toDual, 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 : NoMaxOrder α
inst_5 : FirstCountableTopology α
s : Set α
hs : Dense s
x : α
⊢ ∃ (u : ℕ → α), StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Ioi x ∩ s) ∧ Tendsto u atTop (𝓝 x)

Tactic:
hs.exists_seq_strictMono_tendsto (α := αᵒᵈ) x

Premises used: Set.Ioi, Set.Mem, setOf, StrictAnti, OrderDual, Dense.exists_seq_strictMono_tendsto
-- 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 : x < y
⊢ ∃ (u : ℕ → β), StrictAnti u ∧ (∀ (n : ℕ), f (u n) ∈ Ioo x y) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
simpa using hf.exists_seq_strictMono_tendsto_of_lt (α := αᵒᵈ) (β := βᵒᵈ) hmono.dual
    (OrderDual.toDual_lt_toDual.2 hlt)

Premises used: Iff.mpr, DenseRange.exists_seq_strictMono_tendsto_of_lt, OrderDual.toDual_lt_toDual, Monotone.dual
-- 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 : NoMaxOrder α
inst_6 : FirstCountableTopology α
f : β → α
hf : DenseRange f
hmono : Monotone f
x : α
⊢ ∃ (u : ℕ → β), StrictAnti u ∧ (∀ (n : ℕ), f (u n) ∈ Ioi x) ∧ Tendsto (f ∘ u) atTop (𝓝 x)

Tactic:
hf.exists_seq_strictMono_tendsto (α := αᵒᵈ) (β := βᵒᵈ) hmono.dual x

Premises used: Set.Ioi, Set.Mem, DenseRange.exists_seq_strictMono_tendsto, setOf, Monotone.dual, StrictAnti, OrderDual
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
a : α
h : ∀ (b : α), a < b → ∀ᶠ (x : γ) in l, f x < b
rcases : ∀ (d : α) (hd : IsGLB (Ioi a) d), ∀ᶠ (x : γ) in l, f x ≤ a
⊢ ∀ᶠ (x : γ) in l, f x ≤ a

Tactic:
rcases exists_glb_Ioi a with ⟨d, hd⟩

Premises used: exists_glb_Ioi
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
a : α
h : ∀ (b : α), a < b → ∀ᶠ (x : γ) in l, f x < b
d : α
hd : IsGLB (Ioi a) d
inl : ∀ (h : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b) (hd : IsGLB (Ioi d) d), ∀ᶠ (x : γ) in l, f x ≤ d
inr : ∀ (H0 : Ioi a = Ici d), ∀ᶠ (x : γ) in l, f x ≤ a
⊢ ∀ᶠ (x : γ) in l, f x ≤ a

Tactic:
obtain rfl | H0 := glb_Ioi_eq_self_or_Ioi_eq_Ici _ hd

Premises used: glb_Ioi_eq_self_or_Ioi_eq_Ici, rfl
-- Module: Mathlib.Topology.Order.IsLUB
Goal:
α : Type u_1
γ : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : FirstCountableTopology α
l : Filter γ
inst_4 : CountableInterFilter l
f : γ → α
d : α
h : ∀ (b : α), d < b → ∀ᶠ (x : γ) in l, f x < b
hd : IsGLB (Ioi d) d
inl : ∀ (h : IsTop d), ∀ᶠ (x : γ) in l, f x ≤ d
inl₁ : (∃ (b : α), d < b) → ∀ᶠ (x : γ) in l, f x ≤ d
⊢ ∀ᶠ (x : γ) in l, f x ≤ d

Tactic:
obtain h | _ := isTop_or_exists_gt d

Premises used: isTop_or_exists_gt