awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
⊢ Set.Countable.{u_1} (α := α) ({a : α | IsTop a} ∪ {a : α | ∃ (b : α), a ⋖ b})

Tactic:
exact (subsingleton_isTop α).countable.union countable_setOf_covBy_right

Premises used: Set.subsingleton_isTop, Set.Countable.union, countable_setOf_covBy_right, Set.Subsingleton.countable
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
⊢ Set.Countable.{u_1} (α := α) {x : α | 𝓝[<] x = ⊥}

Tactic:
countable_setOf_isolated_right (α := αᵒᵈ)

Premises used: countable_setOf_isolated_right, setOf, OrderDual, Set.Iio
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
H : t.Countable
x : α
hx : Membership.mem (γ := Set α) {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} x
pos : ∀ (h'x : IsTop x), x ∈ t ∪ {x : α | IsTop x}
neg : ∀ (h'x : ¬IsTop x), x ∈ t ∪ {x : α | IsTop x}
⊢ x ∈ t ∪ {x : α | IsTop x}

Tactic:
by_cases h'x : IsTop x

Premises used: IsTop
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
H : t.Countable
x : α
hx : Membership.mem (γ := Set α) {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} x
h'x : IsTop x
⊢ x ∈ t ∪ {x : α | IsTop x}

Tactic:
simp [h'x]
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
H : t.Countable
x : α
hx : Membership.mem (γ := Set α) {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} x
h'x : ¬IsTop x
⊢ x ∈ t ∪ {x : α | IsTop x}

Tactic:
simpa [-sep_and, t, h'x]

Premises used: Set.sep_and
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
H : t.Countable
⊢ {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ⊆ t ∪ {x : α | IsTop x}

Tactic:
have : { x ∈ s | 𝓝[s ∩ Ioi x] x = ⊥ } ⊆ t ∪ {x | IsTop x} := by
      intro x hx
      by_cases h'x : IsTop x
      · simp [h'x]
      · simpa [-sep_and, t, h'x]
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
H : t.Countable
this : {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ⊆ t ∪ {x : α | IsTop x}
apply : (t ∪ {x : α | IsTop x}).Countable
⊢ Set.Countable.{u_1} (α := α) {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}

Tactic:
apply Countable.mono this

Premises used: Set.Countable.mono
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
H : t.Countable
this : {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ⊆ t ∪ {x : α | IsTop x}
⊢ (t ∪ {x : α | IsTop x}).Countable

Tactic:
simp [H, (subsingleton_isTop α).countable]

Premises used: Set.subsingleton_isTop, Set.Subsingleton.countable
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
suffices : t.Countable
⊢ Set.Countable.{u_1} (α := α) {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}

Tactic:
suffices H : t.Countable by
    have : { x ∈ s | 𝓝[s ∩ Ioi x] x = ⊥ } ⊆ t ∪ {x | IsTop x} := by
      intro x hx
      by_cases h'x : IsTop x
      · simp [h'x]
      · simpa [-sep_and, t, h'x]
    apply Countable.mono this
    simp [H, (subsingleton_isTop α).countable]
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ t
⊢ x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ (x_1 : α), x < x_1

Tactic:
simp only [← empty_mem_iff_bot, mem_nhdsWithin_iff_exists_mem_nhds_inter,
      subset_empty_iff, IsTop, not_forall, not_le, mem_setOf_eq, t] at hx

Premises used: not_le, Set.mem_setOf_eq, Filter.empty_mem_iff_bot, Set.subset_empty_iff, IsTop, Classical.not_forall, mem_nhdsWithin_iff_exists_mem_nhds_inter
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ (x_1 : α), x < x_1
rcases : ∀ (u : Set α) (hu : u ∈ 𝓝 x) (h'u : u ∩ (s ∩ Ioi x) = ∅), ∃ y > x, s ∩ Ioo x y = ∅
⊢ ∃ y > x, s ∩ Ioo x y = ∅

Tactic:
rcases hx.2.1 with ⟨u, hu, h'u⟩

Premises used: And.right, And.left
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ (x_1 : α), x < x_1
u : Set α
hu : u ∈ 𝓝 x
h'u : u ∩ (s ∩ Ioi x) = ∅
⊢ ∃ (y : α), x < y ∧ Ico x y ⊆ u

Tactic:
exists_Ico_subset_of_mem_nhds hu hx.2.2

Premises used: And.right, exists_Ico_subset_of_mem_nhds
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ (x_1 : α), x < x_1
u : Set α
hu : u ∈ 𝓝 x
h'u : u ∩ (s ∩ Ioi x) = ∅
obtain : ∀ (y : α) (hxy : x < y) (hy : Ico x y ⊆ u), ∃ y > x, s ∩ Ioo x y = ∅
⊢ ∃ y > x, s ∩ Ioo x y = ∅

Tactic:
obtain ⟨y, hxy, hy⟩ : ∃ y, x < y ∧ Ico x y ⊆ u := exists_Ico_subset_of_mem_nhds hu hx.2.2

Premises used: And.right, exists_Ico_subset_of_mem_nhds
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ (x_1 : α), x < x_1
u : Set α
hu : u ∈ 𝓝 x
h'u : u ∩ (s ∩ Ioi x) = ∅
y : α
hxy : x < y
hy : Ico x y ⊆ u
⊢ ∃ y > x, s ∩ Ioo x y = ∅

Tactic:
⟨y, hxy, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ (x_1 : α), x < x_1
u : Set α
hu : u ∈ 𝓝 x
h'u : u ∩ (s ∩ Ioi x) = ∅
y : α
hxy : x < y
hy : Ico x y ⊆ u
refine : s ∩ Ioo x y = ∅
⊢ ∃ y > x, s ∩ Ioo x y = ∅

Tactic:
refine ⟨y, hxy, ?_⟩
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ (x_1 : α), x < x_1
u : Set α
hu : u ∈ 𝓝 x
h'u : u ∩ (s ∩ Ioi x) = ∅
y : α
hxy : x < y
hy : Ico x y ⊆ u
contrapose! : ∀ (h'u : (s ∩ Ioo x y).Nonempty), (u ∩ (s ∩ Ioi x)).Nonempty
⊢ s ∩ Ioo x y = ∅

Tactic:
contrapose! h'u
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ (x_1 : α), x < x_1
u : Set α
hu : u ∈ 𝓝 x
y : α
hxy : x < y
hy : Ico x y ⊆ u
h'u : (s ∩ Ioo x y).Nonempty
apply : s ∩ Ioo x y ⊆ u ∩ (s ∩ Ioi x)
⊢ (u ∩ (s ∩ Ioi x)).Nonempty

Tactic:
apply h'u.mono

Premises used: Set.Nonempty.mono
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ (x_1 : α), x < x_1
u : Set α
hu : u ∈ 𝓝 x
y : α
hxy : x < y
hy : Ico x y ⊆ u
h'u : (s ∩ Ioo x y).Nonempty
z : α
hz : z ∈ s ∩ Ioo x y
⊢ z ∈ u ∩ (s ∩ Ioi x)

Tactic:
⟨hy ⟨hz.2.1.le, hz.2.2⟩, hz.1, hz.2.1⟩

Premises used: Set.Mem, setOf, LT.lt.le, Set.inter, And.right, And.left, And.intro
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ (x_1 : α), x < x_1
u : Set α
hu : u ∈ 𝓝 x
y : α
hxy : x < y
hy : Ico x y ⊆ u
h'u : (s ∩ Ioo x y).Nonempty
z : α
hz : z ∈ s ∩ Ioo x y
⊢ z ∈ u ∩ (s ∩ Ioi x)

Tactic:
exact ⟨hy ⟨hz.2.1.le, hz.2.2⟩, hz.1, hz.2.1⟩
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
⊢ ∀ (x : α) (hx : x ∈ t), ∃ y > x, s ∩ Ioo x y = ∅

Tactic:
have (x) (hx : x ∈ t) : ∃ y > x, s ∩ Ioo x y = ∅ := by
    simp only [← empty_mem_iff_bot, mem_nhdsWithin_iff_exists_mem_nhds_inter,
      subset_empty_iff, IsTop, not_forall, not_le, mem_setOf_eq, t] at hx
    rcases hx.2.1 with ⟨u, hu, h'u⟩
    obtain ⟨y, hxy, hy⟩ : ∃ y, x < y ∧ Ico x y ⊆ u := exists_Ico_subset_of_mem_nhds hu hx.2.2
    refine ⟨y, hxy, ?_⟩
    contrapose! h'u
    apply h'u.mono
    intro z hz
    exact ⟨hy ⟨hz.2.1.le, hz.2.2⟩, hz.1, hz.2.1⟩
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
this : ∀ (x : α) (hx : x ∈ t), ∃ y > x, s ∩ Ioo x y = ∅
choose! :
  ∀ (y : (x : α) → α) (hy : ∀ (x : α) (hx : x ∈ t), y x > x) (h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅),
    t.Countable
⊢ t.Countable

Tactic:
choose! y hy h'y using this
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
apply : t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioo x (y x)
⊢ t.Countable

Tactic:
apply Set.PairwiseDisjoint.countable_of_Ioo (y := y) _ hy

Premises used: Set.PairwiseDisjoint.countable_of_Ioo
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
inr :
  ∀ (h : ∀ ⦃a : α⦄ (ha : a ∈ t) ⦃b : α⦄ (hb : b ∈ t) (hab : a ≠ b) (H : a < b), Disjoint (Ioo a (y a)) (Ioo b (y b)))
    (H : b ≤ a), Disjoint (Ioo a (y a)) (Ioo b (y b))
wlog! : ∀ ⦃a : α⦄ (ha : a ∈ t) ⦃b : α⦄ (hb : b ∈ t) (hab : a ≠ b) (H : a < b), Disjoint (Ioo a (y a)) (Ioo b (y b))
⊢ Disjoint (Ioo a (y a)) (Ioo b (y b))

Tactic:
wlog! H : a < b generalizing a b with h
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
h : ∀ ⦃a : α⦄ (ha : a ∈ t) ⦃b : α⦄ (hb : b ∈ t) (hab : a ≠ b) (H : a < b), Disjoint (Ioo a (y a)) (Ioo b (y b))
H : b ≤ a
⊢ b < a

Tactic:
have : b < a := lt_of_le_of_ne H hab.symm
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
h : ∀ ⦃a : α⦄ (ha : a ∈ t) ⦃b : α⦄ (hb : b ∈ t) (hab : a ≠ b) (H : a < b), Disjoint (Ioo a (y a)) (Ioo b (y b))
H : b ≤ a
this : b < a
⊢ Disjoint (Ioo a (y a)) (Ioo b (y b))

Tactic:
(h hb ha hab.symm this).symm

Premises used: Ne.symm, Disjoint.symm
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
h : ∀ ⦃a : α⦄ (ha : a ∈ t) ⦃b : α⦄ (hb : b ∈ t) (hab : a ≠ b) (H : a < b), Disjoint (Ioo a (y a)) (Ioo b (y b))
H : b ≤ a
this : b < a
⊢ Disjoint (Ioo a (y a)) (Ioo b (y b))

Tactic:
exact (h hb ha hab.symm this).symm

Premises used: Ne.symm, Disjoint.symm
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
H : a < b
by_contra! : ∀ (this : b < y a), False
⊢ y a ≤ b

Tactic:
by_contra!
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
H : a < b
this : b < y a
⊢ b ∈ s ∩ Ioo a (y a)

Tactic:
simp [hb.1, H, this]

Premises used: And.left
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
H : a < b
this : b < y a
⊢ b ∈ s ∩ Ioo a (y a)

Tactic:
have : b ∈ s ∩ Ioo a (y a) := by simp [hb.1, H, this]
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
H : a < b
this_1 : b < y a
this : b ∈ s ∩ Ioo a (y a)
⊢ False

Tactic:
simp [h'y a ha] at this
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
H : a < b
⊢ y a ≤ b

Tactic:
have : y a ≤ b := by
    by_contra!
    have : b ∈ s ∩ Ioo a (y a) := by simp [hb.1, H, this]
    simp [h'y a ha] at this
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
H : a < b
this : y a ≤ b
rw : ∀ ⦃a_1 : α⦄, a_1 ∈ Ioo a (y a) → ∀ ⦃b_1 : α⦄, b_1 ∈ Ioo b (y b) → a_1 ≠ b_1
⊢ Disjoint (Ioo a (y a)) (Ioo b (y b))

Tactic:
rw [disjoint_iff_forall_ne]

Premises used: Set.disjoint_iff_forall_ne
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
H : a < b
this : y a ≤ b
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ Ioo a (y a) → ∀ ⦃b_1 : α⦄, b_1 ∈ Ioo b (y b) → a_1 ≠ b_1

Tactic:
fun u hu v hv ↦ ((hu.2.trans_le this).trans hv.1).ne

Premises used: And.right, And.left, LT.lt.trans_le, LT.lt.trans, LT.lt.ne
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
H : a < b
this : y a ≤ b
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ Ioo a (y a) → ∀ ⦃b_1 : α⦄, b_1 ∈ Ioo b (y b) → a_1 ≠ b_1

Tactic:
exact fun u hu v hv ↦ ((hu.2.trans_le this).trans hv.1).ne
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
⊢ Set.Countable.{u_1} (α := α) {x : α | x ∈ s ∧ 𝓝[s ∩ Iio x] x = ⊥}

Tactic:
countable_setOf_isolated_right_within (α := αᵒᵈ)

Premises used: Set.Mem, setOf, OrderDual, Set.Iio, countable_setOf_isolated_right_within
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
inst_4 : DenselyOrdered α
a : α
s : Set α
rw : (∃ u ∈ Ioi a, Ioo a u ⊆ s) ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s
⊢ s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s

Tactic:
rw [mem_nhdsGT_iff_exists_Ioo_subset]

Premises used: mem_nhdsGT_iff_exists_Ioo_subset
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
inst_4 : DenselyOrdered α
a : α
s : Set α
mp : (∃ u ∈ Ioi a, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioc a u ⊆ s
mpr : (∃ u ∈ Ioi a, Ioc a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s
⊢ (∃ u ∈ Ioi a, Ioo a u ⊆ s) ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s

Tactic:
constructor
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
inst_4 : DenselyOrdered α
a : α
s : Set α
u : α
au : u ∈ Ioi a
as : Ioo a u ⊆ s
mp : ∀ (v : α) (hv : a < v ∧ v < u), ∃ u ∈ Ioi a, Ioc a u ⊆ s
⊢ ∃ u ∈ Ioi a, Ioc a u ⊆ s

Tactic:
rcases exists_between au with ⟨v, hv⟩

Premises used: exists_between
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
inst_4 : DenselyOrdered α
a : α
s : Set α
u : α
au : u ∈ Ioi a
as : Ioo a u ⊆ s
v : α
hv : a < v ∧ v < u
⊢ ∃ u ∈ Ioi a, Ioc a u ⊆ s

Tactic:
⟨v, hv.1, fun x hx => as ⟨hx.1, lt_of_le_of_lt hx.2 hv.2⟩⟩

Premises used: lt_of_le_of_lt, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
inst_4 : DenselyOrdered α
a : α
s : Set α
u : α
au : u ∈ Ioi a
as : Ioo a u ⊆ s
v : α
hv : a < v ∧ v < u
⊢ ∃ u ∈ Ioi a, Ioc a u ⊆ s

Tactic:
exact ⟨v, hv.1, fun x hx => as ⟨hx.1, lt_of_le_of_lt hx.2 hv.2⟩⟩
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
inst_4 : DenselyOrdered α
a : α
s : Set α
u : α
au : u ∈ Ioi a
as : Ioc a u ⊆ s
⊢ ∃ u ∈ Ioi a, Ioo a u ⊆ s

Tactic:
⟨u, au, Subset.trans Ioo_subset_Ioc_self as⟩

Premises used: Set.Subset.trans, Set.Ioo_subset_Ioc_self, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
inst_4 : DenselyOrdered α
a : α
s : Set α
u : α
au : u ∈ Ioi a
as : Ioc a u ⊆ s
⊢ ∃ u ∈ Ioi a, Ioo a u ⊆ s

Tactic:
exact ⟨u, au, Subset.trans Ioo_subset_Ioc_self as⟩
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
h : a < b
s : Set α
⊢ [s ∈ 𝓝[<] b, s ∈ 𝓝[Ico a b] b, s ∈ 𝓝[Ioo a b] b, ∃ l ∈ Ico a b, Ioo l b ⊆ s, ∃ l ∈ Iio b, Ioo l b ⊆ s].TFAE

Tactic:
simpa using TFAE_mem_nhdsGT h.dual (ofDual ⁻¹' s)

Premises used: OrderDual.ofDual, TFAE_mem_nhdsGT, Set.preimage, LT.lt.dual, DFunLike.coe
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a l' : α
s : Set α
hl' : l' < a
⊢ s ∈ 𝓝[<] a ↔ ∃ l ∈ Ico l' a, Ioo l a ⊆ s

Tactic:
(TFAE_mem_nhdsLT hl' s).out 0 3

Premises used: List.TFAE.out, TFAE_mem_nhdsLT, OfNat.ofNat
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a l' : α
s : Set α
hl' : l' < a
⊢ s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ioo l a ⊆ s

Tactic:
(TFAE_mem_nhdsLT hl' s).out 0 4

Premises used: List.TFAE.out, TFAE_mem_nhdsLT, OfNat.ofNat
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMinOrder α
a : α
s : Set α
⊢ s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ioo l a ⊆ s

Tactic:
let ⟨_, h⟩ := exists_lt a
  mem_nhdsLT_iff_exists_Ioo_subset' h

Premises used: _private.0.mem_nhdsLT_iff_exists_Ioo_subset.match_1, nhdsWithin, Membership.mem, Exists, HasSubset.Subset, mem_nhdsLT_iff_exists_Ioo_subset', And, Iff, NoMinOrder.exists_lt, Set.Iio, Set.Ioo
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMinOrder α
inst_4 : DenselyOrdered α
a : α
s : Set α
⊢ Membership.mem (γ := Filter αᵒᵈ) (𝓝[>] (toDual : (a : α) → αᵒᵈ) a : Filter αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ↔
    ∃ (u : αᵒᵈ),
      Membership.mem (γ := Set αᵒᵈ) (Ioi ((toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ) u ∧
        Subset (α := Set αᵒᵈ) (Ioc ((toDual : (a : α) → αᵒᵈ) a) u : Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s : Set αᵒᵈ)

Tactic:
have : ofDual ⁻¹' s ∈ 𝓝[>] toDual a ↔ _ := mem_nhdsGT_iff_exists_Ioc_subset