awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
a : α
hd : Disjoint (𝓝 a) atBot
hbot : IsBot a
⊢ (Iic a)ᶜ ∈ 𝓝 a

Tactic:
rw [hbot.atBot_eq, disjoint_principal_right] at hd

Premises used: IsBot.atBot_eq, Filter.disjoint_principal_right
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
a : α
hd : Disjoint (𝓝 a) atBot
hbot : IsBot a
hd₁ : (Iic a)ᶜ ∈ 𝓝 a
⊢ IsBot a

Tactic:
rw [hbot.atBot_eq, disjoint_principal_right] at hd

Premises used: IsBot.atBot_eq, Filter.disjoint_principal_right
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
a : α
hd : (Iic a)ᶜ ∈ 𝓝 a
hbot : IsBot a
⊢ False

Tactic:
mem_of_mem_nhds hd le_rfl

Premises used: le_rfl, mem_of_mem_nhds
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
a : α
hd : (Iic a)ᶜ ∈ 𝓝 a
hbot : IsBot a
⊢ False

Tactic:
exact mem_of_mem_nhds hd le_rfl

Premises used: le_rfl, mem_of_mem_nhds
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
a : α
mpr : (∃ (x : α), ¬a ≤ x) → Disjoint (𝓝 a) atBot
⊢ ¬IsBot a → Disjoint (𝓝 a) atBot

Tactic:
simp only [IsBot, not_forall]

Premises used: IsBot, Classical.not_forall
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
a b : α
hb : ¬a ≤ b
⊢ Disjoint (𝓝 a) atBot

Tactic:
disjoint_of_disjoint_of_mem disjoint_compl_left ?_ (Iic_mem_atBot b)

Premises used: disjoint_compl_left, Filter.disjoint_of_disjoint_of_mem, Filter.Iic_mem_atBot
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
a b : α
hb : ¬a ≤ b
mpr : (Iic b)ᶜ ∈ 𝓝 a
⊢ Disjoint (𝓝 a) atBot

Tactic:
refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ (Iic_mem_atBot b)

Premises used: disjoint_compl_left, Filter.disjoint_of_disjoint_of_mem, Filter.Iic_mem_atBot
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
a b : α
hb : ¬a ≤ b
⊢ (Iic b)ᶜ ∈ 𝓝 a

Tactic:
isClosed_Iic.isOpen_compl.mem_nhds hb

Premises used: IsClosed.isOpen_compl, Set.Mem, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
a b : α
hb : ¬a ≤ b
⊢ (Iic b)ᶜ ∈ 𝓝 a

Tactic:
exact isClosed_Iic.isOpen_compl.mem_nhds hb

Premises used: IsClosed.isOpen_compl, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
f : β → α
a : α
F : Filter β
inst_3 : F.NeBot
hle : ∀ (i : β), f i ≤ a
hlim : Tendsto f F (𝓝 a)
⊢ IsLUB (range f) a

Tactic:
⟨forall_mem_range.mpr hle, fun _c hc ↦ le_of_tendsto' hlim fun i ↦ hc <| mem_range_self i⟩

Premises used: Set.mem_range_self, Iff.mpr, Set.forall_mem_range, IsLeast, And.intro, IsLUB, le_of_tendsto'
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : Preorder α
inst_1 : NoBotOrder α
inst_2 : TopologicalSpace α
inst_3 : ClosedIicTopology α
a : α
⊢ Disjoint (𝓝 a) atBot

Tactic:
simp
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : Preorder α
inst_1 : NoBotOrder α
inst_2 : TopologicalSpace α
inst_3 : ClosedIicTopology α
a : α
⊢ 𝓝 a ⊓ atBot = ⊥

Tactic:
(disjoint_nhds_atBot a).eq_bot

Premises used: Disjoint.eq_bot, disjoint_nhds_atBot
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : NoBotOrder α
inst_2 : TopologicalSpace α
inst_3 : ClosedIicTopology α
l : Filter β
inst_4 : l.NeBot
f : β → α
hf : Tendsto f l atBot
a : α
⊢ ¬Tendsto f l (𝓝 a)

