awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
hs : IsOpen[inst] s
h : s.Nonempty
obtain : ∀ (x : α) (hx : x ∈ s), ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s

Tactic:
obtain ⟨x, hx⟩ : ∃ x, x ∈ s := h
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
hs : IsOpen[inst] s
x : α
hx : x ∈ s
⊢ ∃ (y : α), y ≠ x

Tactic:
exists_ne x

Premises used: exists_ne
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
hs : IsOpen[inst] s
x : α
hx : x ∈ s
obtain : ∀ (y : α) (hy : y ≠ x), ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s

Tactic:
obtain ⟨y, hy⟩ : ∃ y, y ≠ x := exists_ne x

Premises used: exists_ne
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
hs : IsOpen[inst] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
inl : ∀ (H : x < y), ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
inr : ∀ (hy : x ≠ x), ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
inr₁ : ∀ (H : y < x), ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s

Tactic:
rcases lt_trichotomy x y with (H | rfl | H)

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
hs : IsOpen[inst] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : x < y
⊢ ∃ (u : α), x < u ∧ Ico x u ⊆ s

Tactic:
exists_Ico_subset_of_mem_nhds (hs.mem_nhds hx) ⟨y, H⟩

Premises used: IsOpen.mem_nhds, Exists.intro, exists_Ico_subset_of_mem_nhds
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
hs : IsOpen[inst] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : x < y
inl : ∀ (u : α) (xu : x < u) (hu : Ico x u ⊆ s), ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s

Tactic:
obtain ⟨u, xu, hu⟩ : ∃ u, x < u ∧ Ico x u ⊆ s :=
      exists_Ico_subset_of_mem_nhds (hs.mem_nhds hx) ⟨y, H⟩

Premises used: IsOpen.mem_nhds, Exists.intro, exists_Ico_subset_of_mem_nhds
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
hs : IsOpen[inst] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : x < y
u : α
xu : x < u
hu : Ico x u ⊆ s
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s

Tactic:
⟨x, u, xu, Ioo_subset_Ico_self.trans hu⟩

Premises used: HasSubset.Subset.trans, Set.Ioo_subset_Ico_self, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
hs : IsOpen[inst] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : x < y
u : α
xu : x < u
hu : Ico x u ⊆ s
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s

Tactic:
exact ⟨x, u, xu, Ioo_subset_Ico_self.trans hu⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
hs : IsOpen[inst] s
x : α
hx : x ∈ s
hy : x ≠ x
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s

