awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[≤] a
hbs : Icc b a ⊆ s
c : α
hac : a ≤ c
hc_nhds : Icc a c ∈ 𝓝[≥] a
hcs : Icc a c ⊆ s
⊢ ∃ (b : α) (c : α), a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
have refine : Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
Tactic: refine ⟨b, c, ⟨hba, hac⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[≤] a
hbs : Icc b a ⊆ s
c : α
hac : a ≤ c
hc_nhds : Icc a c ∈ 𝓝[≥] a
hcs : Icc a c ⊆ s
⊢ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
have rw : Icc b a ∪ Icc a c ∈ 𝓝[≤] a ⊔ 𝓝[≥] a ∧ Icc b a ∪ Icc a c ⊆ s
Tactic: rw [← Icc_union_Icc_eq_Icc hba hac, ← nhdsLE_sup_nhdsGE]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
hs : IsOpen[inst] s
h : s.Nonempty
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
have obtain : ∀ (x : α) (hx : x ∈ s), ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
Tactic: obtain ⟨x, hx⟩ : ∃ x, x ∈ s := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : Nontrivial α
s : Set α
hs : IsOpen[inst] s
x : α
hx : x ∈ s
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
have obtain : ∀ (y : α) (hy : y ≠ x), ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
Tactic: obtain ⟨y, hy⟩ : ∃ y, y ≠ x := exists_ne x
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
have inl : ∀ (H : x < y), ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
Tactic: rcases lt_trichotomy x y with (H | rfl | H)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
have inr : ∀ (hy : x ≠ x), ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
Tactic: rcases lt_trichotomy x y with (H | rfl | H)
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
have inr₁ : ∀ (H : y < x), ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
Tactic: rcases lt_trichotomy x y with (H | rfl | H)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
have inl : ∀ (u : α) (xu : x < u) (hu : Ico x u ⊆ 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⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ ∃ (a : α) (b : α), a < b ∧ Ioo a b ⊆ s
have inr : ∀ (l : α) (lx : l < x) (hl : Ioc l x ⊆ 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⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
have refine : ∀ (U : Set α) (U_open : IsOpen[inst] U) (U_nonempty : U.Nonempty), (U ∩ s).Nonempty
Tactic: refine dense_iff_inter_open.2 fun U U_open U_nonempty => ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ (U ∩ s).Nonempty
have obtain : ∀ (a b : α) (hab : a < b) (H : Ioo a b ⊆ U), (U ∩ s).Nonempty
Tactic: obtain ⟨a, b, hab, H⟩ : ∃ a b : α, a < b ∧ Ioo a b ⊆ U := U_open.exists_Ioo_subset U_nonempty
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ (U ∩ s).Nonempty
have obtain : ∀ (x : α) (xs : x ∈ s) (hx : a < x ∧ x < b), (U ∩ s).Nonempty
Tactic: obtain ⟨x, xs, hx⟩ : ∃ x ∈ s, a < x ∧ x < b := h hab
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : WellFoundedLT α
s : Set α
h : IsUpperSet s
⊢ IsClosed[inst] s
have inl : ∀ (h : IsUpperSet.{u} (α := α) ∅), IsClosed[inst] ∅
Tactic: obtain rfl | ⟨a, rfl⟩ := h.eq_empty_or_Ici
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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] ∅
⊢ IsClosed[inst] s
have inr : ∀ (a : α) (h : IsUpperSet (Ici a)), IsClosed[inst] (Ici a)
Tactic: obtain rfl | ⟨a, rfl⟩ := h.eq_empty_or_Ici
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hl : ∃ (l : α), l < a
hu : ∃ (u : α), a < u
⊢ s ∈ 𝓝 a ↔ ∃ (l : α) (u : α), a ∈ Ioo l u ∧ Ioo l u ⊆ s
have mp : s ∈ 𝓝 a → ∃ (l : α) (u : α), a ∈ Ioo l u ∧ Ioo l u ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ s ∈ 𝓝 a ↔ ∃ (l : α) (u : α), a ∈ Ioo l u ∧ Ioo l u ⊆ s
have mpr : (∃ (l : α) (u : α), a ∈ Ioo l u ∧ Ioo l u ⊆ s) → s ∈ 𝓝 a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ ∃ (l : α) (u : α), a ∈ Ioo l u ∧ Ioo l u ⊆ s
have mp : ∀ (u : α) (au : a < u) (hu : Ico a 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⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ ∃ (l : α) (u : α), a ∈ Ioo l u ∧ Ioo l u ⊆ s
have mp : ∀ (l : α) (la : l < a) (hl : Ioc l a ⊆ 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⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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)
have refine : Preorder.topology α = generateFrom (Ioi '' s ∪ Iio '' s)
Tactic: refine (OrderTopology.topology_eq_generate_intervals (α := α)).trans ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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)
have refine_1 : Ioi '' s ∪ Iio '' s ⊆ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
Tactic: refine le_antisymm (generateFrom_anti ?_) (le_generateFrom ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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}
⊢ Preorder.topology α = generateFrom (Ioi '' s ∪ Iio '' s)
have 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
Tactic: refine le_antisymm (generateFrom_anti ?_) (le_generateFrom ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
⊢ Ioi '' s ∪ Iio '' s ⊆ {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
have refine_1 : s ⊆ Ioi ⁻¹' {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} ∧ s ⊆ Iio ⁻¹' {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
Tactic: simp only [union_subset_iff, image_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
a : α
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (Ioi a)
have refine_2 : IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (⋃ y ∈ s ∩ Ioi a, Ioi y)
Tactic: rw [hs.Ioi_eq_biUnion]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
hs : Dense s
a : α
⊢ IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (Iio a)
have refine_2 : IsOpen[generateFrom (Ioi '' s ∪ Iio '' s)] (⋃ y ∈ s ∩ Iio a, Iio y)
Tactic: rw [hs.Iio_eq_biUnion]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
inst_4 : SeparableSpace α
⊢ SecondCountableTopology α
have rcases : ∀ (s : Set α) (hc : s.Countable) (hd : Dense s), SecondCountableTopology α
Tactic: rcases exists_countable_dense α with ⟨s, hc, hd⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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 α
have refine : (Ioi '' s ∪ Iio '' s).Countable
Tactic: refine ⟨⟨_, ?_, hd.topology_eq_generateFrom⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
⊢ Set.Countable.{u} (α := α) {x : α | ∃ (y : α), x ⋖ y}
have a : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
⊢ Set.Countable.{u} (α := α) {x : α | ∃ (y : α), x ⋖ y}
have this : ∀ x ∈ s, ∃ (y : α), x ⋖ y
Tactic: have : ∀ x ∈ s, ∃ y, x ⋖ y := fun x => id
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ Set.Countable.{u} (α := α) {x : α | ∃ (y : α), x ⋖ y}
have choose! : ∀ (y : (x : α) → α) (hy : ∀ x ∈ s, x ⋖ y x), Set.Countable.{u} (α := α) {x : α | ∃ (y : α), x ⋖ y}
Tactic: choose! y hy using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
⊢ Set.Countable.{u} (α := α) {x : α | ∃ (y : α), x ⋖ y}
have Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
Tactic: have Hy : ∀ x z, x ∈ s → z < y x → z ≤ x := fun x z hx => (hy x hx).le_of_lt
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen[inst] a → Set.Countable.{u} (α := α) {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a}
x : α
hx : x ∈ s
⊢ Membership.mem (γ := Set α) (⋃ a ∈ countableBasis α, {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a}) x
have rcases : ∀ (a : Set α) (ab : a ∈ countableBasis α) (xa : x ∈ a) (ya : y x ∉ a),
  Membership.mem (γ := Set α) (⋃ a ∈ countableBasis α, {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a}) x
Tactic: rcases (isBasis_countableBasis α).exists_mem_of_ne (hy x hx).ne with ⟨a, ab, xa, ya⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen[inst] a → Set.Countable.{u} (α := α) {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a}
⊢ Set.Countable.{u} (α := α) {x : α | ∃ (y : α), x ⋖ y}
have this : s ⊆ ⋃ a ∈ countableBasis α, {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a}
Tactic: have : s ⊆ ⋃ a ∈ countableBasis α, { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a } := fun x hx => by
      rcases (isBasis_countableBasis α).exists_mem_of_ne (hy x hx).ne with ⟨a, ab, xa, ya⟩
      exact mem_iUnion₂.2 ⟨a, ab, hx, xa, ya⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen[inst] a → Set.Countable.{u} (α := α) {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a}
this : s ⊆ ⋃ a ∈ countableBasis α, {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a}
⊢ Set.Countable.{u} (α := α) {x : α | ∃ (y : α), x ⋖ y}
have refine : Set.Countable.{u} (α := α) (⋃ a ∈ countableBasis α, {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a})
Tactic: refine Set.Countable.mono this ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
H : ∀ (a : Set α), IsOpen[inst] a → Set.Countable.{u} (α := α) {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a}
this : s ⊆ ⋃ a ∈ countableBasis α, {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a}
⊢ Set.Countable.{u} (α := α) (⋃ a ∈ countableBasis α, {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a})
have refine : ∀ (a : Set α) (ha : a ∈ countableBasis α), IsOpen[inst] a
Tactic: refine Countable.biUnion (countable_countableBasis α) fun a ha => H _ ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
⊢ Set.Countable.{u} (α := α) {x : α | ∃ (y : α), x ⋖ y}
have suffices : ∀ (a : Set α), IsOpen[inst] a → Set.Countable.{u} (α := α) {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a}
Tactic: suffices H : ∀ a : Set α, IsOpen a → Set.Countable { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a } by
    have : s ⊆ ⋃ a ∈ countableBasis α, { x | x ∈ s ∧ x ∈ a ∧ y x ∉ a } := fun x hx => by
      rcases (isBasis_countableBasis α).exists_mem_of_ne (hy x hx).ne with ⟨a, ab, xa, ya⟩
      exact mem_iUnion₂.2 ⟨a, ab, hx, xa, ya⟩
    refine Set.Countable.mono this ?_
    refine Countable.biUnion (countable_countableBasis α) fun a ha => H _ ?_
    exact isOpen_of_mem_countableBasis ha
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
⊢ Set.Countable.{u} (α := α) {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a}
have suffices : Set.Countable.{u} (α := α) {x : α | (x ∈ s ∧ x ∈ a ∧ y x ∉ a) ∧ ¬IsBot x}
Tactic: suffices H : Set.Countable { x | (x ∈ s ∧ x ∈ a ∧ y x ∉ a) ∧ ¬IsBot x } from
    H.of_diff (subsingleton_isBot α).countable
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
⊢ Set.Countable.{u} (α := α) {x : α | (x ∈ s ∧ x ∈ a ∧ y x ∉ a) ∧ ¬IsBot x}
have simp : Set.Countable.{u} (α := α) {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
Tactic: simp only [and_assoc]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
t : Set α := {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
x : α
hx : x ∈ t
⊢ ∃ z < x, Ioc z x ⊆ a
have apply : ∃ (l : α), l < x
Tactic: apply exists_Ioc_subset_of_mem_nhds (ha.mem_nhds hx.2.1)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
t : Set α := {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
⊢ Set.Countable.{u} (α := α) {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
have this : ∀ x ∈ t, ∃ z < x, Ioc z x ⊆ a
Tactic: have : ∀ x ∈ t, ∃ z < x, Ioc z x ⊆ a := by
    intro x hx
    apply exists_Ioc_subset_of_mem_nhds (ha.mem_nhds hx.2.1)
    simpa only [IsBot, not_forall, not_le] using hx.right.right.right
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
t : Set α := {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
this : ∀ x ∈ t, ∃ z < x, Ioc z x ⊆ a
⊢ Set.Countable.{u} (α := α) {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
have choose! : ∀ (z : (x : α) → α) (hz : ∀ x ∈ t, z x < x) (h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a),
  Set.Countable.{u} (α := α) {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
Tactic: choose! z hz h'z using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
t : Set α := {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : (x : α) → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
⊢ onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioc (z x) x) x x'
have inl : ∀ (h' : x < x'), onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioc (z x) x) x x'
Tactic: rcases hxx'.lt_or_gt with (h' | h')
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
t : Set α := {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : (x : α) → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
inl : ∀ (h' : x < x'), onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioc (z x) x) x x'
⊢ onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioc (z x) x) x x'
have inr : ∀ (h' : x' < x), onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioc (z x) x) x x'
Tactic: rcases hxx'.lt_or_gt with (h' | h')
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
t : Set α := {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : (x : α) → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x < x'
⊢ onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioc (z x) x) x x'
have inl : ∀ (u : α) (ux : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioc (z x) x) x) u)
  (ux' : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioc (z x) x) x') u), y x ∈ a
Tactic: refine disjoint_left.2 fun u ux ux' => xt.2.2.1 ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
t : Set α := {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : (x : α) → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x < x'
u : α
ux : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioc (z x) x) x) u
ux' : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioc (z x) x) x') u
⊢ y x ∈ a
have inl : y x ≤ x'
Tactic: refine h'z x' x't ⟨ux'.1.trans_le (ux.2.trans (hy x xt.1).le), ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
t : Set α := {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : (x : α) → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x < x'
u : α
ux : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioc (z x) x) x) u
ux' : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioc (z x) x) x') u
⊢ y x ≤ x'
have inl : ∀ (H : x' < y x), False
Tactic: by_contra! H