awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
ha : (Ioi a).Nonempty
⊢ interior (Iic a) = Iio a

Tactic:
interior_Ici' (α := αᵒᵈ) ha

Premises used: setOf, Set.Iic, OrderDual, Set.Iio, interior_Ici'
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMaxOrder α
a : α
⊢ interior (Iic a) = Iio a

Tactic:
interior_Iic' nonempty_Ioi

Premises used: interior_Iic', Set.nonempty_Ioi
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
a b : α
rw : interior (Ici a ∩ Iic b) = Ioo a b
rw₁ : interior (Ici a) ∩ interior (Iic b) = Ioo a b
rw₂ : Ioi a ∩ interior (Iic b) = Ioo a b
rw₃ : Ioi a ∩ Iio b = Ioo a b
rw₄ rw₅ : Ioo a b = Ioo a b
⊢ interior (Icc a b) = Ioo a b

Tactic:
rw [← Ici_inter_Iic, interior_inter, interior_Ici, interior_Iic, Ioi_inter_Iio]

Premises used: interior_Ici, interior_inter, Set.Ioi_inter_Iio, interior_Iic, Set.Ici_inter_Iic
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
a b x : α
rw : Icc a b ∈ 𝓝 x ↔ x ∈ interior (Icc a b)
rw₁ rw₂ : Icc a b ∈ 𝓝 x ↔ Icc a b ∈ 𝓝 x
⊢ Icc a b ∈ 𝓝 x ↔ x ∈ Ioo a b

Tactic:
rw [← interior_Icc, mem_interior_iff_mem_nhds]

Premises used: mem_interior_iff_mem_nhds, interior_Icc
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
a b : α
rw : interior (Ici a ∩ Iio b) = Ioo a b
rw₁ : interior (Ici a) ∩ interior (Iio b) = Ioo a b
rw₂ : Ioi a ∩ interior (Iio b) = Ioo a b
rw₃ : Ioi a ∩ Iio b = Ioo a b
rw₄ rw₅ : Ioo a b = Ioo a b
⊢ interior (Ico a b) = Ioo a b

Tactic:
rw [← Ici_inter_Iio, interior_inter, interior_Ici, interior_Iio, Ioi_inter_Iio]

Premises used: interior_Ici, Set.Ici_inter_Iio, interior_inter, interior_Iio, Set.Ioi_inter_Iio
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
a b x : α
rw : Ico a b ∈ 𝓝 x ↔ x ∈ interior (Ico a b)
rw₁ rw₂ : Ico a b ∈ 𝓝 x ↔ Ico a b ∈ 𝓝 x
⊢ Ico a b ∈ 𝓝 x ↔ x ∈ Ioo a b

Tactic:
rw [← interior_Ico, mem_interior_iff_mem_nhds]

Premises used: mem_interior_iff_mem_nhds, interior_Ico
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMaxOrder α
a b : α
rw : interior (Ioi a ∩ Iic b) = Ioo a b
rw₁ : interior (Ioi a) ∩ interior (Iic b) = Ioo a b
rw₂ : Ioi a ∩ interior (Iic b) = Ioo a b
rw₃ : Ioi a ∩ Iio b = Ioo a b
rw₄ rw₅ : Ioo a b = Ioo a b
⊢ interior (Ioc a b) = Ioo a b

Tactic:
rw [← Ioi_inter_Iic, interior_inter, interior_Ioi, interior_Iic, Ioi_inter_Iio]

Premises used: Set.Ioi_inter_Iic, interior_inter, Set.Ioi_inter_Iio, interior_Iic, interior_Ioi
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMaxOrder α
a b x : α
rw : Ioc a b ∈ 𝓝 x ↔ x ∈ interior (Ioc a b)
rw₁ rw₂ : Ioc a b ∈ 𝓝 x ↔ Ioc a b ∈ 𝓝 x
⊢ Ioc a b ∈ 𝓝 x ↔ x ∈ Ioo a b

Tactic:
rw [← interior_Ioc, mem_interior_iff_mem_nhds]

Premises used: mem_interior_iff_mem_nhds, interior_Ioc
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : a ≠ b
⊢ closure[inst] (interior (Icc a b)) = Icc a b

Tactic:
(closure_minimal interior_subset isClosed_Icc).antisymm <|
    calc
      Icc a b = closure (Ioo a b) := (closure_Ioo h).symm
      _ ⊆ closure (interior (Icc a b)) :=
        closure_mono (interior_maximal Ioo_subset_Icc_self isOpen_Ioo)

