awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_4
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ (r : α), ⨅ (_ : r > 1), 𝓟 {b : α | |a / b|ₘ < r}
a : α
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α := ⋯
⊢ ⨅ (r : α), ⨅ (_ : r > 1), 𝓟 {b : α | |a / b|ₘ < r} = 𝓝 a

Tactic:
(nhds_eq_iInf_mabs_div a).symm

Premises used: nhds_eq_iInf_mabs_div, Eq.symm
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_4
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ (r : α), ⨅ (_ : r > 1), 𝓟 {b : α | |a / b|ₘ < r}
a : α
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α := ⋯
⊢ ⨅ (r : α), ⨅ (_ : r > 1), 𝓟 {b : α | |a / b|ₘ < r} = 𝓝 a

Tactic:
exact (nhds_eq_iInf_mabs_div a).symm

Premises used: nhds_eq_iInf_mabs_div, Eq.symm
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
f : β → α
x : Filter β
a : α
⊢ Tendsto f x (𝓝 a) ↔ ∀ ε > 1, ∀ᶠ (b : β) in x, |f b / a|ₘ < ε

Tactic:
simp [nhds_eq_iInf_mabs_div, mabs_div_comm a]

Premises used: mabs_div_comm, nhds_eq_iInf_mabs_div
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
a ε : α
hε : 1 < ε
⊢ Membership.mem (γ := Filter α) (𝓟 {b : α | |a / b|ₘ < ε}) {x : α | (fun (x : α) ↦ |x / a|ₘ < ε) x}

Tactic:
simp only [mabs_div_comm, mem_principal_self]

Premises used: mabs_div_comm, Filter.mem_principal_self
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
h : Nontrivial α
⊢ ∃ (C' : α), C' < C

Tactic:
exists_lt C

Premises used: NoMinOrder.exists_lt
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
h : Nontrivial α
obtain : ∀ (C' : α) (hC' : C' < C), Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atTop

Tactic:
obtain ⟨C', hC'⟩ : ∃ C', C' < C := exists_lt C

Premises used: NoMinOrder.exists_lt
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
h : Nontrivial α
C' : α
hC' : C' < C
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atTop

Tactic:
tendsto_atTop_mul_left_of_le' _ C' ?_ hg

Premises used: Filter.tendsto_atTop_mul_left_of_le'
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
h : Nontrivial α
C' : α
hC' : C' < C
refine : ∀ᶠ (x : β) in l, C' ≤ f x
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atTop

Tactic:
refine tendsto_atTop_mul_left_of_le' _ C' ?_ hg

Premises used: Filter.tendsto_atTop_mul_left_of_le'
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
h : Nontrivial α
C' : α
hC' : C' < C
⊢ ∀ᶠ (x : β) in l, C' ≤ f x

Tactic:
(hf.eventually (lt_mem_nhds hC')).mono fun x => le_of_lt

Premises used: le_of_lt, Filter.Eventually.mono, Filter.Tendsto.eventually, lt_mem_nhds
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
h : Nontrivial α
C' : α
hC' : C' < C
⊢ ∀ᶠ (x : β) in l, C' ≤ f x

Tactic:
exact (hf.eventually (lt_mem_nhds hC')).mono fun x => le_of_lt

Premises used: le_of_lt, Filter.Eventually.mono, Filter.Tendsto.eventually, lt_mem_nhds
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atBot

Tactic:
Filter.Tendsto.mul_atTop' (α := αᵒᵈ) hf hg

Premises used: setOf, Filter.Tendsto.mul_atTop', Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
x : β
rw : g x * f x
| f x * g x

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
conv : Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ g x * f x) l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atTop

Tactic:
conv in _ * _ => rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ g x * f x) l atTop

Tactic:
hg.mul_atTop' hf

Premises used: Filter.Tendsto.mul_atTop'
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ g x * f x) l atTop

Tactic:
exact hg.mul_atTop' hf

Premises used: Filter.Tendsto.mul_atTop'
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
x : β
rw : g x * f x
| f x * g x

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
conv : Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ g x * f x) l atBot
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atBot

Tactic:
conv in _ * _ => rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ g x * f x) l atBot

Tactic:
hg.mul_atBot' hf

Premises used: Filter.Tendsto.mul_atBot'
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ g x * f x) l atBot