Tactic:
hf.not_tendsto (disjoint_nhds_atBot a).symm

Premises used: Filter.Tendsto.not_tendsto, Disjoint.symm, disjoint_nhds_atBot
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : NoBotOrder α
inst_2 : TopologicalSpace α
inst_3 : ClosedIicTopology α
a : α
l : Filter β
inst_4 : l.NeBot
f : β → α
hf : Tendsto f l (𝓝 a)
⊢ ¬Tendsto f l atBot

Tactic:
hf.not_tendsto (disjoint_nhds_atBot a)

Premises used: Filter.Tendsto.not_tendsto, disjoint_nhds_atBot
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
ι : Type u_1
F : Filter ι
inst : F.NeBot
inst_1 : ConditionallyCompleteLattice α
inst_2 : TopologicalSpace α
inst_3 : ClosedIicTopology α
a : α
f : ι → α
hle : ∀ (i : ι), f i ≤ a
hlim : Tendsto f F (𝓝 a)
⊢ ⨆ (i : ι), f i = a

Tactic:
have := F.nonempty_of_neBot
  (IsLUB.range_of_tendsto hle hlim).ciSup_eq

Premises used: IsLUB.range_of_tendsto, Filter.nonempty_of_neBot, IsLUB.ciSup_eq
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
ι : Type u_1
F : Filter ι
inst : F.NeBot
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : TopologicalSpace α
inst_3 : ClosedIicTopology α
f : ι → α
i : ι
hlt : ∀ (i_1 : ι), f i_1 < f i
hlim : Tendsto f F (𝓝 (f i))
⊢ False

Tactic:
(hlt i).false

Premises used: LT.lt.false
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
ι : Type u_1
F : Filter ι
inst : F.NeBot
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : TopologicalSpace α
inst_3 : ClosedIicTopology α
f : ι → α
i : ι
hlt : ∀ (i_1 : ι), f i_1 < f i
hlim : Tendsto f F (𝓝 (f i))
⊢ False

Tactic:
exact (hlt i).false

Premises used: LT.lt.false
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
ι : Type u_1
F : Filter ι
inst : F.NeBot
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : TopologicalSpace α
inst_3 : ClosedIicTopology α
a : α
f : ι → α
hlt : ∀ (i : ι), f i < a
hlim : Tendsto f F (𝓝 a)
⊢ a ∉ range f

Tactic:
have obs : a ∉ range f := by
    rw [mem_range]
    rintro ⟨i, rfl⟩
    exact (hlt i).false
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
ι : Type u_1
F : Filter ι
inst : F.NeBot
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : TopologicalSpace α
inst_3 : ClosedIicTopology α
a : α
f : ι → α
hlt : ∀ (i : ι), f i < a
hlim : Tendsto f F (𝓝 a)
obs : a ∉ range f
rw : ⋃ x ∈ range f, Iic x = Iio a
rw₁ rw₂ : Iio a = Iio a
⊢ ⋃ (i : ι), Iic (f i) = Iio a

Tactic:
rw [← biUnion_range, (IsLUB.range_of_tendsto (le_of_lt <| hlt ·) hlim).biUnion_Iic_eq_Iio obs]

Premises used: IsLUB.range_of_tendsto, le_of_lt, Set.biUnion_range, IsLUB.biUnion_Iic_eq_Iio
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a : α
rw : IsOpen[inst] (Iic a)ᶜ
⊢ IsOpen[inst] (Ioi a)

Tactic:
rw [← compl_Iic]

Premises used: Set.compl_Iic
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a : α
⊢ IsOpen[inst] (Iic a)ᶜ

Tactic:
isClosed_Iic.isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a : α
⊢ IsOpen[inst] (Iic a)ᶜ

Tactic:
exact isClosed_Iic.isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a : α
⊢ interior (Ioi a) = Ioi a

Tactic:
isOpen_Ioi.interior_eq

Premises used: isOpen_Ioi, IsOpen.interior_eq
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
h : a < b
⊢ Ioi a ∈ 𝓝 b

Tactic:
IsOpen.mem_nhds isOpen_Ioi h