Premises used: Set.Ioo_subset_Icc_self, Trans.trans, interior_subset, closure_minimal, isOpen_Ioo, interior_maximal, closure_mono, isClosed_Icc, HasSubset.Subset.antisymm, Eq.symm, closure_Ioo
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
inl : Ioc a a ⊆ closure[inst] (interior (Ioc a a))
inr : ∀ (h : a ≠ b), Ioc a b ⊆ closure[inst] (interior (Ioc a b))
⊢ Ioc a b ⊆ closure[inst] (interior (Ioc a b))

Tactic:
rcases eq_or_ne a b with (rfl | h)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
⊢ Ioc a a ⊆ closure[inst] (interior (Ioc a a))

Tactic:
simp
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : a ≠ b
⊢ Ioc a b ⊆ Icc a b

Tactic:
Ioc_subset_Icc_self

Premises used: Set.Ioc_subset_Icc_self
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : a ≠ b
⊢ Icc a b = closure[inst] (Ioo a b)

Tactic:
(closure_Ioo h).symm

Premises used: Eq.symm, closure_Ioo
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : a ≠ b
⊢ closure[inst] (Ioo a b) ⊆ closure[inst] (interior (Ioc a b))

Tactic:
closure_mono (interior_maximal Ioo_subset_Ioc_self isOpen_Ioo)

Premises used: isOpen_Ioo, interior_maximal, closure_mono, Set.Ioo_subset_Ioc_self
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : a ≠ b
⊢ Ioc a b ⊆ closure[inst] (interior (Ioc a b))

Tactic:
calc
      Ioc a b ⊆ Icc a b := Ioc_subset_Icc_self
      _ = closure (Ioo a b) := (closure_Ioo h).symm
      _ ⊆ closure (interior (Ioc a b)) :=
        closure_mono (interior_maximal Ioo_subset_Ioc_self isOpen_Ioo)

Premises used: Set.Ioc, isOpen_Ioo, Set.Ioc_subset_Icc_self, interior_maximal, closure_mono, Set.Icc, closure, Set.Ioo_subset_Ioc_self, interior, Eq.symm, Set.Ioo, closure_Ioo
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
⊢ Ico a b ⊆ closure[inst] (interior (Ico a b))

Tactic:
simpa only [Ioc_toDual] using
    Ioc_subset_closure_interior (OrderDual.toDual b) (OrderDual.toDual a)

Premises used: OrderDual.toDual, Ioc_subset_closure_interior, Set.Ioc_toDual, DFunLike.coe
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
ha : (Iio a).Nonempty
⊢ frontier (Ici a) = {a}

Tactic:
simp [frontier, ha]

Premises used: frontier
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
a : α
⊢ frontier (Ici a) = {a}

Tactic:
frontier_Ici' nonempty_Iio

Premises used: frontier_Ici', Set.nonempty_Iio
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
ha : (Ioi a).Nonempty
⊢ frontier (Iic a) = {a}

Tactic:
simp [frontier, ha]

Premises used: frontier
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMaxOrder α
a : α
⊢ frontier (Iic a) = {a}

Tactic:
frontier_Iic' nonempty_Ioi

Premises used: frontier_Iic', Set.nonempty_Ioi
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
ha : (Ioi a).Nonempty
⊢ frontier (Ioi a) = {a}

