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 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
⊢ ∀ (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
-- 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}
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
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
⊢ 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⟩

Premises used: CovBy.ne, TopologicalSpace.IsTopologicalBasis.exists_mem_of_ne, TopologicalSpace.isBasis_countableBasis
-- 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}
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
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:
mem_iUnion₂.2 ⟨a, ab, hx, xa, ya⟩

Premises used: Iff.mpr, Set.mem_iUnion₂, And.intro, Exists.intro
-- 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}
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
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:
exact mem_iUnion₂.2 ⟨a, ab, hx, xa, ya⟩
-- 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}
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}
⊢ 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⟩
-- 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}
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}

Tactic:
Set.Countable.mono this ?_

Premises used: Set.Countable.mono
-- 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}
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}
refine : Set.Countable.{u} (α := α) (⋃ a ∈ countableBasis α, {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a})
⊢ Set.Countable.{u} (α := α) {x : α | ∃ (y : α), x ⋖ y}

Tactic:
refine Set.Countable.mono this ?_

Premises used: Set.Countable.mono
-- 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}
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})

Tactic:
Countable.biUnion (countable_countableBasis α) fun a ha => H _ ?_

Premises used: TopologicalSpace.countable_countableBasis, Set.Countable.biUnion
-- 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}
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}
refine : ∀ (a : Set α) (ha : a ∈ countableBasis α), IsOpen[inst] a
⊢ Set.Countable.{u} (α := α) (⋃ a ∈ countableBasis α, {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a})

Tactic:
refine Countable.biUnion (countable_countableBasis α) fun a ha => H _ ?_

Premises used: TopologicalSpace.countable_countableBasis, Set.Countable.biUnion
-- 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}
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}
a : Set α
ha : a ∈ countableBasis α
⊢ IsOpen[inst] a

Tactic:
isOpen_of_mem_countableBasis ha

Premises used: TopologicalSpace.isOpen_of_mem_countableBasis
-- 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}
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}
a : Set α
ha : a ∈ countableBasis α
⊢ IsOpen[inst] a

Tactic:
exact isOpen_of_mem_countableBasis ha

Premises used: TopologicalSpace.isOpen_of_mem_countableBasis
-- 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}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
suffices : ∀ (a : Set α), IsOpen[inst] a → Set.Countable.{u} (α := α) {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a}
⊢ Set.Countable.{u} (α := α) {x : α | ∃ (y : α), x ⋖ y}

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
-- 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}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
suffices : Set.Countable.{u} (α := α) {x : α | (x ∈ s ∧ x ∈ a ∧ y x ∉ a) ∧ ¬IsBot x}
⊢ Set.Countable.{u} (α := α) {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a}

Tactic:
suffices H : Set.Countable { x | (x ∈ s ∧ x ∈ a ∧ y x ∉ a) ∧ ¬IsBot x } from
    H.of_diff (subsingleton_isBot α).countable
-- 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}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
simp : Set.Countable.{u} (α := α) {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
⊢ Set.Countable.{u} (α := α) {x : α | (x ∈ s ∧ x ∈ a ∧ y x ∉ a) ∧ ¬IsBot x}

Tactic:
simp only [and_assoc]

Premises used: and_assoc
-- 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}
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
apply : ∃ (l : α), l < x
⊢ ∃ z < x, Ioc z x ⊆ a

Tactic:
apply exists_Ioc_subset_of_mem_nhds (ha.mem_nhds hx.2.1)

Premises used: exists_Ioc_subset_of_mem_nhds, And.right, And.left, IsOpen.mem_nhds
-- 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}
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
⊢ ∃ (l : α), l < x

Tactic:
simpa only [IsBot, not_forall, not_le] using hx.right.right.right

Premises used: not_le, IsBot, And.right, Classical.not_forall
-- 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}
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 ∈ 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
-- 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}
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
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}
⊢ Set.Countable.{u} (α := α) {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}

Tactic:
choose! z hz h'z using this
-- 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}
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'
inr : ∀ (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'

Tactic:
rcases hxx'.lt_or_gt with (h' | h')

Premises used: Ne.lt_or_gt
-- 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}
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'

Tactic:
disjoint_left.2 fun u ux ux' => xt.2.2.1 ?_

Premises used: Iff.mpr, Set.disjoint_left, And.right, And.left
-- 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}
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'
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
⊢ onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioc (z x) x) x x'

Tactic:
refine disjoint_left.2 fun u ux ux' => xt.2.2.1 ?_

Premises used: Iff.mpr, Set.disjoint_left, And.right, And.left
-- 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}
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

Tactic:
h'z x' x't ⟨ux'.1.trans_le (ux.2.trans (hy x xt.1).le), ?_⟩

Premises used: And.right, And.left, LT.lt.trans_le, And.intro, LE.le.trans, CovBy.le
-- 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}
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
inl : y x ≤ x'
⊢ y x ∈ a

Tactic:
refine h'z x' x't ⟨ux'.1.trans_le (ux.2.trans (hy x xt.1).le), ?_⟩

Premises used: And.right, And.left, LT.lt.trans_le, And.intro, LE.le.trans, CovBy.le
-- 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}
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
inl : ∀ (H : x' < y x), False
⊢ y x ≤ x'

Tactic:
by_contra! H
-- 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}
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
H : x' < y x
⊢ False

Tactic:
lt_irrefl _ ((Hy _ _ xt.1 H).trans_lt h')

Premises used: lt_irrefl, And.left, LE.le.trans_lt
-- 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}
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
H : x' < y x
⊢ False

Tactic:
exact lt_irrefl _ ((Hy _ _ xt.1 H).trans_lt h')

Premises used: lt_irrefl, And.left, LE.le.trans_lt
-- 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}
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'

Tactic:
disjoint_left.2 fun u ux ux' => x't.2.2.1 ?_

Premises used: Iff.mpr, Set.disjoint_left, And.right, And.left
-- 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}
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
inr :
  ∀ (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
⊢ onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioc (z x) x) x x'

Tactic:
refine disjoint_left.2 fun u ux ux' => x't.2.2.1 ?_

Premises used: Iff.mpr, Set.disjoint_left, And.right, And.left
-- 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}
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

Tactic:
h'z x xt ⟨ux.1.trans_le (ux'.2.trans (hy x' x't.1).le), ?_⟩

Premises used: And.right, And.left, LT.lt.trans_le, And.intro, LE.le.trans, CovBy.le
-- 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}
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
inr : y x' ≤ x
⊢ y x' ∈ a

Tactic:
refine h'z x xt ⟨ux.1.trans_le (ux'.2.trans (hy x' x't.1).le), ?_⟩

Premises used: And.right, And.left, LT.lt.trans_le, And.intro, LE.le.trans, CovBy.le
-- 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}
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
inr : ∀ (H : x < y x'), False
⊢ y x' ≤ x

Tactic:
by_contra! H
-- 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}
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
H : x < y x'
⊢ False

Tactic:
lt_irrefl _ ((Hy _ _ x't.1 H).trans_lt h')

Premises used: lt_irrefl, And.left, LE.le.trans_lt
-- 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}
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
H : x < y x'
⊢ False

Tactic:
exact lt_irrefl _ ((Hy _ _ x't.1 H).trans_lt h')

Premises used: lt_irrefl, And.left, LE.le.trans_lt