Premises used: isOpen_Ioi, IsOpen.mem_nhds
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
hab : b < a
⊢ ∀ᶠ (x : α) in 𝓝 a, b < x

Tactic:
Ioi_mem_nhds hab

Premises used: Ioi_mem_nhds, Set.Ioi, Set.Mem, Filter.Eventually, setOf
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
h : a < b
⊢ Ici a ∈ 𝓝 b

Tactic:
mem_of_superset (Ioi_mem_nhds h) Ioi_subset_Ici_self

Premises used: Ioi_mem_nhds, Set.Ioi_subset_Ici_self, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
hab : b < a
⊢ ∀ᶠ (x : α) in 𝓝 a, b ≤ x

Tactic:
Ici_mem_nhds hab

Premises used: Set.Ici, Set.Mem, Filter.Eventually, setOf, Ici_mem_nhds
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
l : Filter γ
f : γ → α
u v : α
hv : u < v
h : Tendsto f l (𝓝 v)
⊢ ∀ᶠ (a : γ) in l, u < f a

Tactic:
h.eventually <| eventually_gt_nhds hv

Premises used: eventually_gt_nhds, Filter.Tendsto.eventually
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
l : Filter γ
f : γ → α
u v : α
hv : u < v
h : Tendsto f l (𝓝 v)
⊢ ∀ᶠ (a : γ) in l, u ≤ f a

Tactic:
h.eventually <| eventually_ge_nhds hv

Premises used: eventually_ge_nhds, Filter.Tendsto.eventually
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
inst_3 : NoMaxOrder α
s : Set α
hs : Dense s
x : α
⊢ ∃ y ∈ s, x < y

Tactic:
hs.exists_mem_open isOpen_Ioi (exists_gt x)

Premises used: Set.Mem, NoMaxOrder.exists_gt, isOpen_Ioi, Dense.exists_mem_open
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
inst_3 : NoMaxOrder α
s : Set α
hs : Dense s
x : α
⊢ ∃ y ∈ s, x ≤ y

Tactic:
(hs.exists_gt x).imp fun _ h ↦ ⟨h.1, h.2.le⟩

Premises used: Exists.imp, And.intro, Dense.exists_gt
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
pos : ∀ (hx : IsTop x), ∃ y ∈ s, x ≤ y
neg : ∀ (hx : ¬IsTop x), ∃ y ∈ s, x ≤ y
⊢ ∃ y ∈ s, x ≤ y

Tactic:
by_cases hx : IsTop x

Premises used: IsTop
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : IsTop x
⊢ ∃ y ∈ s, x ≤ y

Tactic:
⟨x, htop x hx, le_rfl⟩

Premises used: le_rfl, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : IsTop x
⊢ ∃ y ∈ s, x ≤ y

Tactic:
exact ⟨x, htop x hx, le_rfl⟩
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : ¬IsTop x
⊢ ∃ (x_1 : α), x < x_1

Tactic:
simp only [IsTop, not_forall, not_le] at hx

Premises used: not_le, IsTop, Classical.not_forall
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : ∃ (x_1 : α), x < x_1
neg : ∀ (y : α) (hys : y ∈ s) (hy : x < y), ∃ y ∈ s, x ≤ y
⊢ ∃ y ∈ s, x ≤ y

Tactic:
rcases hs.exists_mem_open isOpen_Ioi hx with ⟨y, hys, hy : x < y⟩

Premises used: isOpen_Ioi, Dense.exists_mem_open
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : ∃ (x_1 : α), x < x_1
y : α
hys : y ∈ s
hy : x < y
⊢ ∃ y ∈ s, x ≤ y

Tactic:
⟨y, hys, hy.le⟩

Premises used: LT.lt.le, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : ∃ (x_1 : α), x < x_1
y : α
hys : y ∈ s
hy : x < y
⊢ ∃ y ∈ s, x ≤ y

Tactic:
exact ⟨y, hys, hy.le⟩
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
H : a < b
⊢ Ioo a b ∈ 𝓝[<] b

Tactic:
simpa only [← Iio_inter_Ioi] using inter_mem_nhdsWithin _ (Ioi_mem_nhds H)