Tactic:
simp [frontier, closure_Ioi' ha]

Premises used: frontier, closure_Ioi'
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMaxOrder α
a : α
⊢ frontier (Ioi a) = {a}

Tactic:
frontier_Ioi' nonempty_Ioi

Premises used: Set.nonempty_Ioi, frontier_Ioi'
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
ha : (Iio a).Nonempty
⊢ frontier (Iio a) = {a}

Tactic:
simp [frontier, closure_Iio' ha]

Premises used: frontier, closure_Iio'
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
a : α
⊢ frontier (Iio a) = {a}

Tactic:
frontier_Iio' nonempty_Iio

Premises used: frontier_Iio', Set.nonempty_Iio
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
a b : α
h : a ≤ b
⊢ frontier (Icc a b) = {a, b}

Tactic:
simp [frontier, h, Icc_diff_Ioo_same]

Premises used: frontier, Set.Icc_diff_Ioo_same
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : a < b
rw : closure[inst] (Ioo a b) \ interior (Ioo a b) = {a, b}
rw₁ : Icc a b \ interior (Ioo a b) = {a, b}
rw₂ : Icc a b \ Ioo a b = {a, b}
rw₃ rw₄ : Eq (α := Set α) {a, b} {a, b}
⊢ frontier (Ioo a b) = {a, b}

Tactic:
rw [frontier, closure_Ioo h.ne, interior_Ioo, Icc_diff_Ioo_same h.le]

Premises used: frontier, LT.lt.le, Set.Icc_diff_Ioo_same, interior_Ioo, LT.lt.ne, closure_Ioo
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
a b : α
h : a < b
rw : closure[inst] (Ico a b) \ interior (Ico a b) = {a, b}
rw₁ : Icc a b \ interior (Ico a b) = {a, b}
rw₂ : Icc a b \ Ioo a b = {a, b}
rw₃ rw₄ : Eq (α := Set α) {a, b} {a, b}
⊢ frontier (Ico a b) = {a, b}

Tactic:
rw [frontier, closure_Ico h.ne, interior_Ico, Icc_diff_Ioo_same h.le]

Premises used: frontier, LT.lt.le, Set.Icc_diff_Ioo_same, closure_Ico, interior_Ico, LT.lt.ne
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMaxOrder α
a b : α
h : a < b
rw : closure[inst] (Ioc a b) \ interior (Ioc a b) = {a, b}
rw₁ : Icc a b \ interior (Ioc a b) = {a, b}
rw₂ : Icc a b \ Ioo a b = {a, b}
rw₃ rw₄ : Eq (α := Set α) {a, b} {a, b}
⊢ frontier (Ioc a b) = {a, b}

Tactic:
rw [frontier, closure_Ioc h.ne, interior_Ioc, Icc_diff_Ioo_same h.le]

Premises used: frontier, LT.lt.le, interior_Ioc, Set.Icc_diff_Ioo_same, LT.lt.ne, closure_Ioc
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
H₁ : (Ioi a).Nonempty
H₂ : a ≤ b
rwa rwa₁ rwa₂ rwa₃ : b ∈ Ici a
⊢ b ∈ closure[inst] (Ioi a)

Tactic:
rwa [closure_Ioi' H₁]

Premises used: closure_Ioi'
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMaxOrder α
a b : α
H : a ≤ b
⊢ (𝓝[Ioi a] b).NeBot

Tactic:
nhdsWithin_Ioi_neBot' nonempty_Ioi H

Premises used: nhdsWithin_Ioi_neBot', Set.nonempty_Ioi
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
H : ∃ (b : α), a < b
⊢ (𝓝[>] a).NeBot

Tactic:
nhdsWithin_Ioi_neBot' H (le_refl a)

Premises used: nhdsWithin_Ioi_neBot', le_refl
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a_1 b : α
s : Set α
inst_4 : NoMaxOrder α
a : α
⊢ (𝓝[>] a).NeBot

Tactic:
nhdsWithin_Ioi_neBot le_rfl

Premises used: le_rfl, nhdsWithin_Ioi_neBot
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
b c : α
H₁ : (Iio c).Nonempty
H₂ : b ≤ c
rwa rwa₁ rwa₂ rwa₃ : b ∈ Iic c
⊢ b ∈ closure[inst] (Iio c)

Tactic:
rwa [closure_Iio' H₁]

Premises used: closure_Iio'
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
a b : α
H : a ≤ b
⊢ (𝓝[Iio b] a).NeBot

Tactic:
nhdsWithin_Iio_neBot' nonempty_Iio H

Premises used: nhdsWithin_Iio_neBot', Set.nonempty_Iio
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
b : α
H : ∃ (a : α), a < b
⊢ (𝓝[<] b).NeBot

Tactic:
nhdsWithin_Iio_neBot' H (le_refl b)

Premises used: le_refl, nhdsWithin_Iio_neBot'
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a_1 b : α
s : Set α
inst_4 : NoMinOrder α
a : α
⊢ (𝓝[<] a).NeBot

Tactic:
nhdsWithin_Iio_neBot (le_refl a)

Premises used: le_refl, nhdsWithin_Iio_neBot
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
H : a < b
⊢ (𝓝[Ico a b] b).NeBot

Tactic:
(isLUB_Ico H).nhdsWithin_neBot (nonempty_Ico.2 H)

Premises used: Iff.mpr, IsLUB.nhdsWithin_neBot, Set.nonempty_Ico, isLUB_Ico
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
H : a < b
⊢ (𝓝[Ioc a b] a).NeBot

Tactic:
(isGLB_Ioc H).nhdsWithin_neBot (nonempty_Ioc.2 H)

Premises used: Iff.mpr, Set.nonempty_Ioc, IsGLB.nhdsWithin_neBot, isGLB_Ioc
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
H : a < b
⊢ (𝓝[Ioo a b] a).NeBot

Tactic:
(isGLB_Ioo H).nhdsWithin_neBot (nonempty_Ioo.2 H)

Premises used: Iff.mpr, isGLB_Ioo, Set.nonempty_Ioo, IsGLB.nhdsWithin_neBot
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
H : a < b
⊢ (𝓝[Ioo a b] b).NeBot

Tactic:
(isLUB_Ioo H).nhdsWithin_neBot (nonempty_Ioo.2 H)

Premises used: Iff.mpr, Set.nonempty_Ioo, isLUB_Ioo, IsLUB.nhdsWithin_neBot
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
x : α
inst_4 : Nontrivial α
⊢ (𝓝[≠] x).NeBot

Tactic:
forall_mem_nonempty_iff_neBot.1 fun s hs => ?_

Premises used: Filter.forall_mem_nonempty_iff_neBot, Iff.mp
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
x : α
inst_4 : Nontrivial α
refine : ∀ (s : Set α) (hs : s ∈ 𝓝[≠] x), s.Nonempty
⊢ (𝓝[≠] x).NeBot

Tactic:
refine forall_mem_nonempty_iff_neBot.1 fun s hs => ?_

Premises used: Filter.forall_mem_nonempty_iff_neBot, Iff.mp
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s_1 : Set α
x : α
inst_4 : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
⊢ ∃ (u : Set α), IsOpen[inst] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ s

Tactic:
mem_nhdsWithin.1 hs

Premises used: mem_nhdsWithin, Iff.mp
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s_1 : Set α
x : α
inst_4 : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
obtain : ∀ (u : Set α) (u_open : IsOpen[inst] u) (xu : x ∈ u) (us : u ∩ {x}ᶜ ⊆ s), s.Nonempty
⊢ s.Nonempty

Tactic:
obtain ⟨u, u_open, xu, us⟩ : ∃ u : Set α, IsOpen u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ s := mem_nhdsWithin.1 hs

Premises used: mem_nhdsWithin, Iff.mp, Set
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s_1 : Set α
x : α
inst_4 : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
u : Set α
u_open : IsOpen[inst] u
xu : x ∈ u
us : u ∩ {x}ᶜ ⊆ s
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ u

Tactic:
u_open.exists_Ioo_subset ⟨x, xu⟩

Premises used: IsOpen.exists_Ioo_subset, Exists.intro
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s_1 : Set α
x : α
inst_4 : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
u : Set α
u_open : IsOpen[inst] u
xu : x ∈ u
us : u ∩ {x}ᶜ ⊆ s
obtain : ∀ (a b : α) (a_lt_b : a < b) (hab : Ioo a b ⊆ u), s.Nonempty
⊢ s.Nonempty

Tactic:
obtain ⟨a, b, a_lt_b, hab⟩ : ∃ a b : α, a < b ∧ Ioo a b ⊆ u := u_open.exists_Ioo_subset ⟨x, xu⟩

Premises used: IsOpen.exists_Ioo_subset, Exists.intro, Set.Ioo
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a_1 b_1 : α
s_1 : Set α
x : α
inst_4 : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
u : Set α
u_open : IsOpen[inst] u
xu : x ∈ u
us : u ∩ {x}ᶜ ⊆ s
a b : α
a_lt_b : a < b
hab : Ioo a b ⊆ u
⊢ ∃ (y : α), a < y ∧ y < b

Tactic:
exists_between a_lt_b

Premises used: exists_between
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a_1 b_1 : α
s_1 : Set α
x : α
inst_4 : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
u : Set α
u_open : IsOpen[inst] u
xu : x ∈ u
us : u ∩ {x}ᶜ ⊆ s
a b : α
a_lt_b : a < b
hab : Ioo a b ⊆ u
obtain : ∀ (y : α) (hy : a < y ∧ y < b), s.Nonempty
⊢ s.Nonempty

Tactic:
obtain ⟨y, hy⟩ : ∃ y, a < y ∧ y < b := exists_between a_lt_b

Premises used: exists_between
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a_1 b_1 : α
s_1 : Set α
x : α
inst_4 : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
u : Set α
u_open : IsOpen[inst] u
xu : x ∈ u
us : u ∩ {x}ᶜ ⊆ s
a b : α
a_lt_b : a < b
hab : Ioo a b ⊆ u
y : α
hy : a < y ∧ y < b
inl : ∀ (xy : x ≠ y), s.Nonempty
inr : ∀ (hy : a < x ∧ x < b), s.Nonempty
⊢ s.Nonempty

Tactic:
rcases ne_or_eq x y with (xy | rfl)

Premises used: ne_or_eq, rfl
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a_1 b_1 : α
s_1 : Set α
x : α
inst_4 : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
u : Set α
u_open : IsOpen[inst] u
xu : x ∈ u
us : u ∩ {x}ᶜ ⊆ s
a b : α
a_lt_b : a < b
hab : Ioo a b ⊆ u
y : α
hy : a < y ∧ y < b
xy : x ≠ y
⊢ s.Nonempty

Tactic:
⟨y, us ⟨hab hy, xy.symm⟩⟩

Premises used: Ne.symm, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a_1 b_1 : α
s_1 : Set α
x : α
inst_4 : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
u : Set α
u_open : IsOpen[inst] u
xu : x ∈ u
us : u ∩ {x}ᶜ ⊆ s
a b : α
a_lt_b : a < b
hab : Ioo a b ⊆ u
y : α
hy : a < y ∧ y < b
xy : x ≠ y
⊢ s.Nonempty

Tactic:
exact ⟨y, us ⟨hab hy, xy.symm⟩⟩
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a_1 b_1 : α
s_1 : Set α
x : α
inst_4 : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
u : Set α
u_open : IsOpen[inst] u
xu : x ∈ u
us : u ∩ {x}ᶜ ⊆ s
a b : α
a_lt_b : a < b
hab : Ioo a b ⊆ u
hy : a < x ∧ x < b
⊢ ∃ (z : α), a < z ∧ z < x

Tactic:
exists_between hy.1

Premises used: exists_between, And.left
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a_1 b_1 : α
s_1 : Set α
x : α
inst_4 : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
u : Set α
u_open : IsOpen[inst] u
xu : x ∈ u
us : u ∩ {x}ᶜ ⊆ s
a b : α
a_lt_b : a < b
hab : Ioo a b ⊆ u
hy : a < x ∧ x < b
inr : ∀ (z : α) (hz : a < z ∧ z < x), s.Nonempty
⊢ s.Nonempty

Tactic:
obtain ⟨z, hz⟩ : ∃ z, a < z ∧ z < x := exists_between hy.1

Premises used: exists_between, And.left
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a_1 b_1 : α
s_1 : Set α
x : α
inst_4 : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
u : Set α
u_open : IsOpen[inst] u
xu : x ∈ u
us : u ∩ {x}ᶜ ⊆ s
a b : α
a_lt_b : a < b
hab : Ioo a b ⊆ u
hy : a < x ∧ x < b
z : α
hz : a < z ∧ z < x
⊢ s.Nonempty

Tactic:
⟨z, us ⟨hab ⟨hz.1, hz.2.trans hy.2⟩, hz.2.ne⟩⟩

Premises used: Set.Nonempty, And.right, And.left, And.intro, Exists.intro, LT.lt.trans, LT.lt.ne
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a_1 b_1 : α
s_1 : Set α
x : α
inst_4 : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
u : Set α
u_open : IsOpen[inst] u
xu : x ∈ u
us : u ∩ {x}ᶜ ⊆ s
a b : α
a_lt_b : a < b
hab : Ioo a b ⊆ u
hy : a < x ∧ x < b
z : α
hz : a < z ∧ z < x
⊢ s.Nonempty

Tactic:
exact ⟨z, us ⟨hab ⟨hz.1, hz.2.trans hy.2⟩, hz.2.ne⟩⟩
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : DiscreteTopology α
suffices : ∀ (a b : α), b ≤ a
⊢ Subsingleton α

Tactic:
suffices ∀ a b : α, b ≤ a from ⟨fun a b ↦ le_antisymm (this b a) (this a b)⟩
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : DiscreteTopology α
a b : α
by_contra! : ∀ (contra : a < b), False
⊢ b ≤ a

Tactic:
by_contra! contra
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : DiscreteTopology α
a b : α
contra : a < b
rw : closure[inst] (Ioo a b) = Icc a b
rw₁ rw₂ : Icc a b = Icc a b
⊢ Ioo a b = Icc a b

Tactic:
rw [← closure_discrete (Ioo a b), closure_Ioo contra.ne]

Premises used: closure_discrete, Set.Ioo, LT.lt.ne, closure_Ioo
-- Module: Mathlib.Topology.Order.DenselyOrdered
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : DiscreteTopology α
a b : α
contra : a < b
⊢ Ioo a b = Icc a b

Tactic:
have : Ioo a b = Icc a b := by rw [← closure_discrete (Ioo a b), closure_Ioo contra.ne]