Tactic:
(hy rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
hs : IsOpen[inst] s
x : α
hx : x ∈ s
hy : x ≠ x
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s

Tactic:
exact (hy rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
hs : IsOpen[inst] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : y < x
⊢ ∃ l < x, Ioc l x ⊆ s

Tactic:
exists_Ioc_subset_of_mem_nhds (hs.mem_nhds hx) ⟨y, H⟩

Premises used: exists_Ioc_subset_of_mem_nhds, IsOpen.mem_nhds, Exists.intro
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
hs : IsOpen[inst] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : y < x
inr : ∀ (l : α) (lx : l < x) (hl : Ioc l x ⊆ s), ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s

Tactic:
obtain ⟨l, lx, hl⟩ : ∃ l, l < x ∧ Ioc l x ⊆ s :=
      exists_Ioc_subset_of_mem_nhds (hs.mem_nhds hx) ⟨y, H⟩

Premises used: exists_Ioc_subset_of_mem_nhds, IsOpen.mem_nhds, Exists.intro
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
hs : IsOpen[inst] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : y < x
l : α
lx : l < x
hl : Ioc l x ⊆ s
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s

Tactic:
⟨l, x, lx, Ioo_subset_Ioc_self.trans hl⟩

Premises used: HasSubset.Subset.trans, Set.Ioo_subset_Ioc_self, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
hs : IsOpen[inst] s
x : α
hx : x ∈ s
y : α
hy : y ≠ x
H : y < x
l : α
lx : l < x
hl : Ioc l x ⊆ s
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s

Tactic:
exact ⟨l, x, lx, Ioo_subset_Ioc_self.trans hl⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, c ∈ Ioo a b
⊢ Dense s

Tactic:
dense_iff_inter_open.2 fun U U_open U_nonempty => ?_

Premises used: Iff.mpr, dense_iff_inter_open
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, c ∈ Ioo a b
refine : ∀ (U : Set α) (U_open : IsOpen[inst] U) (U_nonempty : U.Nonempty), (U ∩ s).Nonempty
⊢ Dense s

Tactic:
refine dense_iff_inter_open.2 fun U U_open U_nonempty => ?_

Premises used: Iff.mpr, dense_iff_inter_open
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, c ∈ Ioo a b
U : Set α
U_open : IsOpen[inst] U
U_nonempty : U.Nonempty
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ U

Tactic:
U_open.exists_Ioo_subset U_nonempty

Premises used: IsOpen.exists_Ioo_subset
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, c ∈ Ioo a b
U : Set α
U_open : IsOpen[inst] U
U_nonempty : U.Nonempty
obtain : ∀ (a b : α) (hab : a < b) (H : Ioo a b ⊆ U), (U ∩ s).Nonempty
⊢ (U ∩ s).Nonempty

Tactic:
obtain ⟨a, b, hab, H⟩ : ∃ a b : α, a < b ∧ Ioo a b ⊆ U := U_open.exists_Ioo_subset U_nonempty

Premises used: IsOpen.exists_Ioo_subset
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, c ∈ Ioo a b
U : Set α
U_open : IsOpen[inst] U
U_nonempty : U.Nonempty
a b : α
hab : a < b
H : Ioo a b ⊆ U
⊢ ∃ x ∈ s, a < x ∧ x < b

Tactic:
h hab

Premises used: Set.Mem, setOf, Set.Ioo
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, c ∈ Ioo a b
U : Set α
U_open : IsOpen[inst] U
U_nonempty : U.Nonempty
a b : α
hab : a < b
H : Ioo a b ⊆ U
obtain : ∀ (x : α) (xs : x ∈ s) (hx : a < x ∧ x < b), (U ∩ s).Nonempty
⊢ (U ∩ s).Nonempty

Tactic:
obtain ⟨x, xs, hx⟩ : ∃ x ∈ s, a < x ∧ x < b := h hab
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, c ∈ Ioo a b
U : Set α
U_open : IsOpen[inst] U
U_nonempty : U.Nonempty
a b : α
hab : a < b
H : Ioo a b ⊆ U
x : α
xs : x ∈ s
hx : a < x ∧ x < b
⊢ (U ∩ s).Nonempty

Tactic:
⟨x, ⟨H hx, xs⟩⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
h : ∀ ⦃a b : α⦄, a < b → ∃ c ∈ s, c ∈ Ioo a b
U : Set α
U_open : IsOpen[inst] U
U_nonempty : U.Nonempty
a b : α
hab : a < b
H : Ioo a b ⊆ U
x : α
xs : x ∈ s
hx : a < x ∧ x < b
⊢ (U ∩ s).Nonempty

Tactic:
exact ⟨x, ⟨H hx, xs⟩⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : WellFoundedLT α
s : Set α
h : IsUpperSet s
inl : ∀ (h : IsUpperSet.{u} (α := α) ∅), IsClosed[inst] ∅
inr : ∀ (a : α) (h : IsUpperSet (Ici a)), IsClosed[inst] (Ici a)
⊢ IsClosed[inst] s

Tactic:
obtain rfl | ⟨a, rfl⟩ := h.eq_empty_or_Ici

Premises used: IsUpperSet.eq_empty_or_Ici, rfl
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : WellFoundedLT α
h : IsUpperSet.{u} (α := α) ∅
⊢ IsClosed[inst] ∅

Tactic:
isClosed_empty

Premises used: isClosed_empty
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : WellFoundedLT α
a : α
h : IsUpperSet (Ici a)
⊢ IsClosed[inst] (Ici a)

Tactic:
isClosed_Ici

Premises used: isClosed_Ici
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : WellFoundedLT α
h : IsUpperSet.{u} (α := α) ∅
⊢ IsClosed[inst] ∅

Tactic:
exacts [isClosed_empty, isClosed_Ici]

Premises used: isClosed_empty, isClosed_Ici
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : WellFoundedLT α
s : Set α
h : IsLowerSet s
⊢ IsOpen[inst] s

Tactic:
simpa using h.compl.isClosed

Premises used: IsLowerSet.compl, IsUpperSet.isClosed
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
s : Set α
⊢ Dense s ↔ ∀ (a b : α), a < b → ∃ c ∈ s, a < c ∧ c < b

Tactic:
⟨fun h _ _ hab => h.exists_between hab, dense_of_exists_between⟩

Premises used: Dense.exists_between, Iff.intro, dense_of_exists_between
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hl : ∃ (l : α), l < a
hu : ∃ (u : α), a < u
mp : s ∈ 𝓝 a → ∃ (l : α) (u : α), a ∈ Ioo l u ∧ Ioo l u ⊆ s
mpr : (∃ (l : α) (u : α), a ∈ Ioo l u ∧ Ioo l u ⊆ s) → s ∈ 𝓝 a
⊢ s ∈ 𝓝 a ↔ ∃ (l : α) (u : α), a ∈ Ioo l u ∧ Ioo l u ⊆ s

Tactic:
constructor
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hl : ∃ (l : α), l < a
hu : ∃ (u : α), a < u
h : s ∈ 𝓝 a
mp : ∀ (u : α) (au : a < u) (hu : Ico a u ⊆ s), ∃ (l : α) (u : α), a ∈ Ioo l u ∧ Ioo l u ⊆ s
⊢ ∃ (l : α) (u : α), a ∈ Ioo l u ∧ Ioo l u ⊆ s

Tactic:
rcases exists_Ico_subset_of_mem_nhds h hu with ⟨u, au, hu⟩

Premises used: exists_Ico_subset_of_mem_nhds
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hl : ∃ (l : α), l < a
hu_1 : ∃ (u : α), a < u
h : s ∈ 𝓝 a
u : α
au : a < u
hu : Ico a u ⊆ s
mp : ∀ (l : α) (la : l < a) (hl : Ioc l a ⊆ s), ∃ (l : α) (u : α), a ∈ Ioo l u ∧ Ioo l u ⊆ s
⊢ ∃ (l : α) (u : α), a ∈ Ioo l u ∧ Ioo l u ⊆ s

Tactic:
rcases exists_Ioc_subset_of_mem_nhds h hl with ⟨l, la, hl⟩

Premises used: exists_Ioc_subset_of_mem_nhds
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hl_1 : ∃ (l : α), l < a
hu_1 : ∃ (u : α), a < u
h : s ∈ 𝓝 a
u : α
au : a < u
hu : Ico a u ⊆ s
l : α
la : l < a
hl : Ioc l a ⊆ s
⊢ ∃ (l : α) (u : α), a ∈ Ioo l u ∧ Ioo l u ⊆ s

Tactic:
⟨l, u, ⟨la, au⟩, Ioc_union_Ico_eq_Ioo la au ▸ union_subset hl hu⟩

Premises used: Eq.rec, Set.union_subset, And.intro, Exists.intro, Set.Ioc_union_Ico_eq_Ioo
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hl_1 : ∃ (l : α), l < a
hu_1 : ∃ (u : α), a < u
h : s ∈ 𝓝 a
u : α
au : a < u
hu : Ico a u ⊆ s
l : α
la : l < a
hl : Ioc l a ⊆ s
⊢ ∃ (l : α) (u : α), a ∈ Ioo l u ∧ Ioo l u ⊆ s

Tactic:
exact ⟨l, u, ⟨la, au⟩, Ioc_union_Ico_eq_Ioo la au ▸ union_subset hl hu⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hl : ∃ (l : α), l < a
hu : ∃ (u : α), a < u
l u : α
ha : a ∈ Ioo l u
h : Ioo l u ⊆ s
⊢ s ∈ 𝓝 a

Tactic:
apply mem_of_superset (Ioo_mem_nhds ha.1 ha.2) h

Premises used: Ioo_mem_nhds, And.right, And.left, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
inst_4 : NoMinOrder α
a : α
s : Set α
⊢ s ∈ 𝓝 a ↔ ∃ (l : α) (u : α), a ∈ Ioo l u ∧ Ioo l u ⊆ s

Tactic:
mem_nhds_iff_exists_Ioo_subset' (exists_lt a) (exists_gt a)

Premises used: NoMaxOrder.exists_gt, NoMinOrder.exists_lt, mem_nhds_iff_exists_Ioo_subset'
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
hl : ∃ (l : α), l < a
hu : ∃ (u : α), a < u
s : Set α
⊢ (∃ (l : α) (u : α), a ∈ Ioo l u ∧ Ioo l u ⊆ s) ↔ ∃ (i : α × α), (i.1 < a ∧ a < i.2) ∧ Ioo i.1 i.2 ⊆ s

Tactic:
simp
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
inst_4 : NoMinOrder α
a : α
⊢ (𝓝 a).HasBasis (fun (b : α × α) ↦ b.1 < a ∧ a < b.2) fun (b : α × α) ↦ Ioo b.1 b.2

Tactic:
nhds_basis_Ioo' (exists_lt a) (exists_gt a)

Premises used: NoMaxOrder.exists_gt, nhds_basis_Ioo', NoMinOrder.exists_lt
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
inst_4 : NoMinOrder α
a : α
p : α → Prop
hp : ∀ᶠ (x : α) in 𝓝 a, p x
⊢ ∃ (l : α) (u : α), a ∈ Ioo l u ∧ Ioo l u ⊆ {x : α | p x}

Tactic:
mem_nhds_iff_exists_Ioo_subset.1 hp

Premises used: Iff.mp, mem_nhds_iff_exists_Ioo_subset
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
⊢ inst = generateFrom (Ioi '' s ∪ Iio '' s)

Tactic:
(OrderTopology.topology_eq_generate_intervals (α := α)).trans ?_

Premises used: OrderTopology.topology_eq_generate_intervals, Eq.trans
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
refine : Preorder.topology α = generateFrom (Ioi '' s ∪ Iio '' s)
⊢ inst = generateFrom (Ioi '' s ∪ Iio '' s)

Tactic:
refine (OrderTopology.topology_eq_generate_intervals (α := α)).trans ?_

Premises used: OrderTopology.topology_eq_generate_intervals, Eq.trans
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
⊢ Preorder.topology α = generateFrom (Ioi '' s ∪ Iio '' s)

Tactic:
le_antisymm (generateFrom_anti ?_) (le_generateFrom ?_)

Premises used: TopologicalSpace.generateFrom_anti, le_antisymm, le_generateFrom
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
refine_1 : Ioi '' s ∪ Iio '' s ⊆ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
refine_2 :
  ∀ (s_1 : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} s_1 →
      IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] s_1
⊢ Preorder.topology α = generateFrom (Ioi '' s ∪ Iio '' s)

Tactic:
refine le_antisymm (generateFrom_anti ?_) (le_generateFrom ?_)

Premises used: TopologicalSpace.generateFrom_anti, le_antisymm, le_generateFrom
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
refine_1 :
  s ⊆ Ioi ⁻¹' {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} ∧
    s ⊆ Iio ⁻¹' {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
⊢ Ioi '' s ∪ Iio '' s ⊆ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}