Premises used: Ioi_mem_nhds, inter_mem_nhdsWithin, Set.Iio_inter_Ioi
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b c : α
H : b ∈ Ioc a c
⊢ Ioo a c ∈ 𝓝[<] b

Tactic:
mem_of_superset (Ioo_mem_nhdsLT H.1) <| Ioo_subset_Ioo_right H.2

Premises used: Set.Ioo_subset_Ioo_right, Ioo_mem_nhdsLT, And.right, And.left, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
h : a ⋖ b
⊢ 𝓝[<] b = ⊥

Tactic:
empty_mem_iff_bot.mp <| h.Ioo_eq ▸ Ioo_mem_nhdsLT h.1

Premises used: Eq.rec, Ioo_mem_nhdsLT, And.left, Filter.empty_mem_iff_bot, Iff.mp, CovBy.Ioo_eq
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a : α
inst_3 : PredOrder α
h : IsMin a
⊢ 𝓝[<] a = ⊥

Tactic:
simp [h.Iio_eq]

Premises used: IsMin.Iio_eq
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a : α
inst_3 : PredOrder α
h : ¬IsMin a
⊢ 𝓝[<] a = ⊥

Tactic:
(Order.pred_covBy_of_not_isMin h).nhdsLT

Premises used: Order.pred_covBy_of_not_isMin, CovBy.nhdsLT
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a : α
inst_3 : PredOrder α
h : ¬IsMin a
⊢ 𝓝[<] a = ⊥

Tactic:
exact (Order.pred_covBy_of_not_isMin h).nhdsLT

Premises used: Order.pred_covBy_of_not_isMin, CovBy.nhdsLT
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a : α
inst_3 : PredOrder α
if : ∀ (h : IsMin a), 𝓝[<] a = ⊥
if₁ : ∀ (h : ¬IsMin a), 𝓝[<] a = ⊥
if₂ : ∀ (h : IsMin a), 𝓝[<] a = ⊥
if₃ if₄ : ∀ (h : ¬IsMin a), 𝓝[<] a = ⊥
⊢ 𝓝[<] a = ⊥

Tactic:
if h : IsMin a then simp [h.Iio_eq]
  else exact (Order.pred_covBy_of_not_isMin h).nhdsLT

Premises used: IsMin
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
inst_3 : PredOrder α
a : α
rw : 𝓝[>] a = 𝓝[<] a ⊔ 𝓝[>] a
rw₁ : 𝓝[>] a = ⊥ ⊔ 𝓝[>] a
rw₂ rw₃ : 𝓝[>] a = 𝓝[>] a
⊢ 𝓝[>] a = 𝓝[≠] a

Tactic:
rw [← nhdsLT_sup_nhdsGT, PredOrder.nhdsLT, bot_sup_eq]

Premises used: bot_sup_eq, PredOrder.nhdsLT, nhdsLT_sup_nhdsGT
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
inst_3 : PredOrder α
a : α
rw : 𝓝[≥] a = 𝓝[<] a ⊔ 𝓝[≥] a
rw₁ : 𝓝[≥] a = ⊥ ⊔ 𝓝[≥] a
rw₂ rw₃ : 𝓝[≥] a = 𝓝[≥] a
⊢ 𝓝[≥] a = 𝓝 a

Tactic:
rw [← nhdsLT_sup_nhdsGE, PredOrder.nhdsLT, bot_sup_eq]

Premises used: bot_sup_eq, nhdsLT_sup_nhdsGE, PredOrder.nhdsLT
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b c : α
H : b ∈ Ioc a c
⊢ Ico a c ∈ 𝓝[<] b

Tactic:
mem_of_superset (Ioo_mem_nhdsLT_of_mem H) Ioo_subset_Ico_self

Premises used: Ioo_mem_nhdsLT_of_mem, Set.Ioo_subset_Ico_self, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
H : a < b
⊢ Ico a b ∈ 𝓝[<] b

Tactic:
Ico_mem_nhdsLT_of_mem ⟨H, le_rfl⟩

Premises used: le_rfl, Ico_mem_nhdsLT_of_mem, And.intro
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b c : α
H : b ∈ Ioc a c
⊢ Ioc a c ∈ 𝓝[<] b