Tactic:
exact hg.mul_atBot' hf

Premises used: Filter.Tendsto.mul_atBot'
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
inst_5 : NoMaxOrder α
a : α
simp :
  HasBasis (α := α) (⨅ (r : α), ⨅ (_ : r > 1), 𝓟 {b : α | |b / a|ₘ < r}) (fun (ε : α) ↦ 1 < ε) fun (ε : α) ↦
    {b : α | |b / a|ₘ < ε}
⊢ (𝓝 a).HasBasis (fun (ε : α) ↦ 1 < ε) fun (ε : α) ↦ {b : α | |b / a|ₘ < ε}

Tactic:
simp only [nhds_eq_iInf_mabs_div, mabs_div_comm (a := a)]

Premises used: mabs_div_comm, nhds_eq_iInf_mabs_div
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
inst_5 : NoMaxOrder α
a : α
⊢ HasBasis (α := α) (⨅ (r : α), ⨅ (_ : r > 1), 𝓟 {b : α | |b / a|ₘ < r}) (fun (ε : α) ↦ 1 < ε) fun (ε : α) ↦
    {b : α | |b / a|ₘ < ε}

Tactic:
hasBasis_biInf_principal' (fun x hx y hy => ?_) (exists_gt _)

Premises used: NoMaxOrder.exists_gt, Filter.hasBasis_biInf_principal'
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
inst_5 : NoMaxOrder α
a : α
refine :
  ∀ (x : α) (hx : x > 1) (y : α) (hy : y > 1),
    ∃ k > 1,
      Subset.{u_1} (α := Set α) {b : α | |b / a|ₘ < k} {b : α | |b / a|ₘ < x} ∧
        Subset.{u_1} (α := Set α) {b : α | |b / a|ₘ < k} {b : α | |b / a|ₘ < y}
⊢ HasBasis (α := α) (⨅ (r : α), ⨅ (_ : r > 1), 𝓟 {b : α | |b / a|ₘ < r}) (fun (ε : α) ↦ 1 < ε) fun (ε : α) ↦
    {b : α | |b / a|ₘ < ε}

Tactic:
refine hasBasis_biInf_principal' (fun x hx y hy => ?_) (exists_gt _)

Premises used: NoMaxOrder.exists_gt, Filter.hasBasis_biInf_principal'
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
inst_5 : NoMaxOrder α
a x : α
hx : x > 1
y : α
hy : y > 1
⊢ ∃ k > 1,
    Subset.{u_1} (α := Set α) {b : α | |b / a|ₘ < k} {b : α | |b / a|ₘ < x} ∧
      Subset.{u_1} (α := Set α) {b : α | |b / a|ₘ < k} {b : α | |b / a|ₘ < y}

Tactic:
⟨min x y, lt_min hx hy, fun _ hz => hz.trans_le (min_le_left _ _),
    fun _ hz => hz.trans_le (min_le_right _ _)⟩

Premises used: lt_min, min_le_left, LT.lt.trans_le, And.intro, min_le_right, Exists.intro, Min.min
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
inst_5 : NoMaxOrder α
a x : α
hx : x > 1
y : α
hy : y > 1
⊢ ∃ k > 1,
    Subset.{u_1} (α := Set α) {b : α | |b / a|ₘ < k} {b : α | |b / a|ₘ < x} ∧
      Subset.{u_1} (α := Set α) {b : α | |b / a|ₘ < k} {b : α | |b / a|ₘ < y}

Tactic:
exact ⟨min x y, lt_min hx hy, fun _ hz => hz.trans_le (min_le_left _ _),
    fun _ hz => hz.trans_le (min_le_right _ _)⟩
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
inst_5 : NoMaxOrder α
a : α
⊢ (𝓝 a).HasBasis (fun (ε : α) ↦ 1 < ε) fun (ε : α) ↦ {b : α | |b / a|ₘ < ε}

Tactic:
nhds_basis_mabs_div_lt a

