awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst : Preorder ι₂
inst_1 : CompleteLattice α
l : Filter ι₁
inst_2 : l.NeBot
f : ι₂ → α
φ : ι₁ → ι₂
hf : Antitone f
hφ : Tendsto φ l atBot
⊢ Eq.{u_5 + 1} (α := α) (⨆ (i : ι₂), f i) (⨆ (i : ι₁), f (φ i))

Tactic:
le_antisymm
    (iSup_mono' fun i =>
      Exists.imp (fun j (hj : φ j ≤ i) => hf hj) (hφ.eventually <| eventually_le_atBot i).exists)
    (iSup_mono' fun i => ⟨φ i, le_rfl⟩)

Premises used: le_rfl, iSup_mono', Exists.imp, Filter.Eventually.exists, le_antisymm, Filter.Tendsto.eventually, Exists.intro, Filter.eventually_le_atBot
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst : Preorder ι₂
inst_1 : CompleteLattice α
l : Filter ι₁
inst_2 : l.NeBot
f : ι₂ → α
φ : ι₁ → ι₂
hf : Monotone f
hφ : Tendsto φ l atBot
⊢ Eq.{u_5 + 1} (α := α) (⨅ (i : ι₂), f i) (⨅ (i : ι₁), f (φ i))

Tactic:
iSup_eq_iSup_subseq_of_monotone hf.dual hφ

Premises used: iInf, iSup_eq_iSup_subseq_of_monotone, Monotone.dual, OrderDual
-- Module: Mathlib.Topology.Order.MonotoneConvergence
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst : Preorder ι₂
inst_1 : CompleteLattice α
l : Filter ι₁
inst_2 : l.NeBot
f : ι₂ → α
φ : ι₁ → ι₂
hf : Antitone f
hφ : Tendsto φ l atTop
⊢ Eq.{u_5 + 1} (α := α) (⨅ (i : ι₂), f i) (⨅ (i : ι₁), f (φ i))

Tactic:
iSup_eq_iSup_subseq_of_antitone hf.dual hφ

Premises used: iInf, iSup_eq_iSup_subseq_of_antitone, Antitone.dual, OrderDual
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a : α
⊢ 𝓝ˢ (Ioi a) = 𝓟 (Ioi a)

Tactic:
isOpen_Ioi.nhdsSet_eq

Premises used: isOpen_Ioi, IsOpen.nhdsSet_eq
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a : α
⊢ 𝓝ˢ (Iio a) = 𝓟 (Iio a)

Tactic:
isOpen_Iio.nhdsSet_eq

Premises used: isOpen_Iio, IsOpen.nhdsSet_eq
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
⊢ 𝓝ˢ (Ioo a b) = 𝓟 (Ioo a b)

Tactic:
isOpen_Ioo.nhdsSet_eq

Premises used: isOpen_Ioo, IsOpen.nhdsSet_eq
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a : α
rw : 𝓝ˢ (insert a (Ioi a)) = 𝓝 a ⊔ 𝓟 (Ioi a)
rw₁ : 𝓝 a ⊔ 𝓝ˢ (Ioi a) = 𝓝 a ⊔ 𝓟 (Ioi a)
rw₂ rw₃ : 𝓝 a ⊔ 𝓟 (Ioi a) = 𝓝 a ⊔ 𝓟 (Ioi a)
⊢ 𝓝ˢ (Ici a) = 𝓝 a ⊔ 𝓟 (Ioi a)

Tactic:
rw [← Ioi_insert, nhdsSet_insert, nhdsSet_Ioi]

Premises used: nhdsSet_insert, Set.Ioi_insert, nhdsSet_Ioi
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a : α
⊢ 𝓝ˢ (Iic a) = 𝓝 a ⊔ 𝓟 (Iio a)

Tactic:
nhdsSet_Ici (α := αᵒᵈ)

Premises used: Set.Mem, setOf, nhdsSet_Ici, Set.Iic, OrderDual, Set.Iio
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
h : a < b
rw : 𝓝ˢ (insert a (Ioo a b)) = 𝓝 a ⊔ 𝓟 (Ioo a b)
rw₁ : 𝓝 a ⊔ 𝓝ˢ (Ioo a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)
rw₂ rw₃ : 𝓝 a ⊔ 𝓟 (Ioo a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)
⊢ 𝓝ˢ (Ico a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)

Tactic:
rw [← Ioo_insert_left h, nhdsSet_insert, nhdsSet_Ioo]

Premises used: nhdsSet_insert, nhdsSet_Ioo, Set.Ioo_insert_left
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
h : a < b
rw : 𝓝ˢ (insert b (Ioo a b)) = 𝓝 b ⊔ 𝓟 (Ioo a b)
rw₁ : 𝓝 b ⊔ 𝓝ˢ (Ioo a b) = 𝓝 b ⊔ 𝓟 (Ioo a b)
rw₂ rw₃ : 𝓝 b ⊔ 𝓟 (Ioo a b) = 𝓝 b ⊔ 𝓟 (Ioo a b)
⊢ 𝓝ˢ (Ioc a b) = 𝓝 b ⊔ 𝓟 (Ioo a b)

Tactic:
rw [← Ioo_insert_right h, nhdsSet_insert, nhdsSet_Ioo]

Premises used: nhdsSet_insert, nhdsSet_Ioo, Set.Ioo_insert_right
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
h : a ≤ b
inl : ∀ (h : a ≤ a), 𝓝ˢ (Icc a a) = 𝓝 a ⊔ 𝓝 a ⊔ 𝓟 (Ioo a a)
inr : ∀ (hlt : a < b), 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)

