awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
l : β
hl : l < sSup (f '' Iio x)
⊢ ∃ a < x, l < f a

Tactic:
simpa only [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_lt_csSup (h.image _) hl

Premises used: Set.mem_image, exists_prop, exists_lt_of_lt_csSup, exists_exists_and_eq_and, Set.Nonempty.image
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
l : β
hl : l < sSup (f '' Iio x)
inr : ∀ (z : α) (zx : z < x) (lz : l < f z), ∀ᶠ (b : α) in 𝓝[<] x, l < f b
⊢ ∀ᶠ (b : α) in 𝓝[<] x, l < f b

Tactic:
obtain ⟨z, zx, lz⟩ : ∃ a : α, a < x ∧ l < f a := by
      simpa only [mem_image, exists_prop, exists_exists_and_eq_and] using
        exists_lt_of_lt_csSup (h.image _) hl
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
l : β
hl : l < sSup (f '' Iio x)
z : α
zx : z < x
lz : l < f z
y : α
hy : y ∈ Ioo z x
⊢ l < f y

Tactic:
lz.trans_le (Mf zx hy.2 hy.1.le)

Premises used: LT.lt.le, And.right, And.left, LT.lt.trans_le
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
l : β
hl : l < sSup (f '' Iio x)
z : α
zx : z < x
lz : l < f z
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x_1 : α | x_1 ∈ Ioo z x → Membership.mem (γ := Set α) {x : α | (fun (b : α) ↦ l < f b) x} x_1} a
h₂ h₃ : ∀ (y : α) (hy : y ∈ Ioo z x), l < f y
⊢ ∀ᶠ (b : α) in 𝓝[<] x, l < f b

Tactic:
filter_upwards [Ioo_mem_nhdsLT zx] with y hy using lz.trans_le (Mf zx hy.2 hy.1.le)

Premises used: Ioo_mem_nhdsLT
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
m : β
hm : m > sSup (f '' Iio x)
⊢ ∀ᶠ (b : α) in 𝓝[<] x, f b < m

Tactic:
mem_of_superset self_mem_nhdsWithin fun y hy => lt_of_le_of_lt ?_ hm

Premises used: lt_of_le_of_lt, Filter.Eventually, self_mem_nhdsWithin, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
m : β
hm : m > sSup (f '' Iio x)
inr : ∀ (y : α) (hy : y ∈ Iio x), f y ≤ sSup (f '' Iio x)
⊢ ∀ᶠ (b : α) in 𝓝[<] x, f b < m

Tactic:
refine mem_of_superset self_mem_nhdsWithin fun y hy => lt_of_le_of_lt ?_ hm

Premises used: lt_of_le_of_lt, self_mem_nhdsWithin, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
m : β
hm : m > sSup (f '' Iio x)
y : α
hy : y ∈ Iio x
⊢ f y ≤ sSup (f '' Iio x)

Tactic:
le_csSup h_bdd (mem_image_of_mem _ hy)

Premises used: Set.mem_image_of_mem, le_csSup
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
m : β
hm : m > sSup (f '' Iio x)
y : α
hy : y ∈ Iio x
⊢ f y ≤ sSup (f '' Iio x)

Tactic:
exact le_csSup h_bdd (mem_image_of_mem _ hy)

Premises used: Set.mem_image_of_mem, le_csSup
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Ioi x)
h_bdd : BddBelow (f '' Ioi x)
⊢ Tendsto f (𝓝[>] x) (𝓝 (sInf (f '' Ioi x)))

Tactic:
MonotoneOn.tendsto_nhdsLT (α := αᵒᵈ) (β := βᵒᵈ) Mf.dual h_bdd

Premises used: Set.Ioi, MonotoneOn.tendsto_nhdsLT, setOf, MonotoneOn.dual, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
Mf : Monotone f
x : α
⊢ Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))

Tactic:
MonotoneOn.tendsto_nhdsLT (Mf.monotoneOn _) (Mf.map_bddAbove bddAbove_Iio)

Premises used: MonotoneOn.tendsto_nhdsLT, bddAbove_Iio, Monotone.map_bddAbove, Monotone.monotoneOn
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
Mf : Monotone f
x : α
⊢ Tendsto f (𝓝[>] x) (𝓝 (sInf (f '' Ioi x)))