Premises used: nhds_basis_mabs_div_lt
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
inst_5 : NoMaxOrder α
a : α
h : ∀ (x : α), Ioo (a / x) (a * x) = {b : α | |b / a|ₘ < x}
⊢ (𝓝 a).HasBasis (fun (ε : α) ↦ 1 < ε) fun (ε : α) ↦ Ioo (a / ε) (a * ε)

Tactic:
convert! nhds_basis_mabs_div_lt a

Premises used: nhds_basis_mabs_div_lt
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
inst_5 : NoMaxOrder α
a x : α
⊢ Ioo (a / x) (a * x) = {b : α | |b / a|ₘ < x}

Tactic:
simp only [Ioo, mabs_lt, ← div_lt_iff_lt_mul, inv_lt_div_iff_lt_mul, div_lt_comm]

Premises used: div_lt_comm, inv_lt_div_iff_lt_mul, mabs_lt, Set.Ioo, div_lt_iff_lt_mul
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
inst_5 : NoMaxOrder α
inst_6 : DenselyOrdered α
a _ε : α
ε₁ : 1 < _ε
δ : α
δ₁ : 1 < δ
δε : δ < _ε
⊢ a / _ε < a / δ

Tactic:
gcongr
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
inst_5 : NoMaxOrder α
inst_6 : DenselyOrdered α
a _ε : α
ε₁ : 1 < _ε
δ : α
δ₁ : 1 < δ
δε : δ < _ε
⊢ a * δ < a * _ε

Tactic:
gcongr
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
inst_5 : NoMaxOrder α
⊢ HasBasis (α := α) (𝓝 1) (fun (ε : α) ↦ 1 < ε) fun (ε : α) ↦ {b : α | |b|ₘ < ε}

Tactic:
simpa using nhds_basis_mabs_div_lt (1 : α)

Premises used: OfNat.ofNat, nhds_basis_mabs_div_lt
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
inst_5 : NoMaxOrder α
a : α
ha : 1 < a
ε : α
hε : 1 < ε
ha₁ hb : min a ε ≤ ε
⊢ Ioo (a / min a ε) (a * min a ε) ⊆ Ioo (a / ε) (a * ε)

Tactic:
gcongr
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
inst_5 : NoMaxOrder α
a : α
ha : 1 < a
ε : α
hε : 1 < ε
⊢ min a ε ≤ ε

Tactic:
apply min_le_right

Premises used: min_le_right
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIciTopology α
S : Set α
x y : α
hS : S.OrdConnected
hx : x ∈ S
hy : y ∈ S
hxy : x < y
⊢ S ∈ 𝓝[≥] x

Tactic:
mem_of_superset (Icc_mem_nhdsGE hxy) <| hS.out hx hy

Premises used: Icc_mem_nhdsGE, Set.OrdConnected.out, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIciTopology α
S : Set α
x y : α
hS : S.OrdConnected
hx : x ∈ S
hy : y ∈ S
hxy : x < y
⊢ S ∈ 𝓝[>] x

Tactic:
nhdsWithin_mono _ Ioi_subset_Ici_self <| hS.mem_nhdsGE hx hy hxy

Premises used: Set.Ioi_subset_Ici_self, Set.OrdConnected.mem_nhdsGE, nhdsWithin_mono
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
S : Set α
x y : α
hS : S.OrdConnected
hx : x ∈ S
hy : y ∈ S
hxy : x < y
⊢ S ∈ 𝓝[≤] y

Tactic:
hS.dual.mem_nhdsGE hy hx hxy

Premises used: Set.Mem, setOf, Set.OrdConnected.mem_nhdsGE, Set.preimage, Set.OrdConnected.dual, Set.Iic, OrderDual
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
S : Set α
x y : α
hS : S.OrdConnected
hx : x ∈ S
hy : y ∈ S
hxy : x < y
⊢ S ∈ 𝓝[<] y

Tactic:
hS.dual.mem_nhdsGT hy hx hxy

Premises used: Set.Mem, setOf, Set.OrdConnected.mem_nhdsGT, Set.preimage, Set.OrdConnected.dual, OrderDual, Set.Iio
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : BoundedLENhdsClass α
a : α
⊢ IsBounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (𝓝 a)

Tactic:
BoundedLENhdsClass.isBounded_le_nhds _