Tactic:
rcases h.eq_or_lt with rfl | hlt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a : α
h : a ≤ a
⊢ 𝓝ˢ (Icc a a) = 𝓝 a ⊔ 𝓝 a ⊔ 𝓟 (Ioo a a)

Tactic:
simp
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
h : a ≤ b
hlt : a < b
inr : 𝓝ˢ (insert a (Ioc a b)) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
inr₁ : 𝓝 a ⊔ 𝓝ˢ (Ioc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
inr₂ : 𝓝 a ⊔ (𝓝 b ⊔ 𝓟 (Ioo a b)) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
inr₃ inr₄ : 𝓝 a ⊔ (𝓝 b ⊔ 𝓟 (Ioo a b)) = 𝓝 a ⊔ (𝓝 b ⊔ 𝓟 (Ioo a b))
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)

Tactic:
rw [← Ioc_insert_left h, nhdsSet_insert, nhdsSet_Ioc hlt, sup_assoc]

Premises used: nhdsSet_insert, Set.Ioc_insert_left, sup_assoc, nhdsSet_Ioc
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
rw : Ici b ⊆ Ioi a ↔ a < b
rw₁ rw₂ : a < b ↔ a < b
⊢ Ioi a ∈ 𝓝ˢ (Ici b) ↔ a < b

Tactic:
rw [isOpen_Ioi.mem_nhdsSet, Ici_subset_Ioi]

Premises used: isOpen_Ioi, Set.Ici_subset_Ioi, IsOpen.mem_nhdsSet
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
h : a < b
⊢ Ici a ∈ 𝓝ˢ (Ici b)

Tactic:
mem_of_superset (Ioi_mem_nhdsSet_Ici h) Ioi_subset_Ici_self

Premises used: Ioi_mem_nhdsSet_Ici, Set.Ioi_subset_Ici_self, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
⊢ Iio b ∈ 𝓝ˢ (Iic a) ↔ a < b

Tactic:
Ioi_mem_nhdsSet_Ici_iff (α := αᵒᵈ)

Premises used: Set.Mem, setOf, Ioi_mem_nhdsSet_Ici_iff, Set.Iic, OrderDual, Set.Iio
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
h : a < b
⊢ Iic b ∈ 𝓝ˢ (Iic a)

Tactic:
Ici_mem_nhdsSet_Ici (α := αᵒᵈ) h

Premises used: Set.Mem, setOf, Ici_mem_nhdsSet_Ici, Set.Iic, OrderDual
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c : α
h : a < b
⊢ Ioi a ∈ 𝓝ˢ (Icc b c)