Tactic:
Monotone.tendsto_nhdsLT (α := αᵒᵈ) (β := βᵒᵈ) Mf.dual x

Premises used: Set.Ioi, setOf, Monotone.tendsto_nhdsLT, Monotone.dual, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo y x).Nonempty
Af : AntitoneOn f (Ioo y x)
h_bdd : BddBelow (f '' Ioo y x)
⊢ Tendsto f (𝓝[<] x) (𝓝 (sInf (f '' Ioo y x)))

Tactic:
MonotoneOn.tendsto_nhdsWithin_Ioo_left h_nonempty Af.dual_right h_bdd

Premises used: AntitoneOn.dual_right, MonotoneOn.tendsto_nhdsWithin_Ioo_left, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x y : α
h_nonempty : (Ioo x y).Nonempty
Af : AntitoneOn f (Ioo x y)
h_bdd : BddAbove (f '' Ioo x y)
⊢ Tendsto f (𝓝[>] x) (𝓝 (sSup (f '' Ioo x y)))

Tactic:
MonotoneOn.tendsto_nhdsWithin_Ioo_right h_nonempty Af.dual_right h_bdd

Premises used: AntitoneOn.dual_right, MonotoneOn.tendsto_nhdsWithin_Ioo_right, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Af : AntitoneOn f (Iio x)
h_bdd : BddBelow (f '' Iio x)
⊢ Tendsto f (𝓝[<] x) (𝓝 (sInf (f '' Iio x)))

Tactic:
MonotoneOn.tendsto_nhdsLT Af.dual_right h_bdd

Premises used: MonotoneOn.tendsto_nhdsLT, AntitoneOn.dual_right, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
x : α
Af : AntitoneOn f (Ioi x)
h_bdd : BddAbove (f '' Ioi x)
⊢ Tendsto f (𝓝[>] x) (𝓝 (sSup (f '' Ioi x)))

Tactic:
MonotoneOn.tendsto_nhdsGT Af.dual_right h_bdd

Premises used: MonotoneOn.tendsto_nhdsGT, AntitoneOn.dual_right, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
Af : Antitone f
x : α
⊢ Tendsto f (𝓝[<] x) (𝓝 (sInf (f '' Iio x)))

Tactic:
Monotone.tendsto_nhdsLT Af.dual_right x

Premises used: Antitone.dual_right, Monotone.tendsto_nhdsLT, OrderDual
-- Module: Mathlib.Topology.Order.Monotone
Goal:
α : Type u_3
β : Type u_4
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : ConditionallyCompleteLinearOrder β
inst_4 : TopologicalSpace β
inst_5 : OrderTopology β
f : α → β
Af : Antitone f
x : α
⊢ Tendsto f (𝓝[>] x) (𝓝 (sSup (f '' Ioi x)))

Tactic:
Monotone.tendsto_nhdsGT Af.dual_right x

Premises used: Antitone.dual_right, OrderDual, Monotone.tendsto_nhdsGT
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : InfConvergenceClass α
⊢ SupConvergenceClass.{u_1} αᵒᵈ

Tactic:
⟨‹InfConvergenceClass α›.1⟩

Premises used: SupConvergenceClass.mk, InfConvergenceClass.tendsto_coe_atBot_isGLB
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : SupConvergenceClass α
⊢ InfConvergenceClass.{u_1} αᵒᵈ

Tactic:
⟨‹SupConvergenceClass α›.1⟩

Premises used: SupConvergenceClass.tendsto_coe_atTop_isLUB, InfConvergenceClass.mk
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
⊢ SupConvergenceClass α

Tactic:
⟨fun a s ha => tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩⟩

Premises used: Iff.mpr, SupConvergenceClass.mk, tendsto_order, And.intro
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
refine_1 :
  ∀ (a : α) (s : Set α) (ha : IsLUB s a) (b : α) (hb : b < a), ∀ᶠ (b_1 : { x : α // x ∈ s }) in atTop, b < (↑b_1 : α)
refine_2 :
  ∀ (a : α) (s : Set α) (ha : IsLUB s a) (b : α) (hb : b > a), ∀ᶠ (b_1 : { x : α // x ∈ s }) in atTop, (↑b_1 : α) < b
⊢ SupConvergenceClass α

Tactic:
refine ⟨fun a s ha => tendsto_order.2 ⟨fun b hb => ?_, fun b hb => ?_⟩⟩
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
refine_1 : ∀ (c : α) (hcs : c ∈ s) (bc : b < c) (bca : c ≤ a), ∀ᶠ (b_1 : { x : α // x ∈ s }) in atTop, b < (↑b_1 : α)
⊢ ∀ᶠ (b_1 : { x : α // x ∈ s }) in atTop, b < (↑b_1 : α)

Tactic:
rcases ha.exists_between hb with ⟨c, hcs, bc, bca⟩

Premises used: IsLUB.exists_between
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
c : α
hcs : c ∈ s
bc : b < c
bca : c ≤ a
⊢ c ∈ s

Tactic:
hcs
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
c : α
hcs : c ∈ s
bc : b < c
bca : c ≤ a
refine_1 :
  ∀ (c : { x : α // x ∈ s }) (bc : b < (↑c : α)) (bca : (↑c : α) ≤ a),
    ∀ᶠ (b_1 : { x : α // x ∈ s }) in atTop, b < (↑b_1 : α)
⊢ ∀ᶠ (b_1 : { x : α // x ∈ s }) in atTop, b < (↑b_1 : α)

Tactic:
lift c to s using hcs
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
c : { x : α // x ∈ s }
bc : b < (↑c : α)
bca : (↑c : α) ≤ a
⊢ ∀ᶠ (b_1 : { x : α // x ∈ s }) in atTop, b < (↑b_1 : α)

Tactic:
(eventually_ge_atTop c).mono fun x hx => bc.trans_le hx

Premises used: Filter.Eventually.mono, LT.lt.trans_le, Filter.eventually_ge_atTop
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
c : { x : α // x ∈ s }
bc : b < (↑c : α)
bca : (↑c : α) ≤ a
⊢ ∀ᶠ (b_1 : { x : α // x ∈ s }) in atTop, b < (↑b_1 : α)

Tactic:
exact (eventually_ge_atTop c).mono fun x hx => bc.trans_le hx

Premises used: Filter.Eventually.mono, LT.lt.trans_le, Filter.eventually_ge_atTop
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b > a
⊢ ∀ᶠ (b_1 : { x : α // x ∈ s }) in atTop, (↑b_1 : α) < b

Tactic:
Eventually.of_forall fun x => (ha.1 x.2).trans_lt hb

Premises used: Filter.Eventually.of_forall, And.left, LE.le.trans_lt, Subtype.property
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b > a
⊢ ∀ᶠ (b_1 : { x : α // x ∈ s }) in atTop, (↑b_1 : α) < b

Tactic:
exact Eventually.of_forall fun x => (ha.1 x.2).trans_lt hb

Premises used: Filter.Eventually.of_forall, And.left, LE.le.trans_lt
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
⊢ InfConvergenceClass α

Tactic:
show InfConvergenceClass αᵒᵈᵒᵈ from OrderDual.infConvergenceClass

Premises used: OrderDual.infConvergenceClass, OrderDual
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : Preorder α
inst_3 : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
suffices : Tendsto (rangeFactorization f) atTop atTop
⊢ Tendsto f atTop (𝓝 a)

Tactic:
suffices Tendsto (rangeFactorization f) atTop atTop from
    (SupConvergenceClass.tendsto_coe_atTop_isLUB _ _ ha).comp this
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : Preorder α
inst_3 : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto (rangeFactorization f) atTop atTop

Tactic:
h_mono.rangeFactorization.tendsto_atTop_atTop fun b => b.2.imp fun a ha => ha.ge

Premises used: Exists.imp, Monotone.tendsto_atTop_atTop, Monotone.rangeFactorization, Subtype.property
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : Preorder α
inst_3 : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto (rangeFactorization f) atTop atTop

Tactic:
exact h_mono.rangeFactorization.tendsto_atTop_atTop fun b => b.2.imp fun a ha => ha.ge

Premises used: Exists.imp, Monotone.tendsto_atTop_atTop, Monotone.rangeFactorization, Subtype.property
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : Preorder α
inst_3 : SupConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
ha : IsLUB (range f) a
⊢ Tendsto (α := ιᵒᵈ) (f ∘ (⇑OrderDual.ofDual : (a : ιᵒᵈ) → ι)) atTop (𝓝 a)

Tactic:
tendsto_atTop_isLUB h_anti.dual_left ha

Premises used: Antitone.dual_left, tendsto_atTop_isLUB
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : Preorder α
inst_3 : SupConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
ha : IsLUB (range f) a
⊢ Tendsto f atBot (𝓝 a)

Tactic:
convert! tendsto_atTop_isLUB h_anti.dual_left ha using 1

Premises used: Antitone.dual_left, tendsto_atTop_isLUB
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : Preorder α
inst_3 : InfConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsGLB (range f) a
⊢ Tendsto (α := ιᵒᵈ) (β := αᵒᵈ)
    ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f ∘ (⇑OrderDual.ofDual : (a : ιᵒᵈ) → ι) : ιᵒᵈ → αᵒᵈ) atTop
    (𝓝 ((OrderDual.toDual : (a : α) → αᵒᵈ) a) : Filter αᵒᵈ)

Tactic:
tendsto_atTop_isLUB h_mono.dual ha.dual

Premises used: IsGLB.dual, Monotone.dual, tendsto_atTop_isLUB
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : Preorder α
inst_3 : InfConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsGLB (range f) a
⊢ Tendsto f atBot (𝓝 a)

Tactic:
convert! tendsto_atTop_isLUB h_mono.dual ha.dual using 1

Premises used: IsGLB.dual, Monotone.dual, tendsto_atTop_isLUB
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : Preorder α
inst_3 : InfConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
ha : IsGLB (range f) a
⊢ Tendsto (α := ιᵒᵈ) (β := αᵒᵈ)
    ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f ∘ (⇑OrderDual.ofDual : (a : ιᵒᵈ) → ι) : ιᵒᵈ → αᵒᵈ) atBot
    (𝓝 ((OrderDual.toDual : (a : α) → αᵒᵈ) a) : Filter αᵒᵈ)

Tactic:
tendsto_atBot_isLUB h_anti.dual ha.dual

Premises used: tendsto_atBot_isLUB, IsGLB.dual, Antitone.dual
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : Preorder α
inst_3 : InfConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
ha : IsGLB (range f) a
⊢ Tendsto f atTop (𝓝 a)

Tactic:
convert! tendsto_atBot_isLUB h_anti.dual ha.dual using 1

Premises used: tendsto_atBot_isLUB, IsGLB.dual, Antitone.dual
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompletePartialOrderSup α
inst_3 : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
inl : ∀ (h : Eq.{u_3 + 1} (α := Filter ι) atTop ⊥), Tendsto f atTop (𝓝 (⨆ (i : ι), f i))
inr : ∀ (h : Ne.{u_3 + 1} (α := Filter ι) atTop ⊥), Tendsto f atTop (𝓝 (⨆ (i : ι), f i))
⊢ Tendsto f atTop (𝓝 (⨆ (i : ι), f i))

Tactic:
obtain (h | h) := eq_or_ne atTop (⊥ : Filter ι)

Premises used: Bot.bot, Filter.atTop, eq_or_ne
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompletePartialOrderSup α
inst_3 : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h : Eq.{u_3 + 1} (α := Filter ι) atTop ⊥
⊢ Tendsto f atTop (𝓝 (⨆ (i : ι), f i))

Tactic:
simp [h]
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompletePartialOrderSup α
inst_3 : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h : Ne.{u_3 + 1} (α := Filter ι) atTop ⊥
⊢ Nonempty ι

Tactic:
obtain ⟨h₁, h₂⟩ := Filter.atTop_neBot_iff.mp ⟨h⟩

Premises used: Filter.NeBot.mk, Iff.mp, Filter.atTop_neBot_iff
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompletePartialOrderSup α
inst_3 : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h : Ne.{u_3 + 1} (α := Filter ι) atTop ⊥
h₁ : Nonempty ι
⊢ IsDirectedOrder ι

Tactic:
obtain ⟨h₁, h₂⟩ := Filter.atTop_neBot_iff.mp ⟨h⟩

Premises used: Filter.NeBot.mk, Iff.mp, Filter.atTop_neBot_iff
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompletePartialOrderSup α
inst_3 : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h : Ne.{u_3 + 1} (α := Filter ι) atTop ⊥
h₁ : Nonempty ι
h₂ : IsDirectedOrder ι
⊢ Tendsto f atTop (𝓝 (⨆ (i : ι), f i))

Tactic:
tendsto_atTop_isLUB h_mono <|
      h_mono.directed_le.directedOn_range.isLUB_csSup (Set.range_nonempty f) hbdd

Premises used: Directed.directedOn_range, Set.range_nonempty, Monotone.directed_le, tendsto_atTop_isLUB, DirectedOn.isLUB_csSup
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompletePartialOrderSup α
inst_3 : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h : Ne.{u_3 + 1} (α := Filter ι) atTop ⊥
h₁ : Nonempty ι
h₂ : IsDirectedOrder ι
⊢ Tendsto f atTop (𝓝 (⨆ (i : ι), f i))

Tactic:
exact tendsto_atTop_isLUB h_mono <|
      h_mono.directed_le.directedOn_range.isLUB_csSup (Set.range_nonempty f) hbdd

Premises used: Directed.directedOn_range, Set.range_nonempty, Monotone.directed_le, tendsto_atTop_isLUB, DirectedOn.isLUB_csSup
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompletePartialOrderSup α
inst_3 : SupConvergenceClass α
f : ι → α
h_anti : Antitone f
hbdd : BddAbove (range f)
⊢ Tendsto (α := ιᵒᵈ) (β := α) ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f ∘ (⇑OrderDual.ofDual : (a : ιᵒᵈ) → ι)) atTop
    (𝓝 (⨆ (i : ιᵒᵈ), ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f ∘ (⇑OrderDual.ofDual : (a : ιᵒᵈ) → ι)) i))

Tactic:
tendsto_atTop_ciSup h_anti.dual hbdd.dual

Premises used: tendsto_atTop_ciSup, Antitone.dual, BddAbove.dual
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompletePartialOrderSup α
inst_3 : SupConvergenceClass α
f : ι → α
h_anti : Antitone f
hbdd : BddAbove (range f)
⊢ Tendsto f atBot (𝓝 (⨆ (i : ι), f i))

Tactic:
convert! tendsto_atTop_ciSup h_anti.dual hbdd.dual using 1

Premises used: tendsto_atTop_ciSup, Antitone.dual, BddAbove.dual
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompletePartialOrderInf α
inst_3 : InfConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddBelow (range f)
⊢ Tendsto (α := ιᵒᵈ) (β := αᵒᵈ) ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f ∘ (⇑OrderDual.ofDual : (a : ιᵒᵈ) → ι)) atTop
    (𝓝 (⨆ (i : ιᵒᵈ), ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f ∘ (⇑OrderDual.ofDual : (a : ιᵒᵈ) → ι)) i))

Tactic:
tendsto_atTop_ciSup h_mono.dual hbdd.dual

Premises used: tendsto_atTop_ciSup, BddBelow.dual, Monotone.dual
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompletePartialOrderInf α
inst_3 : InfConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddBelow (range f)
⊢ Tendsto f atBot (𝓝 (⨅ (i : ι), f i))

Tactic:
convert! tendsto_atTop_ciSup h_mono.dual hbdd.dual using 1

Premises used: tendsto_atTop_ciSup, BddBelow.dual, Monotone.dual
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompletePartialOrderInf α
inst_3 : InfConvergenceClass α
f : ι → α
h_anti : Antitone f
hbdd : BddBelow (range f)
⊢ Tendsto (α := ιᵒᵈ) (β := αᵒᵈ) ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f ∘ (⇑OrderDual.ofDual : (a : ιᵒᵈ) → ι)) atBot
    (𝓝 (⨆ (i : ιᵒᵈ), ((⇑OrderDual.toDual : (a : α) → αᵒᵈ) ∘ f ∘ (⇑OrderDual.ofDual : (a : ιᵒᵈ) → ι)) i))

Tactic:
tendsto_atBot_ciSup h_anti.dual hbdd.dual

Premises used: tendsto_atBot_ciSup, Antitone.dual, BddBelow.dual