Tactic:
mem_of_superset (Ioo_mem_nhdsLT_of_mem H) Ioo_subset_Ioc_self

Premises used: Ioo_mem_nhdsLT_of_mem, Set.Ioo_subset_Ioc_self, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
H : a < b
⊢ Ioc a b ∈ 𝓝[<] b

Tactic:
Ioc_mem_nhdsLT_of_mem ⟨H, le_rfl⟩

Premises used: le_rfl, Ioc_mem_nhdsLT_of_mem, And.intro
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b c : α
H : b ∈ Ioc a c
⊢ Icc a c ∈ 𝓝[<] b

Tactic:
mem_of_superset (Ioo_mem_nhdsLT_of_mem H) Ioo_subset_Icc_self

Premises used: Set.Ioo_subset_Icc_self, Ioo_mem_nhdsLT_of_mem, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
H : a < b
⊢ Icc a b ∈ 𝓝[<] b

Tactic:
Icc_mem_nhdsLT_of_mem ⟨H, le_rfl⟩

Premises used: le_rfl, And.intro, Icc_mem_nhdsLT_of_mem
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
h : a < b
⊢ 𝓝[Ico a b] b = 𝓝[<] b

Tactic:
nhdsWithin_inter_of_mem <| nhdsWithin_le_nhds <| Ici_mem_nhds h

Premises used: Set.Mem, setOf, Set.inter, nhdsWithin_inter_of_mem, Set.Ico, nhdsWithin_le_nhds, Ici_mem_nhds, Set.Iio
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
h : a < b
⊢ 𝓝[Ioo a b] b = 𝓝[<] b

Tactic:
nhdsWithin_inter_of_mem <| nhdsWithin_le_nhds <| Ioi_mem_nhds h

Premises used: Ioi_mem_nhds, Set.Mem, setOf, Set.inter, nhdsWithin_inter_of_mem, nhdsWithin_le_nhds, Set.Iio, Set.Ioo
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
inst_3 : TopologicalSpace β
a b : α
f : α → β
h : a < b
⊢ ContinuousWithinAt f (Ico a b) b ↔ ContinuousWithinAt f (Iio b) b

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_Ico_eq_nhdsLT h]

Premises used: ContinuousWithinAt, nhdsWithin_Ico_eq_nhdsLT
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
inst_3 : TopologicalSpace β
a b : α
f : α → β
h : a < b
⊢ ContinuousWithinAt f (Ioo a b) b ↔ ContinuousWithinAt f (Iio b) b

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_Ioo_eq_nhdsLT h]

Premises used: nhdsWithin_Ioo_eq_nhdsLT, ContinuousWithinAt
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
H : a ⋖ b
rw : 𝓝[insert b (Iio b)] b = pure b
rw₁ : pure b ⊔ 𝓝[<] b = pure b
rw₂ : Eq (α := Filter α) (pure b ⊔ ⊥) (pure b)
rw₃ rw₄ : Eq (α := Filter α) (pure b) (pure b)
⊢ 𝓝[≤] b = pure b

Tactic:
rw [← Iio_insert, nhdsWithin_insert, H.nhdsLT, sup_bot_eq]

Premises used: nhdsWithin_insert, sup_bot_eq, CovBy.nhdsLT, Set.Iio_insert
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
b : α
inst_3 : PredOrder α
rw : 𝓝[insert b (Iio b)] b = pure b
rw₁ : pure b ⊔ 𝓝[<] b = pure b
rw₂ : Eq (α := Filter α) (pure b ⊔ ⊥) (pure b)
rw₃ rw₄ : Eq (α := Filter α) (pure b) (pure b)
⊢ 𝓝[≤] b = pure b

Tactic:
rw [← Iio_insert, nhdsWithin_insert, PredOrder.nhdsLT, sup_bot_eq]

Premises used: nhdsWithin_insert, sup_bot_eq, PredOrder.nhdsLT, Set.Iio_insert
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
H : a < b
⊢ Ioc a b ∈ 𝓝[≤] b

Tactic:
inter_mem (nhdsWithin_le_nhds <| Ioi_mem_nhds H) self_mem_nhdsWithin

