awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
u : Set α
⊢ IsOpen[instTopologicalSpace] ((⇑ofScott : (a : WithScott α) → α) ⁻¹' u) ↔ IsUpperSet u ∧ TopologicalSpace.IsOpen u

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, IsUpperSet, Set.inter, Topology.WithScott, Set.preimage, IsOpen
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
⊢ scottHausdorff α univ ≤ lower α

Tactic:
let : TopologicalSpace α := scottHausdorff α univ
  fun s h ↦ IsScottHausdorff.isOpen_of_isLowerSet isLowerSet_univ <|
    @IsLower.isLowerSet_of_isOpen (Topology.WithLower α) _ _ _ s h

Premises used: Topology.IsScottHausdorff.isOpen_of_isLowerSet, isLowerSet_univ, Set.univ, Topology.scottHausdorff, Topology.IsLower.isLowerSet_of_isOpen
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
rw : scottHausdorff α univ ≤ upperSet α ⊔ scottHausdorff α univ
⊢ scottHausdorff α univ ≤ inst_1

Tactic:
rw [IsScott.topology_eq α univ, scott]

Premises used: Topology.IsScott.topology_eq, Set.univ, Topology.scott
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
⊢ scottHausdorff α univ ≤ upperSet α ⊔ scottHausdorff α univ

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
⊢ scottHausdorff α univ ≤ upperSet α ⊔ scottHausdorff α univ

Tactic:
exact le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
rw : scottHausdorff α univ ≤ lower α
⊢ scottHausdorff α univ ≤ inst_1

Tactic:
rw [IsLower.topology_eq α]

Premises used: Topology.IsLower.topology_eq
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
⊢ scottHausdorff α univ ≤ lower α

Tactic:
scottHausdorff_le_lower

Premises used: Topology.scottHausdorff_le_lower
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
⊢ scottHausdorff α univ ≤ lower α

Tactic:
exact scottHausdorff_le_lower

Premises used: Topology.scottHausdorff_le_lower
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
ha : ¬IsSuccPrelimit a
obtain : ∀ (b : α) (hb : b ⋖ a), IsOpen[inst_1] {a}
⊢ IsOpen[inst_1] {a}

Tactic:
obtain ⟨b, hb⟩ := not_isSuccPrelimit_iff.1 ha

Premises used: Iff.mp, Order.not_isSuccPrelimit_iff
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
pos : ∀ (ha' : IsMax a), IsOpen[inst_1] {a}
neg : ∀ (ha' : ¬IsMax a), IsOpen[inst_1] {a}
⊢ IsOpen[inst_1] {a}

Tactic:
by_cases ha' : IsMax a

Premises used: IsMax
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : IsMax a
⊢ IsOpen[inst_1] (Set.Ioi b)

Tactic:
isOpen_Ioi (a := b)

Premises used: isOpen_Ioi
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : IsMax a
h : {a} = Set.Ioi b
⊢ IsOpen[inst_1] {a}

Tactic:
convert! isOpen_Ioi (a := b) using 1

Premises used: isOpen_Ioi
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : IsMax a
h : {a} = Set.Ici a
⊢ {a} = Set.Ioi b

Tactic:
rw [hb.Ioi_eq]

Premises used: CovBy.Ioi_eq
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : IsMax a
⊢ {a} = Set.Ici a

Tactic:
grind [IsMax]

Premises used: IsMax
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : ¬IsMax a
⊢ IsOpen[inst_1] (Set.Ioo b (Order.succ a))

Tactic:
isOpen_Ioo (a := b) (b := Order.succ a)

Premises used: isOpen_Ioo
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : ¬IsMax a
h : {a} = Set.Ioo b (Order.succ a)
⊢ IsOpen[inst_1] {a}

Tactic:
convert! isOpen_Ioo (a := b) (b := Order.succ a) using 1

Premises used: isOpen_Ioo
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : ¬IsMax a
⊢ {a} = Set.Ioo b (Order.succ a)

Tactic:
simp [(covBy_succ_of_not_isMax ha').Ioo_eq_Ioc, hb.Ioc_eq]

Premises used: CovBy.Ioc_eq, Order.covBy_succ_of_not_isMax, CovBy.Ioo_eq_Ioc
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
⊢ Nontrivial α

Tactic:
nontriviality α
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h : Nontrivial α
⊢ IsOpen[inst_1] {a} ↔ ¬IsSuccLimit a

Tactic:
⟨fun h ha ↦ ?_, fun ha ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h : Nontrivial α
refine_1 : ∀ (h : IsOpen[inst_1] {a}) (ha : IsSuccLimit a), False
refine_2 : ∀ (ha : ¬IsSuccLimit a), IsOpen[inst_1] {a}
⊢ IsOpen[inst_1] {a} ↔ ¬IsSuccLimit a

Tactic:
refine ⟨fun h ha ↦ ?_, fun ha ↦ ?_⟩
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h_1 : Nontrivial α
h : IsOpen[inst_1] {a}
ha : IsSuccLimit a
⊢ ∃ (l : α), l < a

Tactic:
simpa using ha.not_isMin

Premises used: Order.IsSuccLimit.not_isMin
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h_1 : Nontrivial α
h : IsOpen[inst_1] {a}
ha : IsSuccLimit a
⊢ ∃ (u : α), a < u

Tactic:
simpa only [not_isMax_iff] using not_isMax a

Premises used: not_isMax, not_isMax_iff
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h_1 : Nontrivial α
h : IsOpen[inst_1] {a}
ha : IsSuccLimit a
refine_1 : ∀ (l u : α) (h₁ : a ∈ Set.Ioo l u) (h₂ : Set.Ioo l u ⊆ {a}), False
⊢ False

Tactic:
obtain ⟨l, u, h₁, h₂⟩ := mem_nhds_iff_exists_Ioo_subset' (by simpa using ha.not_isMin)
      (by simpa only [not_isMax_iff] using not_isMax a) |>.mp (h.mem_nhds (Set.mem_singleton a))

Premises used: Set.mem_singleton, IsOpen.mem_nhds, Iff.mp, mem_nhds_iff_exists_Ioo_subset'
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h_1 : Nontrivial α
h : IsOpen[inst_1] {a}
ha : IsSuccLimit a
l u : α
h₁ : a ∈ Set.Ioo l u
h₂ : Set.Ioo l u ⊆ {a}
⊢ False

Tactic:
ha.isSuccPrelimit l ?_

Premises used: Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h_1 : Nontrivial α
h : IsOpen[inst_1] {a}
ha : IsSuccLimit a
l u : α
h₁ : a ∈ Set.Ioo l u
h₂ : Set.Ioo l u ⊆ {a}
refine_1 : l ⋖ a
⊢ False

Tactic:
refine ha.isSuccPrelimit l ?_

Premises used: Order.IsSuccLimit.isSuccPrelimit
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h_1 : Nontrivial α
h : IsOpen[inst_1] {a}
ha : IsSuccLimit a
l u : α
h₁ : a ∈ Set.Ioo l u
h₂ : Set.Ioo l u ⊆ {a}
refine_1 : Order.succ l = a
⊢ l ⋖ a

Tactic:
rw [← succ_eq_iff_covBy]

Premises used: Order.succ_eq_iff_covBy
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h_1 : Nontrivial α
h : IsOpen[inst_1] {a}
ha : IsSuccLimit a
l u : α
h₁ : a ∈ Set.Ioo l u
h₂ : Set.Ioo l u ⊆ {a}
⊢ l < a ∧ a < u

Tactic:
simp only [Set.mem_Ioo, Set.subset_singleton_iff] at h₁ h₂

Premises used: Set.mem_Ioo, Set.subset_singleton_iff
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h_1 : Nontrivial α
h : IsOpen[inst_1] {a}
ha : IsSuccLimit a
l u : α
h₁ : a ∈ Set.Ioo l u
h₂ : Set.Ioo l u ⊆ {a}
h₃ : l < a ∧ a < u
⊢ ∀ (y : α), l < y ∧ y < u → y = a

Tactic:
simp only [Set.mem_Ioo, Set.subset_singleton_iff] at h₁ h₂

Premises used: Set.mem_Ioo, Set.subset_singleton_iff
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h_1 : Nontrivial α
h : IsOpen[inst_1] {a}
ha : IsSuccLimit a
l u : α
h₁ : l < a ∧ a < u
h₂ : ∀ (y : α), l < y ∧ y < u → y = a
⊢ Order.succ l = a

Tactic:
h₂ _ ⟨lt_succ l, h₁.1.succ_le.trans_lt h₁.2⟩

Premises used: Order.lt_succ, And.right, And.left, And.intro, LT.lt.succ_le, LE.le.trans_lt
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h_1 : Nontrivial α
h : IsOpen[inst_1] {a}
ha : IsSuccLimit a
l u : α
h₁ : l < a ∧ a < u
h₂ : ∀ (y : α), l < y ∧ y < u → y = a
⊢ Order.succ l = a

Tactic:
exact h₂ _ ⟨lt_succ l, h₁.1.succ_le.trans_lt h₁.2⟩

Premises used: Order.lt_succ, And.right, And.left, And.intro, LT.lt.succ_le, LE.le.trans_lt
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h : Nontrivial α
ha : ¬IsSuccLimit a
refine_2 : ∀ (ha : IsMin a), IsOpen[inst_1] {a}
refine_2₁ : ∀ (ha : ¬IsSuccPrelimit a), IsOpen[inst_1] {a}
⊢ IsOpen[inst_1] {a}

Tactic:
obtain (ha | ha) := not_isSuccLimit_iff.mp ha

Premises used: Order.not_isSuccLimit_iff, Iff.mp
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h : Nontrivial α
ha_1 : ¬IsSuccLimit a
ha : IsMin a
⊢ IsOpen[inst_1] (Set.Iio (Order.succ a))

Tactic:
isOpen_Iio (a := Order.succ a)

Premises used: isOpen_Iio
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h_1 : Nontrivial α
ha_1 : ¬IsSuccLimit a
ha : IsMin a
h : {a} = Set.Iio (Order.succ a)
⊢ IsOpen[inst_1] {a}

Tactic:
convert! isOpen_Iio (a := Order.succ a) using 1

Premises used: isOpen_Iio
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h : Nontrivial α
ha_1 : ¬IsSuccLimit a
ha : IsMin a
⊢ {a} = Set.Iio (Order.succ a)

Tactic:
simp [ha.Iic_eq]

Premises used: IsMin.Iic_eq
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h : Nontrivial α
ha_1 : ¬IsSuccLimit a
ha : ¬IsSuccPrelimit a
⊢ IsOpen[inst_1] {a}

Tactic:
isOpen_singleton_of_not_isSuccPrelimit ha

Premises used: SuccOrder.isOpen_singleton_of_not_isSuccPrelimit
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h : Nontrivial α
ha_1 : ¬IsSuccLimit a
ha : ¬IsSuccPrelimit a
⊢ IsOpen[inst_1] {a}

Tactic:
exact isOpen_singleton_of_not_isSuccPrelimit ha

Premises used: SuccOrder.isOpen_singleton_of_not_isSuccPrelimit
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
a : α
⊢ 𝓝 a = pure a ↔ ¬IsSuccLimit a

Tactic:
(isOpen_singleton_iff_nhds_eq_pure _).symm.trans isOpen_singleton_iff

Premises used: SuccOrder.isOpen_singleton_iff, isOpen_singleton_iff_nhds_eq_pure, Iff.trans, Iff.symm
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
s : Set α
⊢ IsOpen[inst_1] s ↔ ∀ o ∈ s, IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s

Tactic:
isOpen_iff_mem_nhds.trans <| forall₂_congr fun o ho ↦ ?_

Premises used: forall₂_congr, Iff.trans, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
s : Set α
refine : ∀ (o : α) (ho : o ∈ s), s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s
⊢ IsOpen[inst_1] s ↔ ∀ o ∈ s, IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s

Tactic:
refine isOpen_iff_mem_nhds.trans <| forall₂_congr fun o ho ↦ ?_

Premises used: forall₂_congr, Iff.trans, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
s : Set α
o : α
ho : o ∈ s
pos : ∀ (ho' : IsSuccLimit o), s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s
neg : ∀ (ho' : ¬IsSuccLimit o), s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s
⊢ s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s

Tactic:
by_cases ho' : IsSuccLimit o

Premises used: Order.IsSuccLimit
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
s : Set α
o : α
ho : o ∈ s
ho' : IsSuccLimit o
pos : (∃ i < o, Set.Ioc i o ⊆ s) ↔ IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s
⊢ s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s

Tactic:
rw [(SuccOrder.hasBasis_nhds_Ioc_of_exists_lt (not_isMin_iff.1 ho'.not_isMin)).mem_iff]

Premises used: not_isMin_iff, Filter.HasBasis.mem_iff, SuccOrder.hasBasis_nhds_Ioc_of_exists_lt, Order.IsSuccLimit.not_isMin, Iff.mp
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
s : Set α
o : α
ho : o ∈ s
ho' : IsSuccLimit o
⊢ (∃ i < o, Set.Ioc i o ⊆ s) ↔ IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s

Tactic:
grind
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
s : Set α
o : α
ho : o ∈ s
ho' : ¬IsSuccLimit o
⊢ s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s

Tactic:
simp [nhds_eq_pure.2 ho', ho, ho']

Premises used: Iff.mpr, SuccOrder.nhds_eq_pure
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
a : α
s : Set α
ha : a ∈ frontier s
rw : ¬IsOpen[inst_1] {a}
⊢ IsSuccLimit a

Tactic:
rw [← isOpen_singleton_iff.not_left]

Premises used: Iff.not_left, SuccOrder.isOpen_singleton_iff
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
a : α
s : Set α
ha : a ∈ frontier s
⊢ a ∈ closure[inst_1] s ∩ closure[inst_1] sᶜ

Tactic:
rw [frontier_eq_closure_inter_closure] at ha

Premises used: frontier_eq_closure_inter_closure
-- Module: Mathlib.Topology.Order.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
a : α
s : Set α
ha : a ∈ closure[inst_1] s ∩ closure[inst_1] sᶜ
⊢ ¬IsOpen[inst_1] {a}

Tactic:
grind [mem_closure_iff, Set.Nonempty]

Premises used: mem_closure_iff, Set.Nonempty
-- Module: Mathlib.Topology.Order.T5
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s : Set X
⊢ s.ordConnectedComponent a ∈ 𝓝 a ↔ s ∈ 𝓝 a

Tactic:
⟨fun h => mem_of_superset h ordConnectedComponent_subset, fun h => ?_⟩

Premises used: Iff.intro, Set.ordConnectedComponent_subset, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.T5
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s : Set X
refine : ∀ (h : s ∈ 𝓝 a), s.ordConnectedComponent a ∈ 𝓝 a
⊢ s.ordConnectedComponent a ∈ 𝓝 a ↔ s ∈ 𝓝 a

Tactic:
refine ⟨fun h => mem_of_superset h ordConnectedComponent_subset, fun h => ?_⟩
-- Module: Mathlib.Topology.Order.T5
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s : Set X
h : s ∈ 𝓝 a
rcases : ∀ (b c : X) (ha : a ∈ Icc b c) (ha' : Icc b c ∈ 𝓝 a) (hs : Icc b c ⊆ s), s.ordConnectedComponent a ∈ 𝓝 a
⊢ s.ordConnectedComponent a ∈ 𝓝 a

Tactic:
rcases exists_Icc_mem_subset_of_mem_nhds h with ⟨b, c, ha, ha', hs⟩

Premises used: exists_Icc_mem_subset_of_mem_nhds
-- Module: Mathlib.Topology.Order.T5
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s : Set X
h : s ∈ 𝓝 a
b c : X
ha : a ∈ Icc b c
ha' : Icc b c ∈ 𝓝 a
hs : Icc b c ⊆ s
⊢ s.ordConnectedComponent a ∈ 𝓝 a

Tactic:
mem_of_superset ha' (subset_ordConnectedComponent ha hs)

Premises used: Set.subset_ordConnectedComponent, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.T5
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s : Set X
h : s ∈ 𝓝 a
b c : X
ha : a ∈ Icc b c
ha' : Icc b c ∈ 𝓝 a
hs : Icc b c ⊆ s
⊢ s.ordConnectedComponent a ∈ 𝓝 a

Tactic:
exact mem_of_superset ha' (subset_ordConnectedComponent ha hs)

Premises used: Set.subset_ordConnectedComponent, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.T5
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
⊢ tᶜ ∈ 𝓝[≥] a

Tactic:
mem_nhdsWithin_of_mem_nhds ?_

Premises used: mem_nhdsWithin_of_mem_nhds
-- Module: Mathlib.Topology.Order.T5
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
refine : tᶜ ∈ 𝓝 a
⊢ tᶜ ∈ 𝓝[≥] a

Tactic:
refine mem_nhdsWithin_of_mem_nhds ?_

Premises used: mem_nhdsWithin_of_mem_nhds
-- Module: Mathlib.Topology.Order.T5
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
rw : a ∈ (closure[inst_1] t)ᶜ
⊢ tᶜ ∈ 𝓝 a

Tactic:
rw [← mem_interior_iff_mem_nhds, interior_compl]

Premises used: mem_interior_iff_mem_nhds, interior_compl
-- Module: Mathlib.Topology.Order.T5
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
⊢ a ∈ (closure[inst_1] t)ᶜ

Tactic:
disjoint_left.1 hd ha

Premises used: Set.Mem, Set.disjoint_left, setOf, Iff.mp, Not
-- Module: Mathlib.Topology.Order.T5
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
⊢ a ∈ (closure[inst_1] t)ᶜ

Tactic:
exact disjoint_left.1 hd ha

Premises used: Set.disjoint_left, Iff.mp
-- Module: Mathlib.Topology.Order.T5
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
⊢ tᶜ ∈ 𝓝[≥] a

Tactic:
have hmem : tᶜ ∈ 𝓝[≥] a := by
    refine mem_nhdsWithin_of_mem_nhds ?_
    rw [← mem_interior_iff_mem_nhds, interior_compl]
    exact disjoint_left.1 hd ha
-- Module: Mathlib.Topology.Order.T5
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
rcases :
  ∀ (b : X) (hab : a ≤ b) (hmem' : Icc a b ∈ 𝓝[≥] a) (hsub : Icc a b ⊆ tᶜ),
    (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
rcases exists_Icc_mem_subset_of_mem_nhdsGE hmem with ⟨b, hab, hmem', hsub⟩

Premises used: exists_Icc_mem_subset_of_mem_nhdsGE
-- Module: Mathlib.Topology.Order.T5
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
pos :
  ∀ (H : Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection),
    (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
neg :
  ∀ (H : ¬Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection),
    (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
by_cases H : Disjoint (Icc a b) (ordConnectedSection <| ordSeparatingSet s t)

Premises used: Set.ordSeparatingSet, Disjoint, Set.Icc, Set.ordConnectedSection
-- Module: Mathlib.Topology.Order.T5
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
H : Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
mem_of_superset hmem' (disjoint_left.1 H)

Premises used: Set.disjoint_left, Iff.mp, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.T5
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
H : Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
exact mem_of_superset hmem' (disjoint_left.1 H)

Premises used: Set.disjoint_left, Iff.mp, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.T5
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
H : ¬Disjoint (Icc a b) (s.ordSeparatingSet t).ordConnectedSection
⊢ ∃ (x : X) (_ : x ∈ Icc a b), x ∈ (s.ordSeparatingSet t).ordConnectedSection

Tactic:
simp only [Set.disjoint_left, not_forall, Classical.not_not] at H

Premises used: Classical.not_not, Set.disjoint_left, Classical.not_forall