Tactic:
nhdsSet_mono Icc_subset_Ici_self <| Ioi_mem_nhdsSet_Ici h

Premises used: nhdsSet_mono, Ioi_mem_nhdsSet_Ici, Set.Icc_subset_Ici_self
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c : α
h : a < b
⊢ Ici a ∈ 𝓝ˢ (Icc b c)

Tactic:
mem_of_superset (Ioi_mem_nhdsSet_Icc h) Ioi_subset_Ici_self

Premises used: Set.Ioi_subset_Ici_self, Ioi_mem_nhdsSet_Icc, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c : α
h : b < c
⊢ Iio c ∈ 𝓝ˢ (Icc a b)

Tactic:
nhdsSet_mono Icc_subset_Iic_self <| Iio_mem_nhdsSet_Iic h

Premises used: nhdsSet_mono, Set.Icc_subset_Iic_self, Iio_mem_nhdsSet_Iic
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c : α
h : b < c
⊢ Iic c ∈ 𝓝ˢ (Icc a b)

Tactic:
mem_of_superset (Iio_mem_nhdsSet_Icc h) Iio_subset_Iic_self

Premises used: Iio_mem_nhdsSet_Icc, Set.Iio_subset_Iic_self, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c d : α
h : a < b
h' : c < d
⊢ Ioo a d ∈ 𝓝ˢ (Icc b c)