Premises used: Set.Ioc, Ioi_mem_nhds, Set.Mem, Filter.inter_mem, setOf, Set.inter, nhdsWithin_le_nhds, self_mem_nhdsWithin
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b c : α
H : b ∈ Ioo a c
⊢ Ioo a c ∈ 𝓝[≤] b

Tactic:
mem_of_superset (Ioc_mem_nhdsLE H.1) <| Ioc_subset_Ioo_right H.2

Premises used: Ioc_mem_nhdsLE, And.right, Set.Ioc_subset_Ioo_right, And.left, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b c : α
H : b ∈ Ioo a c
⊢ Ico a c ∈ 𝓝[≤] b

Tactic:
mem_of_superset (Ioo_mem_nhdsLE_of_mem H) Ioo_subset_Ico_self

Premises used: Ioo_mem_nhdsLE_of_mem, Set.Ioo_subset_Ico_self, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b c : α
H : b ∈ Ioc a c
⊢ Ioc a c ∈ 𝓝[≤] b

Tactic:
mem_of_superset (Ioc_mem_nhdsLE H.1) <| Ioc_subset_Ioc_right H.2

Premises used: Ioc_mem_nhdsLE, Set.Ioc_subset_Ioc_right, And.right, And.left, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b c : α
H : b ∈ Ioc a c
⊢ Icc a c ∈ 𝓝[≤] b

Tactic:
mem_of_superset (Ioc_mem_nhdsLE_of_mem H) Ioc_subset_Icc_self

Premises used: Set.Ioc_subset_Icc_self, Ioc_mem_nhdsLE_of_mem, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
H : a < b
⊢ Icc a b ∈ 𝓝[≤] b

Tactic:
Icc_mem_nhdsLE_of_mem ⟨H, le_rfl⟩

Premises used: le_rfl, And.intro, Icc_mem_nhdsLE_of_mem
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
h : a < b
⊢ 𝓝[Icc a b] b = 𝓝[≤] b

Tactic:
nhdsWithin_inter_of_mem <| nhdsWithin_le_nhds <| Ici_mem_nhds h

Premises used: Set.Mem, setOf, Set.inter, nhdsWithin_inter_of_mem, nhdsWithin_le_nhds, Set.Icc, Ici_mem_nhds, Set.Iic
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a b : α
h : a < b
⊢ 𝓝[Ioc a b] b = 𝓝[≤] b

Tactic:
nhdsWithin_inter_of_mem <| nhdsWithin_le_nhds <| Ioi_mem_nhds h

Premises used: Set.Ioc, Ioi_mem_nhds, Set.Mem, setOf, Set.inter, nhdsWithin_inter_of_mem, nhdsWithin_le_nhds, Set.Iic
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
inst_3 : TopologicalSpace β
a b : α
f : α → β
h : a < b
⊢ ContinuousWithinAt f (Icc a b) b ↔ ContinuousWithinAt f (Iic b) b

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_Icc_eq_nhdsLE h]

Premises used: ContinuousWithinAt, nhdsWithin_Icc_eq_nhdsLE
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
inst_3 : TopologicalSpace β
a b : α
f : α → β
h : a < b
⊢ ContinuousWithinAt f (Ioc a b) b ↔ ContinuousWithinAt f (Iic b) b

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_Ioc_eq_nhdsLE h]

Premises used: ContinuousWithinAt, nhdsWithin_Ioc_eq_nhdsLE
-- Module: Mathlib.Topology.Order.OrderClosed
Goal:
α : Type u
ι : Type u_1
F : Filter ι
inst : F.NeBot
inst_1 : ConditionallyCompleteLattice α
inst_2 : TopologicalSpace α
inst_3 : ClosedIciTopology α
a : α
f : ι → α
hle : ∀ (i : ι), a ≤ f i
hlim : Tendsto f F (𝓝 a)
⊢ ⨅ (i : ι), f i = a

Tactic:
iSup_eq_of_forall_le_of_tendsto (α := αᵒᵈ) hle hlim

Premises used: iInf, iSup_eq_of_forall_le_of_tendsto, OrderDual