Premises used: BoundedLENhdsClass.isBounded_le_nhds
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : BoundedLENhdsClass α
f : Filter ι
u : ι → α
a : α
h : Tendsto u f (𝓝 a)
⊢ IsBoundedUnder (fun (x1 x2 : α) ↦ x1 ≤ x2) f u

Tactic:
(isBounded_le_nhds a).mono h

Premises used: Filter.IsBounded.mono, Filter.IsBoundedUnder, isBounded_le_nhds
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : BoundedLENhdsClass α
u : ι → α
a : α
inst_3 : IsDirectedOrder α
h : Tendsto u cofinite (𝓝 a)
⊢ BddAbove (Set.range u)

Tactic:
h.isBoundedUnder_le.bddAbove_range_of_cofinite

Premises used: Filter.Tendsto.isBoundedUnder_le, Filter.IsBoundedUnder.bddAbove_range_of_cofinite
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : BoundedLENhdsClass α
a : α
inst_3 : IsDirectedOrder α
u : ℕ → α
h : Tendsto u atTop (𝓝 a)
⊢ BddAbove (Set.range u)

Tactic:
h.isBoundedUnder_le.bddAbove_range

Premises used: Filter.Tendsto.isBoundedUnder_le, Filter.IsBoundedUnder.bddAbove_range
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
α : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : BoundedLENhdsClass α
a : α
⊢ IsCobounded (fun (x1 x2 : α) ↦ x1 ≥ x2) (𝓝 a)

Tactic:
(isBounded_le_nhds a).isCobounded_flip

Premises used: Filter.IsBounded.isCobounded_flip, isBounded_le_nhds
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : BoundedLENhdsClass α
f : Filter ι
u : ι → α
a : α
inst_3 : f.NeBot
h : Tendsto u f (𝓝 a)
⊢ IsCoboundedUnder (fun (x1 x2 : α) ↦ x1 ≥ x2) f u

Tactic:
h.isBoundedUnder_le.isCobounded_flip

Premises used: Filter.Tendsto.isBoundedUnder_le, Filter.IsCoboundedUnder, Filter.IsBounded.isCobounded_flip
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : BoundedLENhdsClass α
inst_5 : BoundedLENhdsClass β
f : Filter ι
u : ι → α
a : α
⊢ BoundedGENhdsClass.{u_2} αᵒᵈ

Tactic:
⟨@isBounded_le_nhds α _ _ _⟩

Premises used: BoundedGENhdsClass.mk, isBounded_le_nhds
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : BoundedLENhdsClass α
inst_5 : BoundedLENhdsClass β
f : Filter ι
u : ι → α
a : α
⊢ BoundedLENhdsClass (α × β)

Tactic:
⟨fun x ↦ ?_⟩

Premises used: BoundedLENhdsClass.mk
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : BoundedLENhdsClass α
inst_5 : BoundedLENhdsClass β
f : Filter ι
u : ι → α
a : α
refine : ∀ (x : α × β), IsBounded (fun (x1 x2 : α × β) ↦ x1 ≤ x2) (𝓝 x)
⊢ BoundedLENhdsClass (α × β)

Tactic:
refine ⟨fun x ↦ ?_⟩
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : BoundedLENhdsClass α
inst_5 : BoundedLENhdsClass β
f : Filter ι
u : ι → α
a : α
x : α × β
obtain :
  ∀ (a : α) (ha : ∀ᶠ (x : α) in 𝓝 x.1, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a), IsBounded (fun (x1 x2 : α × β) ↦ x1 ≤ x2) (𝓝 x)
⊢ IsBounded (fun (x1 x2 : α × β) ↦ x1 ≤ x2) (𝓝 x)

Tactic:
obtain ⟨a, ha⟩ := isBounded_le_nhds x.1

Premises used: Prod.fst, isBounded_le_nhds
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : BoundedLENhdsClass α
inst_5 : BoundedLENhdsClass β
f : Filter ι
u : ι → α
a_1 : α
x : α × β
a : α
ha : ∀ᶠ (x : α) in 𝓝 x.1, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a
obtain :
  ∀ (b : β) (hb : ∀ᶠ (x : β) in 𝓝 x.2, (fun (x1 x2 : β) ↦ x1 ≤ x2) x b), IsBounded (fun (x1 x2 : α × β) ↦ x1 ≤ x2) (𝓝 x)