Tactic:
simp only [union_subset_iff, image_subset_iff]

Premises used: Set.union_subset_iff, Set.image_subset_iff
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
⊢ s ⊆ Ioi ⁻¹' {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} ∧
    s ⊆ Iio ⁻¹' {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}

Tactic:
⟨fun a _ ↦ ⟨a, .inl rfl⟩, fun a _ ↦ ⟨a, .inr rfl⟩⟩

Premises used: And.intro, Exists.intro, Or.inl, Or.inr, rfl
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
⊢ s ⊆ Ioi ⁻¹' {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} ∧
    s ⊆ Iio ⁻¹' {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}

Tactic:
exact ⟨fun a _ ↦ ⟨a, .inl rfl⟩, fun a _ ↦ ⟨a, .inr rfl⟩⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
a : α
refine_2 : IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (⋃ y ∈ s ∩ Ioi a, Ioi y)
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (Ioi a)

Tactic:
rw [hs.Ioi_eq_biUnion]

Premises used: Dense.Ioi_eq_biUnion
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
a : α
x : TopologicalSpace α := generateFrom (Ioi '' s ∪ Iio '' s)
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (⋃ y ∈ s ∩ Ioi a, Ioi y)

Tactic:
isOpen_iUnion fun x ↦ isOpen_iUnion fun h ↦ .basic _ <| .inl <| mem_image_of_mem _ h.1