Tactic:
inter_mem (Ioi_mem_nhdsSet_Icc h) (Iio_mem_nhdsSet_Icc h')

Premises used: Set.Mem, Filter.inter_mem, setOf, Set.inter, Iio_mem_nhdsSet_Icc, Ioi_mem_nhdsSet_Icc, Set.Ioo
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c d : α
h : a < b
h' : c < d
⊢ Ico a d ∈ 𝓝ˢ (Icc b c)

Tactic:
inter_mem (Ici_mem_nhdsSet_Icc h) (Iio_mem_nhdsSet_Icc h')

Premises used: Set.Mem, Filter.inter_mem, setOf, Set.inter, Iio_mem_nhdsSet_Icc, Set.Ico, Ici_mem_nhdsSet_Icc
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c d : α
h : a < b
h' : c < d
⊢ Ioc a d ∈ 𝓝ˢ (Icc b c)

Tactic:
inter_mem (Ioi_mem_nhdsSet_Icc h) (Iic_mem_nhdsSet_Icc h')

Premises used: Set.Ioc, Set.Mem, Filter.inter_mem, setOf, Iic_mem_nhdsSet_Icc, Set.inter, Ioi_mem_nhdsSet_Icc
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c d : α
h : a < b
h' : c < d
⊢ Icc a d ∈ 𝓝ˢ (Icc b c)

Tactic:
inter_mem (Ici_mem_nhdsSet_Icc h) (Iic_mem_nhdsSet_Icc h')

Premises used: Set.Mem, Filter.inter_mem, setOf, Iic_mem_nhdsSet_Icc, Set.inter, Ici_mem_nhdsSet_Icc, Set.Icc
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c : α
h : a < b
⊢ Ici a ∈ 𝓝ˢ (Ico b c)

Tactic:
nhdsSet_mono Ico_subset_Icc_self <| Ici_mem_nhdsSet_Icc h

Premises used: Set.Ico_subset_Icc_self, nhdsSet_mono, Ici_mem_nhdsSet_Icc
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c : α
h : a < b
⊢ Ioi a ∈ 𝓝ˢ (Ico b c)

Tactic:
nhdsSet_mono Ico_subset_Icc_self <| Ioi_mem_nhdsSet_Icc h

Premises used: Set.Ico_subset_Icc_self, nhdsSet_mono, Ioi_mem_nhdsSet_Icc
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c : α
h : b ≤ c
⊢ Iio c ∈ 𝓝ˢ (Iio b)

Tactic:
simpa
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c : α
h : b ≤ c
⊢ Iic c ∈ 𝓝ˢ (Ico a b)

Tactic:
mem_of_superset (Iio_mem_nhdsSet_Ico h) Iio_subset_Iic_self

Premises used: Iio_mem_nhdsSet_Ico, Set.Iio_subset_Iic_self, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c d : α
h : a < b
h' : c ≤ d
⊢ Ioo a d ∈ 𝓝ˢ (Ico b c)

Tactic:
inter_mem (Ioi_mem_nhdsSet_Ico h) (Iio_mem_nhdsSet_Ico h')

Premises used: Ioi_mem_nhdsSet_Ico, Set.Mem, Filter.inter_mem, setOf, Set.inter, Iio_mem_nhdsSet_Ico, Set.Ioo
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c d : α
h : a < b
h' : c ≤ d
⊢ Icc a d ∈ 𝓝ˢ (Ico b c)

Tactic:
inter_mem (Ici_mem_nhdsSet_Ico h) (Iic_mem_nhdsSet_Ico h')

Premises used: Set.Mem, Filter.inter_mem, setOf, Set.inter, Set.Icc, Ici_mem_nhdsSet_Ico, Iic_mem_nhdsSet_Ico
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c d : α
h : a < b
h' : c ≤ d
⊢ Ioc a d ∈ 𝓝ˢ (Ico b c)

Tactic:
inter_mem (Ioi_mem_nhdsSet_Ico h) (Iic_mem_nhdsSet_Ico h')

Premises used: Set.Ioc, Ioi_mem_nhdsSet_Ico, Set.Mem, Filter.inter_mem, setOf, Set.inter, Iic_mem_nhdsSet_Ico
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c d : α
h : a < b
h' : c ≤ d
⊢ Ico a d ∈ 𝓝ˢ (Ico b c)

Tactic:
inter_mem (Ici_mem_nhdsSet_Ico h) (Iio_mem_nhdsSet_Ico h')

Premises used: Set.Mem, Filter.inter_mem, setOf, Set.inter, Iio_mem_nhdsSet_Ico, Set.Ico, Ici_mem_nhdsSet_Ico
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c : α
h : a ≤ b
⊢ Ioi a ∈ 𝓝ˢ (Ioi b)

Tactic:
simpa
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c : α
h : b < c
⊢ Iio c ∈ 𝓝ˢ (Ioc a b)

Tactic:
nhdsSet_mono Ioc_subset_Icc_self <| Iio_mem_nhdsSet_Icc h

Premises used: nhdsSet_mono, Set.Ioc_subset_Icc_self, Iio_mem_nhdsSet_Icc
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c : α
h : a ≤ b
⊢ Ici a ∈ 𝓝ˢ (Ioc b c)

Tactic:
mem_of_superset (Ioi_mem_nhdsSet_Ioc h) Ioi_subset_Ici_self

Premises used: Ioi_mem_nhdsSet_Ioc, Set.Ioi_subset_Ici_self, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c : α
h : b < c
⊢ Iic c ∈ 𝓝ˢ (Ioc a b)

Tactic:
nhdsSet_mono Ioc_subset_Icc_self <| Iic_mem_nhdsSet_Icc h

Premises used: nhdsSet_mono, Iic_mem_nhdsSet_Icc, Set.Ioc_subset_Icc_self
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c d : α
h : a ≤ b
h' : c < d
⊢ Ioo a d ∈ 𝓝ˢ (Ioc b c)

Tactic:
inter_mem (Ioi_mem_nhdsSet_Ioc h) (Iio_mem_nhdsSet_Ioc h')

Premises used: Ioi_mem_nhdsSet_Ioc, Set.Mem, Filter.inter_mem, setOf, Set.inter, Iio_mem_nhdsSet_Ioc, Set.Ioo
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c d : α
h : a ≤ b
h' : c < d
⊢ Icc a d ∈ 𝓝ˢ (Ioc b c)

Tactic:
inter_mem (Ici_mem_nhdsSet_Ioc h) (Iic_mem_nhdsSet_Ioc h')

Premises used: Set.Mem, Filter.inter_mem, setOf, Set.inter, Set.Icc, Ici_mem_nhdsSet_Ioc, Iic_mem_nhdsSet_Ioc
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c d : α
h : a ≤ b
h' : c < d
⊢ Ioc a d ∈ 𝓝ˢ (Ioc b c)

Tactic:
inter_mem (Ioi_mem_nhdsSet_Ioc h) (Iic_mem_nhdsSet_Ioc h')

Premises used: Set.Ioc, Ioi_mem_nhdsSet_Ioc, Set.Mem, Filter.inter_mem, setOf, Set.inter, Iic_mem_nhdsSet_Ioc
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b c d : α
h : a ≤ b
h' : c < d
⊢ Ico a d ∈ 𝓝ˢ (Ioc b c)

Tactic:
inter_mem (Ici_mem_nhdsSet_Ioc h) (Iio_mem_nhdsSet_Ioc h')

Premises used: Set.Mem, Filter.inter_mem, setOf, Set.inter, Set.Ico, Ici_mem_nhdsSet_Ioc, Iio_mem_nhdsSet_Ioc
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
h : Nonempty.{u_1 + 1} (↑(Ioi a) : Type u_1)
⊢ (𝓝ˢ (Iic a)).HasBasis (fun (x : α) ↦ a < x) Iio

Tactic:
⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨b, hab, hb⟩ ↦ mem_of_superset (Iio_mem_nhdsSet_Iic hab) hb⟩⟩

Premises used: Iio_mem_nhdsSet_Iic, Membership.mem, _private.0.hasBasis_nhdsSet_Iic_Iio.match_1, Filter.HasBasis.mk, Iff.intro, Set.Iic, nhdsSet, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
h : Nonempty.{u_1 + 1} (↑(Ioi a) : Type u_1)
refine : ∀ (s : Set α) (hs : s ∈ 𝓝ˢ (Iic a)), ∃ (i : α), a < i ∧ Iio i ⊆ s
⊢ (𝓝ˢ (Iic a)).HasBasis (fun (x : α) ↦ a < x) Iio

Tactic:
refine ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨b, hab, hb⟩ ↦ mem_of_superset (Iio_mem_nhdsSet_Iic hab) hb⟩⟩
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
h : Nonempty.{u_1 + 1} (↑(Ioi a) : Type u_1)
s : Set α
hs : s ∈ 𝓝ˢ (Iic a)
⊢ s ∈ 𝓝 a ∧ Iio a ⊆ s

Tactic:
rw [nhdsSet_Iic, mem_sup, mem_principal] at hs

Premises used: nhdsSet_Iic, Filter.mem_principal, Filter.mem_sup
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
h : Nonempty.{u_1 + 1} (↑(Ioi a) : Type u_1)
s : Set α
hs : s ∈ 𝓝 a ∧ Iio a ⊆ s
rcases : ∀ (b : α) (hab : a < b) (hbs : Ico a b ⊆ s), ∃ (i : α), a < i ∧ Iio i ⊆ s
⊢ ∃ (i : α), a < i ∧ Iio i ⊆ s

Tactic:
rcases exists_Ico_subset_of_mem_nhds hs.1 (Set.nonempty_coe_sort.1 h) with ⟨b, hab, hbs⟩

Premises used: Set.nonempty_coe_sort, And.left, exists_Ico_subset_of_mem_nhds, Iff.mp
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
h : Nonempty.{u_1 + 1} (↑(Ioi a) : Type u_1)
s : Set α
hs : s ∈ 𝓝 a ∧ Iio a ⊆ s
b : α
hab : a < b
hbs : Ico a b ⊆ s
⊢ ∃ (i : α), a < i ∧ Iio i ⊆ s

Tactic:
⟨b, hab, Iio_subset_Iio_union_Ico.trans (union_subset hs.2 hbs)⟩

Premises used: HasSubset.Subset.trans, Set.union_subset, And.right, And.intro, Exists.intro, Set.Iio_subset_Iio_union_Ico
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
h : Nonempty.{u_1 + 1} (↑(Ioi a) : Type u_1)
s : Set α
hs : s ∈ 𝓝 a ∧ Iio a ⊆ s
b : α
hab : a < b
hbs : Ico a b ⊆ s
⊢ ∃ (i : α), a < i ∧ Iio i ⊆ s

Tactic:
exact ⟨b, hab, Iio_subset_Iio_union_Ico.trans (union_subset hs.2 hbs)⟩
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : (𝓝[>] a).NeBot
⊢ Nonempty.{u_1 + 1} (↑(Ioi a) : Type u_1)

Tactic:
have : Nonempty (Ioi a) :=
    (Filter.nonempty_of_mem (self_mem_nhdsWithin : Ioi a ∈ 𝓝[>] a)).to_subtype
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : (𝓝[>] a).NeBot
this : Nonempty.{u_1 + 1} (↑(Ioi a) : Type u_1)
⊢ (𝓝ˢ (Iic a)).HasBasis (fun (x : α) ↦ a < x) Iic

Tactic:
(hasBasis_nhdsSet_Iic_Iio _).to_hasBasis
    (fun c hc ↦ ?_) (fun _ h ↦ ⟨_, h, Iio_subset_Iic_self⟩)

Premises used: hasBasis_nhdsSet_Iic_Iio, And.intro, Exists.intro, Set.Iio_subset_Iic_self, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : (𝓝[>] a).NeBot
this : Nonempty.{u_1 + 1} (↑(Ioi a) : Type u_1)
refine : ∀ (c : α) (hc : a < c), ∃ (i' : α), a < i' ∧ Iic i' ⊆ Iio c
⊢ (𝓝ˢ (Iic a)).HasBasis (fun (x : α) ↦ a < x) Iic

Tactic:
refine (hasBasis_nhdsSet_Iic_Iio _).to_hasBasis
    (fun c hc ↦ ?_) (fun _ h ↦ ⟨_, h, Iio_subset_Iic_self⟩)

Premises used: hasBasis_nhdsSet_Iic_Iio, And.intro, Exists.intro, Set.Iio_subset_Iic_self, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : (𝓝[>] a).NeBot
this : Nonempty.{u_1 + 1} (↑(Ioi a) : Type u_1)
c : α
hc : a < c
⊢ ∃ (i' : α), a < i' ∧ Iic i' ⊆ Iio c

Tactic:
simpa only [Iic_subset_Iio] using Filter.nonempty_of_mem (Ioo_mem_nhdsGT hc)

Premises used: Set.Iic_subset_Iio, Filter.nonempty_of_mem, Ioo_mem_nhdsGT
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
inst_3 : (𝓝[>] b).NeBot
⊢ Iic a ∈ 𝓝ˢ (Iic b) ↔ b < a

Tactic:
(hasBasis_nhdsSet_Iic_Iic b).mem_iff.trans
    ⟨fun ⟨_c, hbc, hca⟩ ↦ hbc.trans_le (Iic_subset_Iic.1 hca), fun h ↦ ⟨_, h, Subset.rfl⟩⟩

Premises used: Filter.HasBasis.mem_iff, Set.Iic_subset_Iic, hasBasis_nhdsSet_Iic_Iic, Set.Subset.rfl, LT.lt.trans_le, And.intro, LT.lt, _private.0.Iic_mem_nhdsSet_Iic_iff.match_1, Iff.intro, Exists.intro, Iff.mp, Iff.trans
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : Nonempty.{u_1 + 1} (↑(Iio a) : Type u_1)
⊢ (𝓝ˢ (Ici a)).HasBasis (fun (x : α) ↦ x < a) Ioi

Tactic:
have : Nonempty (Ioi (toDual a)) := ‹_›; hasBasis_nhdsSet_Iic_Iio (toDual a)

Premises used: OrderDual.toDual, Set.Ioi, Set.Ici, setOf, hasBasis_nhdsSet_Iic_Iio, OrderDual, DFunLike.coe
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : (𝓝[<] a).NeBot
⊢ (𝓝ˢ (Ici a)).HasBasis (fun (x : α) ↦ x < a) Ici

Tactic:
have : NeBot (𝓝[>] (toDual a)) := ‹_›; hasBasis_nhdsSet_Iic_Iic (toDual a)

Premises used: OrderDual.toDual, Set.Ici, setOf, hasBasis_nhdsSet_Iic_Iic, OrderDual, DFunLike.coe
-- Module: Mathlib.Topology.Order.NhdsSet
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a b : α
inst_3 : (𝓝[<] b).NeBot
⊢ Ici a ∈ 𝓝ˢ (Ici b) ↔ a < b

Tactic:
have : NeBot (𝓝[>] (toDual b)) := ‹_›; Iic_mem_nhdsSet_Iic_iff (a := toDual a) (b := toDual b)

Premises used: Set.Ici, Set.Mem, setOf, Iic_mem_nhdsSet_Iic_iff, OrderDual
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
h : FirstCountableTopology α
⊢ FirstCountableTopology.{u} αᵒᵈ

Tactic:
h

Premises used: OrderDual
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
h : SecondCountableTopology α
⊢ SecondCountableTopology.{u} αᵒᵈ

Tactic:
h

Premises used: OrderDual
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
h : SeparableSpace α
⊢ SeparableSpace.{u} αᵒᵈ

Tactic:
h

Premises used: OrderDual
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
s : Set α
hs : Dense s
⊢ Dense (X := αᵒᵈ) ((⇑OrderDual.ofDual : (a : αᵒᵈ) → α) ⁻¹' s)

Tactic:
hs

Premises used: Set.Mem, setOf, Set.preimage, OrderDual
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
s : Set α
⊢ BddAbove (closure[inst] s) → BddAbove s

Tactic:
BddAbove.mono subset_closure

Premises used: subset_closure, BddAbove.mono
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
a : α
⊢ IsClosed[inst] (Iic a)

Tactic:
ClosedIicTopology.isClosed_Iic a

Premises used: ClosedIicTopology.isClosed_Iic
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
a : α
⊢ closure[inst] (Iic a) = Iic a

Tactic:
isClosed_Iic.closure_eq

Premises used: IsClosed.closure_eq, isClosed_Iic
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
f : β → α
a b : α
x : Filter β
lim : Tendsto f x (𝓝 a)
h : ∃ᶠ (c : β) in x, f c ≤ b
⊢ a ≤ b

Tactic:
isClosed_Iic.mem_of_frequently_of_tendsto h lim

Premises used: Set.Mem, setOf, IsClosed.mem_of_frequently_of_tendsto, isClosed_Iic, Set.Iic
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
f : β → α
a b : α
x : Filter β
inst_3 : x.NeBot
lim : Tendsto f x (𝓝 a)
h : ∀ᶠ (c : β) in x, f c ≤ b
⊢ a ≤ b

Tactic:
isClosed_Iic.mem_of_tendsto lim h

Premises used: Set.Mem, setOf, IsClosed.mem_of_tendsto, isClosed_Iic, Set.Iic
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
f : β → α
a b : α
x : Filter β
inst_3 : x.NeBot
lim : Tendsto f x (𝓝 a)
h : ∀ (c : β), f c ≤ b
⊢ a ≤ b

Tactic:
le_of_tendsto lim (Eventually.of_forall h)

Premises used: Filter.Eventually.of_forall, le_of_tendsto
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
s : Set α
a : α
simp_rw : closure[inst] s ⊆ Iic a ↔ s ⊆ Iic a
⊢ a ∈ upperBounds (closure[inst] s) ↔ a ∈ upperBounds s

Tactic:
simp_rw [mem_upperBounds_iff_subset_Iic, isClosed_Iic.closure_subset_iff]

Premises used: mem_upperBounds_iff_subset_Iic, isClosed_Iic, IsClosed.closure_subset_iff
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
a : α
mp : Disjoint (𝓝 a) atBot → ¬IsBot a
mpr : ¬IsBot a → Disjoint (𝓝 a) atBot
⊢ Disjoint (𝓝 a) atBot ↔ ¬IsBot a

Tactic:
constructor