⊢ IsBounded (fun (x1 x2 : α × β) ↦ x1 ≤ x2) (𝓝 x)

Tactic:
obtain ⟨b, hb⟩ := isBounded_le_nhds x.2

Premises used: Prod.snd, isBounded_le_nhds
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : BoundedLENhdsClass α
inst_5 : BoundedLENhdsClass β
f : Filter ι
u : ι → α
a_1 : α
x : α × β
a : α
ha : ∀ᶠ (x : α) in 𝓝 x.1, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a
b : β
hb : ∀ᶠ (x : β) in 𝓝 x.2, (fun (x1 x2 : β) ↦ x1 ≤ x2) x b
rw : IsBounded (fun (x1 x2 : α × β) ↦ x1 ≤ x2) (𝓝 x.1 ×ˢ 𝓝 x.2)
⊢ IsBounded (fun (x1 x2 : α × β) ↦ x1 ≤ x2) (𝓝 x)

Tactic:
rw [← @Prod.mk.eta _ _ x, nhds_prod_eq]

Premises used: Prod.mk.eta, nhds_prod_eq
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : BoundedLENhdsClass α
inst_5 : BoundedLENhdsClass β
f : Filter ι
u : ι → α
a_1 : α
x : α × β
a : α
ha : ∀ᶠ (x : α) in 𝓝 x.1, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a
b : β
hb : ∀ᶠ (x : β) in 𝓝 x.2, (fun (x1 x2 : β) ↦ x1 ≤ x2) x b
⊢ IsBounded (fun (x1 x2 : α × β) ↦ x1 ≤ x2) (𝓝 x.1 ×ˢ 𝓝 x.2)

Tactic:
⟨(a, b), ha.prod_mk hb⟩

Premises used: Prod.mk, Filter.IsBounded, Filter.Eventually.prod_mk, Exists.intro
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : BoundedLENhdsClass α
inst_5 : BoundedLENhdsClass β
f : Filter ι
u : ι → α
a_1 : α
x : α × β
a : α
ha : ∀ᶠ (x : α) in 𝓝 x.1, (fun (x1 x2 : α) ↦ x1 ≤ x2) x a
b : β
hb : ∀ᶠ (x : β) in 𝓝 x.2, (fun (x1 x2 : β) ↦ x1 ≤ x2) x b
⊢ IsBounded (fun (x1 x2 : α × β) ↦ x1 ≤ x2) (𝓝 x.1 ×ˢ 𝓝 x.2)

Tactic:
exact ⟨(a, b), ha.prod_mk hb⟩
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : BoundedLENhdsClass α
inst_5 : BoundedLENhdsClass β
f : Filter ι
u : ι → α
a : α
inst_6 : Finite ι
inst_7 : (i : ι) → Preorder (π i)
inst_8 : (i : ι) → TopologicalSpace (π i)
inst_9 : ∀ (i : ι), BoundedLENhdsClass.{u_6} (π i)
⊢ BoundedLENhdsClass ((i : ι) → π i)

Tactic:
⟨fun x ↦ ?_⟩

Premises used: BoundedLENhdsClass.mk
-- Module: Mathlib.Topology.Order.LiminfLimsup
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
R : Type u_4
S : Type u_5
π : ι → Type u_6
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : BoundedLENhdsClass α
inst_5 : BoundedLENhdsClass β
f : Filter ι
u : ι → α
a : α
inst_6 : Finite ι
inst_7 : (i : ι) → Preorder (π i)
inst_8 : (i : ι) → TopologicalSpace (π i)
inst_9 : ∀ (i : ι), BoundedLENhdsClass.{u_6} (π i)
refine : ∀ (x : (i : ι) → π i), IsBounded (fun (x1 x2 : (i : ι) → π i) ↦ x1 ≤ x2) (𝓝 x)
⊢ BoundedLENhdsClass ((i : ι) → π i)

Tactic:
refine ⟨fun x ↦ ?_⟩