Premises used: Set.Ioi, TopologicalSpace.GenerateOpen.basic, isOpen_iUnion, And.left, Set.mem_image_of_mem, Or.inl
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
a : α
x : TopologicalSpace α := generateFrom (Ioi '' s ∪ Iio '' s)
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (⋃ y ∈ s ∩ Ioi a, Ioi y)

Tactic:
exact isOpen_iUnion fun x ↦ isOpen_iUnion fun h ↦ .basic _ <| .inl <| mem_image_of_mem _ h.1
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
a : α
refine_2 : IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (⋃ y ∈ s ∩ Iio a, Iio y)
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (Iio a)

Tactic:
rw [hs.Iio_eq_biUnion]

Premises used: Dense.Iio_eq_biUnion
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
a : α
x : TopologicalSpace α := generateFrom (Ioi '' s ∪ Iio '' s)
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (⋃ y ∈ s ∩ Iio a, Iio y)

Tactic:
isOpen_iUnion fun x ↦ isOpen_iUnion fun h ↦ .basic _ <| .inr <| mem_image_of_mem _ h.1

Premises used: TopologicalSpace.GenerateOpen.basic, isOpen_iUnion, And.left, Set.mem_image_of_mem, Set.Iio, Or.inr
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
a : α
x : TopologicalSpace α := generateFrom (Ioi '' s ∪ Iio '' s)
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (⋃ y ∈ s ∩ Iio a, Iio y)

