awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
⊢ interior (Icc a b) = Ioo a b
have rw₂ : Ioi a ∩ interior (Iic b) = Ioo a b
Tactic: rw [← Ici_inter_Iic, interior_inter, interior_Ici, interior_Iic, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
⊢ interior (Icc a b) = Ioo a b
have rw₃ : Ioi a ∩ Iio b = Ioo a b
Tactic: rw [← Ici_inter_Iic, interior_inter, interior_Ici, interior_Iic, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
⊢ interior (Icc a b) = Ioo a b
have rw₄ : Ioo a b = Ioo a b
Tactic: rw [← Ici_inter_Iic, interior_inter, interior_Ici, interior_Iic, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
inst_5 : NoMaxOrder α
a b x : α
⊢ Icc a b ∈ 𝓝 x ↔ x ∈ Ioo a b
have rw : Icc a b ∈ 𝓝 x ↔ x ∈ interior (Icc a b)
Tactic: rw [← interior_Icc, mem_interior_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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)
⊢ Icc a b ∈ 𝓝 x ↔ x ∈ Ioo a b
have rw₁ : Icc a b ∈ 𝓝 x ↔ Icc a b ∈ 𝓝 x
Tactic: rw [← interior_Icc, mem_interior_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
a b : α
⊢ interior (Ico a b) = Ioo a b
have rw : interior (Ici a ∩ Iio b) = Ioo a b
Tactic: rw [← Ici_inter_Iio, interior_inter, interior_Ici, interior_Iio, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
⊢ interior (Ico a b) = Ioo a b
have rw₁ : interior (Ici a) ∩ interior (Iio b) = Ioo a b
Tactic: rw [← Ici_inter_Iio, interior_inter, interior_Ici, interior_Iio, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
⊢ interior (Ico a b) = Ioo a b
have rw₂ : Ioi a ∩ interior (Iio b) = Ioo a b
Tactic: rw [← Ici_inter_Iio, interior_inter, interior_Ici, interior_Iio, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
⊢ interior (Ico a b) = Ioo a b
have rw₃ : Ioi a ∩ Iio b = Ioo a b
Tactic: rw [← Ici_inter_Iio, interior_inter, interior_Ici, interior_Iio, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
⊢ interior (Ico a b) = Ioo a b
have rw₄ : Ioo a b = Ioo a b
Tactic: rw [← Ici_inter_Iio, interior_inter, interior_Ici, interior_Iio, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
a b x : α
⊢ Ico a b ∈ 𝓝 x ↔ x ∈ Ioo a b
have rw : Ico a b ∈ 𝓝 x ↔ x ∈ interior (Ico a b)
Tactic: rw [← interior_Ico, mem_interior_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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)
⊢ Ico a b ∈ 𝓝 x ↔ x ∈ Ioo a b
have rw₁ : Ico a b ∈ 𝓝 x ↔ Ico a b ∈ 𝓝 x
Tactic: rw [← interior_Ico, mem_interior_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMaxOrder α
a b : α
⊢ interior (Ioc a b) = Ioo a b
have rw : interior (Ioi a ∩ Iic b) = Ioo a b
Tactic: rw [← Ioi_inter_Iic, interior_inter, interior_Ioi, interior_Iic, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
⊢ interior (Ioc a b) = Ioo a b
have rw₁ : interior (Ioi a) ∩ interior (Iic b) = Ioo a b
Tactic: rw [← Ioi_inter_Iic, interior_inter, interior_Ioi, interior_Iic, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
⊢ interior (Ioc a b) = Ioo a b
have rw₂ : Ioi a ∩ interior (Iic b) = Ioo a b
Tactic: rw [← Ioi_inter_Iic, interior_inter, interior_Ioi, interior_Iic, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
⊢ interior (Ioc a b) = Ioo a b
have rw₃ : Ioi a ∩ Iio b = Ioo a b
Tactic: rw [← Ioi_inter_Iic, interior_inter, interior_Ioi, interior_Iic, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
⊢ interior (Ioc a b) = Ioo a b
have rw₄ : Ioo a b = Ioo a b
Tactic: rw [← Ioi_inter_Iic, interior_inter, interior_Ioi, interior_Iic, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMaxOrder α
a b x : α
⊢ Ioc a b ∈ 𝓝 x ↔ x ∈ Ioo a b
have rw : Ioc a b ∈ 𝓝 x ↔ x ∈ interior (Ioc a b)
Tactic: rw [← interior_Ioc, mem_interior_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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)
⊢ Ioc a b ∈ 𝓝 x ↔ x ∈ Ioo a b
have rw₁ : Ioc a b ∈ 𝓝 x ↔ Ioc a b ∈ 𝓝 x
Tactic: rw [← interior_Ioc, mem_interior_iff_mem_nhds]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
⊢ Ioc a b ⊆ closure[inst] (interior (Ioc a b))
have inl : Ioc a a ⊆ closure[inst] (interior (Ioc a a))
Tactic: rcases eq_or_ne a b with (rfl | h)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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))
⊢ Ioc a b ⊆ closure[inst] (interior (Ioc a b))
have inr : ∀ (h : a ≠ b), Ioc a b ⊆ closure[inst] (interior (Ioc a b))
Tactic: rcases eq_or_ne a b with (rfl | h)
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : a < b
⊢ frontier (Ioo a b) = {a, b}
have rw : closure[inst] (Ioo a b) \ interior (Ioo a b) = {a, b}
Tactic: rw [frontier, closure_Ioo h.ne, interior_Ioo, Icc_diff_Ioo_same h.le]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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}
⊢ frontier (Ioo a b) = {a, b}
have rw₁ : Icc a b \ interior (Ioo a b) = {a, b}
Tactic: rw [frontier, closure_Ioo h.ne, interior_Ioo, Icc_diff_Ioo_same h.le]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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}
⊢ frontier (Ioo a b) = {a, b}
have rw₂ : Icc a b \ Ioo a b = {a, b}
Tactic: rw [frontier, closure_Ioo h.ne, interior_Ioo, Icc_diff_Ioo_same h.le]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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}
⊢ frontier (Ioo a b) = {a, b}
have rw₃ : Eq (α := Set α) {a, b} {a, b}
Tactic: rw [frontier, closure_Ioo h.ne, interior_Ioo, Icc_diff_Ioo_same h.le]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMinOrder α
a b : α
h : a < b
⊢ frontier (Ico a b) = {a, b}
have rw : closure[inst] (Ico a b) \ interior (Ico a b) = {a, b}
Tactic: rw [frontier, closure_Ico h.ne, interior_Ico, Icc_diff_Ioo_same h.le]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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}
⊢ frontier (Ico a b) = {a, b}
have rw₁ : Icc a b \ interior (Ico a b) = {a, b}
Tactic: rw [frontier, closure_Ico h.ne, interior_Ico, Icc_diff_Ioo_same h.le]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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}
⊢ frontier (Ico a b) = {a, b}
have rw₂ : Icc a b \ Ioo a b = {a, b}
Tactic: rw [frontier, closure_Ico h.ne, interior_Ico, Icc_diff_Ioo_same h.le]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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}
⊢ frontier (Ico a b) = {a, b}
have rw₃ : Eq (α := Set α) {a, b} {a, b}
Tactic: rw [frontier, closure_Ico h.ne, interior_Ico, Icc_diff_Ioo_same h.le]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : NoMaxOrder α
a b : α
h : a < b
⊢ frontier (Ioc a b) = {a, b}
have rw : closure[inst] (Ioc a b) \ interior (Ioc a b) = {a, b}
Tactic: rw [frontier, closure_Ioc h.ne, interior_Ioc, Icc_diff_Ioo_same h.le]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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}
⊢ frontier (Ioc a b) = {a, b}
have rw₁ : Icc a b \ interior (Ioc a b) = {a, b}
Tactic: rw [frontier, closure_Ioc h.ne, interior_Ioc, Icc_diff_Ioo_same h.le]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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}
⊢ frontier (Ioc a b) = {a, b}
have rw₂ : Icc a b \ Ioo a b = {a, b}
Tactic: rw [frontier, closure_Ioc h.ne, interior_Ioc, Icc_diff_Ioo_same h.le]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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}
⊢ frontier (Ioc a b) = {a, b}
have rw₃ : Eq (α := Set α) {a, b} {a, b}
Tactic: rw [frontier, closure_Ioc h.ne, interior_Ioc, Icc_diff_Ioo_same h.le]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
H₁ : (Ioi a).Nonempty
H₂ : a ≤ b
⊢ b ∈ closure[inst] (Ioi a)
have rwa : b ∈ Ici a
Tactic: rwa [closure_Ioi' H₁]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
b c : α
H₁ : (Iio c).Nonempty
H₂ : b ≤ c
⊢ b ∈ closure[inst] (Iio c)
have rwa : b ∈ Iic c
Tactic: rwa [closure_Iio' H₁]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
have refine : ∀ (s : Set α) (hs : s ∈ 𝓝[≠] x), s.Nonempty
Tactic: refine forall_mem_nonempty_iff_neBot.1 fun s hs => ?_
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
⊢ s.Nonempty
have obtain : ∀ (u : Set α) (u_open : IsOpen[inst] u) (xu : x ∈ u) (us : u ∩ {x}ᶜ ⊆ s), s.Nonempty
Tactic: obtain ⟨u, u_open, xu, us⟩ : ∃ u : Set α, IsOpen u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ s := mem_nhdsWithin.1 hs
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
⊢ s.Nonempty
have obtain : ∀ (a b : α) (a_lt_b : a < b) (hab : Ioo a b ⊆ u), 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⟩
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
⊢ s.Nonempty
have obtain : ∀ (y : α) (hy : a < y ∧ y < b), s.Nonempty
Tactic: obtain ⟨y, hy⟩ : ∃ y, a < y ∧ y < b := exists_between a_lt_b
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
⊢ s.Nonempty
have inl : ∀ (xy : x ≠ y), s.Nonempty
Tactic: rcases ne_or_eq x y with (xy | rfl)
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
⊢ s.Nonempty
have inr : ∀ (hy : a < x ∧ x < b), s.Nonempty
Tactic: rcases ne_or_eq x y with (xy | rfl)
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
⊢ s.Nonempty
have inr : ∀ (z : α) (hz : a < z ∧ z < x), s.Nonempty
Tactic: obtain ⟨z, hz⟩ : ∃ z, a < z ∧ z < x := exists_between hy.1
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : DiscreteTopology α
⊢ Subsingleton α
have suffices : ∀ (a b : α), b ≤ a
Tactic: suffices ∀ a b : α, b ≤ a from ⟨fun a b ↦ le_antisymm (this b a) (this a b)⟩
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : DiscreteTopology α
a b : α
⊢ b ≤ a
have by_contra! : ∀ (contra : a < b), False
Tactic: by_contra! contra
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
have rw : closure[inst] (Ioo a b) = Icc a b
Tactic: rw [← closure_discrete (Ioo a b), closure_Ioo contra.ne]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
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
⊢ Ioo a b = Icc a b
have rw₁ : Icc a b = Icc a b
Tactic: rw [← closure_discrete (Ioo a b), closure_Ioo contra.ne]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : DiscreteTopology α
a b : α
contra : a < b
⊢ False
have this : 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]
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
s : Set α
inst_5 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∉ t) ∧ ∀ (x : α), IsTop x → x ∉ t
have rcases : ∀ (t : Set α) (hts : t ⊆ s) (htc : t.Countable) (htd : Dense t),
  ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∉ t) ∧ ∀ (x : α), IsTop x → x ∉ t
Tactic: rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
s : Set α
inst_5 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∉ t) ∧ ∀ (x : α), IsTop x → x ∉ t
have refine_1 : t \ ({x : α | IsBot x} ∪ {x : α | IsTop x}) ⊆ s
Tactic: refine ⟨t \ ({ x | IsBot x } ∪ { x | IsTop x }), ?_, ?_, ?_, fun x hx => ?_, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
s : Set α
inst_5 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
refine_1 : t \ ({x : α | IsBot x} ∪ {x : α | IsTop x}) ⊆ s
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∉ t) ∧ ∀ (x : α), IsTop x → x ∉ t
have refine_2 : (t \ ({x : α | IsBot x} ∪ {x : α | IsTop x})).Countable
Tactic: refine ⟨t \ ({ x | IsBot x } ∪ { x | IsTop x }), ?_, ?_, ?_, fun x hx => ?_, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
s : Set α
inst_5 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
refine_1 : t \ ({x : α | IsBot x} ∪ {x : α | IsTop x}) ⊆ s
refine_2 : (t \ ({x : α | IsBot x} ∪ {x : α | IsTop x})).Countable
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∉ t) ∧ ∀ (x : α), IsTop x → x ∉ t
have refine_3 : Dense (t \ ({x : α | IsBot x} ∪ {x : α | IsTop x}))
Tactic: refine ⟨t \ ({ x | IsBot x } ∪ { x | IsTop x }), ?_, ?_, ?_, fun x hx => ?_, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.DenselyOrdered (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : Nontrivial α
s : Set α
inst_5 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
refine_1 : t \ ({x : α | IsBot x} ∪ {x : α | IsTop x}) ⊆ s
refine_2 : (t \ ({x : α | IsBot x} ∪ {x : α | IsTop x})).Countable
refine_3 : Dense (t \ ({x : α | IsBot x} ∪ {x : α | IsTop x}))
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∉ t) ∧ ∀ (x : α), IsTop x → x ∉ t
have refine_4 : ∀ (x : α) (hx : IsBot x), x ∉ t \ ({x : α | IsBot x} ∪ {x : α | IsTop x})
Tactic: refine ⟨t \ ({ x | IsBot x } ∪ { x | IsTop x }), ?_, ?_, ?_, fun x hx => ?_, fun x hx => ?_⟩