Tactic:
exact isOpen_iUnion fun x ↦ isOpen_iUnion fun h ↦ .basic _ <| .inr <| mem_image_of_mem _ h.1
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SuccOrder α
a : α
ha : ∃ (l : α), l < a
⊢ (𝓝 a).HasBasis (fun (x : α) ↦ x < a) fun (x : α) ↦ Ioc x a

Tactic:
SuccOrder.nhdsLE_eq_nhds a ▸ nhdsLE_basis_of_exists_lt ha

Premises used: SuccOrder.nhdsLE_eq_nhds, nhdsLE_basis_of_exists_lt, Eq.rec
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SuccOrder α
a : α
inst_4 : NoMinOrder α
⊢ (𝓝 a).HasBasis (fun (x : α) ↦ x < a) fun (x : α) ↦ Ioc x a

Tactic:
SuccOrder.hasBasis_nhds_Ioc_of_exists_lt (exists_lt a)

Premises used: SuccOrder.hasBasis_nhds_Ioc_of_exists_lt, NoMinOrder.exists_lt
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : SeparableSpace α
rcases : ∀ (s : Set α) (hc : s.Countable) (hd : Dense s), SecondCountableTopology α
⊢ SecondCountableTopology α

Tactic:
rcases exists_countable_dense α with ⟨s, hc, hd⟩

Premises used: TopologicalSpace.exists_countable_dense
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : SeparableSpace α
s : Set α
hc : s.Countable
hd : Dense s
⊢ SecondCountableTopology α

Tactic:
⟨⟨_, ?_, hd.topology_eq_generateFrom⟩⟩

Premises used: SecondCountableTopology.mk, And.intro, Exists.intro, Dense.topology_eq_generateFrom
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : SeparableSpace α
s : Set α
hc : s.Countable
hd : Dense s
refine : (Ioi '' s ∪ Iio '' s).Countable
⊢ SecondCountableTopology α

Tactic:
refine ⟨⟨_, ?_, hd.topology_eq_generateFrom⟩⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : SeparableSpace α
s : Set α
hc : s.Countable
hd : Dense s
⊢ (Ioi '' s ∪ Iio '' s).Countable

Tactic:
(hc.image _).union (hc.image _)

Premises used: Set.Countable.image, Set.Countable.union
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : SeparableSpace α
s : Set α
hc : s.Countable
hd : Dense s
⊢ (Ioi '' s ∪ Iio '' s).Countable

Tactic:
exact (hc.image _).union (hc.image _)

Premises used: Set.Countable.image, Set.Countable.union
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
⊢ ∀ x ∈ s, ∃ (y : α), x ⋖ y

Tactic:
have : ∀ x ∈ s, ∃ y, x ⋖ y := fun x => id
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
this : ∀ x ∈ s, ∃ (y : α), x ⋖ y
choose! : ∀ (y : (x : α) → α) (hy : ∀ x ∈ s, x ⋖ y x), Set.Countable.{u} (α := α) {x : α | ∃ (y : α), x ⋖ y}
⊢ Set.Countable.{u} (α := α) {x : α | ∃ (y : α), x ⋖ y}

Tactic:
choose! y hy using this