awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ∃ (x : X) (_ : x ∈ Icc a b), x ∈ (s.ordSeparatingSet t).ordConnectedSection
neg :
  ∀ (c : X) (hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection) (hac : a ≤ c) (hcb : c ≤ b),
    (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
rcases H with ⟨c, ⟨hac, hcb⟩, hc⟩
-- 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hac : a ≤ c
hcb : c ≤ b
⊢ Icc a b ⊆ tᶜ.ordConnectedComponent a

Tactic:
have hsub' : Icc a b ⊆ ordConnectedComponent tᶜ a :=
      subset_ordConnectedComponent (left_mem_Icc.2 hab) hsub
-- 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hac : a ≤ c
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
⊢ Disjoint s (s.ordSeparatingSet t).ordConnectedSection

Tactic:
have hd : Disjoint s (ordConnectedSection (ordSeparatingSet s t)) :=
      disjoint_left_ordSeparatingSet.mono_right ordConnectedSection_subset
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hac : a ≤ c
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
⊢ a < c

Tactic:
replace hac : a < c := hac.lt_of_ne <| Ne.symm <| ne_of_mem_of_not_mem hc <|
      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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
h : ∀ (x : X) (hx : x ∈ Ico a c) (hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection), False
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
filter_upwards [Ico_mem_nhdsGE hac] with x hx hx'

Premises used: Ico_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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ False

Tactic:
hx.2.ne (eq_of_mem_ordConnectedSection_of_uIcc_subset hx' hc ?_)

Premises used: Set.eq_of_mem_ordConnectedSection_of_uIcc_subset, And.right, LT.lt.ne
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
h : [[x, c]] ⊆ s.ordSeparatingSet t
⊢ False

Tactic:
refine hx.2.ne (eq_of_mem_ordConnectedSection_of_uIcc_subset hx' hc ?_)

Premises used: Set.eq_of_mem_ordConnectedSection_of_uIcc_subset, And.right, LT.lt.ne
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ [[x, c]] ⊆ s.ordSeparatingSet t

Tactic:
subset_inter (subset_iUnion₂_of_subset a ha ?_) ?_

Premises used: Set.ordSeparatingSet, Set.subset_iUnion₂_of_subset, Set.subset_inter
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
h : [[x, c]] ⊆ tᶜ.ordConnectedComponent a
h₁ : [[x, c]] ⊆ ⋃ x ∈ t, sᶜ.ordConnectedComponent x
⊢ [[x, c]] ⊆ s.ordSeparatingSet t

Tactic:
refine subset_inter (subset_iUnion₂_of_subset a ha ?_) ?_

Premises used: Set.subset_iUnion₂_of_subset, Set.subset_inter
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ [[x, c]] ⊆ tᶜ.ordConnectedComponent a

Tactic:
OrdConnected.uIcc_subset inferInstance (hsub' ⟨hx.1, hx.2.le.trans hcb⟩)
        (hsub' ⟨hac.le, hcb⟩)

Premises used: Set.OrdConnected.uIcc_subset, inferInstance, LT.lt.le, And.right, And.left, And.intro, LE.le.trans
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ [[x, c]] ⊆ tᶜ.ordConnectedComponent a

Tactic:
exact OrdConnected.uIcc_subset inferInstance (hsub' ⟨hx.1, hx.2.le.trans hcb⟩)
        (hsub' ⟨hac.le, hcb⟩)

Premises used: Set.OrdConnected.uIcc_subset, inferInstance, LT.lt.le, And.right, And.left, And.intro, LE.le.trans
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
h : ∀ (y : X) (hyt : y ∈ t) (hxy : x ∈ sᶜ.ordConnectedComponent y), [[x, c]] ⊆ ⋃ x ∈ t, sᶜ.ordConnectedComponent x
⊢ [[x, c]] ⊆ ⋃ x ∈ t, sᶜ.ordConnectedComponent x

Tactic:
rcases mem_iUnion₂.1 (ordConnectedSection_subset hx').2 with ⟨y, hyt, hxy⟩

Premises used: Set.mem_iUnion₂, And.right, Iff.mp, Set.ordConnectedSection_subset
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
⊢ [[x, c]] ⊆ ⋃ x ∈ t, sᶜ.ordConnectedComponent x

Tactic:
subset_iUnion₂_of_subset y hyt (OrdConnected.uIcc_subset inferInstance hxy ?_)

Premises used: Set.OrdConnected.uIcc_subset, Set.subset_iUnion₂_of_subset, inferInstance
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
h : c ∈ sᶜ.ordConnectedComponent y
⊢ [[x, c]] ⊆ ⋃ x ∈ t, sᶜ.ordConnectedComponent x

Tactic:
refine subset_iUnion₂_of_subset y hyt (OrdConnected.uIcc_subset inferInstance hxy ?_)

Premises used: Set.subset_iUnion₂_of_subset
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
⊢ c ∈ sᶜ.ordConnectedComponent y

Tactic:
subset_ordConnectedComponent left_mem_uIcc hxy ?_

Premises used: Set.subset_ordConnectedComponent, Set.left_mem_uIcc
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
h : c ∈ [[y, x]]
⊢ c ∈ sᶜ.ordConnectedComponent y

Tactic:
refine subset_ordConnectedComponent left_mem_uIcc hxy ?_

Premises used: Set.subset_ordConnectedComponent, Set.left_mem_uIcc
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
this : c < y
rw : c ∈ Icc x y
⊢ c ∈ [[y, x]]

Tactic:
rw [uIcc_of_ge (hx.2.trans this).le]

Premises used: Set.uIcc_of_ge, LT.lt.le, And.right, LT.lt.trans
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
this : c < y
⊢ c ∈ Icc x y

Tactic:
⟨hx.2.le, this.le⟩

Premises used: Set.Mem, setOf, LT.lt.le, Set.Icc, And.right, And.intro
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
this : c < y
⊢ c ∈ Icc x y

Tactic:
exact ⟨hx.2.le, this.le⟩
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
h : c < y
⊢ c ∈ [[y, x]]

Tactic:
suffices c < y by
        rw [uIcc_of_ge (hx.2.trans this).le]
        exact ⟨hx.2.le, this.le⟩
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
⊢ c < y

Tactic:
lt_of_not_ge fun hyc => ?_

Premises used: lt_of_not_ge
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
h : ∀ (hyc : y ≤ c), False
⊢ c < y

Tactic:
refine lt_of_not_ge fun hyc => ?_

Premises used: lt_of_not_ge
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
hyc : y ≤ c
⊢ y < a

Tactic:
have hya : y < a := not_le.1 fun hay => hsub ⟨hay, hyc.trans hcb⟩ hyt
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
hyc : y ≤ c
hya : y < a
⊢ False

Tactic:
hxy (Icc_subset_uIcc ⟨hya.le, hx.1⟩) ha

Premises used: Set.Icc_subset_uIcc, LT.lt.le, And.left, And.intro
-- 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_1 : 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ᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
hyc : y ≤ c
hya : y < a
⊢ False

Tactic:
exact hxy (Icc_subset_uIcc ⟨hya.le, hx.1⟩) ha

Premises used: Set.Icc_subset_uIcc, LT.lt.le, And.left, And.intro
-- 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
⊢ Disjoint (α := Set Xᵒᵈ) ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s)
    (closure[instTopologicalSpace] ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' t))

Tactic:
have hd' : Disjoint (ofDual ⁻¹' s) (closure <| ofDual ⁻¹' t) := hd
-- 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
hd' :
  Disjoint (α := Set Xᵒᵈ) ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s)
    (closure[instTopologicalSpace] ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' t))
⊢ Membership.mem (α := Xᵒᵈ) (γ := Set Xᵒᵈ) ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s) ((toDual : (a : X) → Xᵒᵈ) a : Xᵒᵈ)

Tactic:
have ha' : toDual a ∈ ofDual ⁻¹' s := 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
hd' :
  Disjoint (α := Set Xᵒᵈ) ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s)
    (closure[instTopologicalSpace] ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' t))
ha' : Membership.mem (α := Xᵒᵈ) (γ := Set Xᵒᵈ) ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s) ((toDual : (a : X) → Xᵒᵈ) a : Xᵒᵈ)
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a

Tactic:
simpa only [dual_ordSeparatingSet, dual_ordConnectedSection] using
    compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE hd' ha'

Premises used: Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE, Set.dual_ordConnectedSection, Set.dual_ordSeparatingSet
-- 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 : (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a ∧ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝 a

Tactic:
rw [← nhdsLE_sup_nhdsGE, mem_sup]

Premises used: Filter.mem_sup, nhdsLE_sup_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
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a ∧ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
⟨compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE hd ha,
    compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE hd ha⟩

Premises used: Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE, Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE, And.intro
-- 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
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a ∧ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
exact ⟨compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE hd ha,
    compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE hd ha⟩
-- Module: Mathlib.Topology.Order.T5
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
x : X
hx : x ∈ s
rw : x ∈ (closure[inst_1] t)ᶜ
⊢ tᶜ ∈ 𝓝 x

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
s t : Set X
hd : Disjoint s (closure[inst_1] t)
x : X
hx : x ∈ s
⊢ x ∈ (closure[inst_1] t)ᶜ

Tactic:
disjoint_left.1 hd hx

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
s t : Set X
hd : Disjoint s (closure[inst_1] t)
x : X
hx : x ∈ s
⊢ x ∈ (closure[inst_1] t)ᶜ

Tactic:
exact disjoint_left.1 hd hx

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
⊢ CompletelyNormalSpace X

Tactic:
⟨fun s t h₁ h₂ => Filter.disjoint_iff.2
    ⟨ordT5Nhd s t, ordT5Nhd_mem_nhdsSet h₂, ordT5Nhd t s, ordT5Nhd_mem_nhdsSet h₁.symm,
      disjoint_ordT5Nhd⟩⟩

Premises used: Iff.mpr, Set.disjoint_ordT5Nhd, Set.ordT5Nhd_mem_nhdsSet, Filter.disjoint_iff, Disjoint.symm, Set.ordT5Nhd, And.intro, Exists.intro, CompletelyNormalSpace.mk
-- 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
⊢ T5Space X

Tactic:
T5Space.mk

Premises used: T5Space.mk
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := WithUpperSet α ≃ α) (Equiv.symm toUpperSet) ofUpperSet

Tactic:
rfl

Premises used: Topology.WithUpperSet, Topology.WithUpperSet.ofUpperSet, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α ≃ WithUpperSet α) (Equiv.symm ofUpperSet) toUpperSet

Tactic:
rfl

Premises used: Topology.WithUpperSet.toUpperSet, Topology.WithUpperSet, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
a : WithUpperSet α
⊢ (toUpperSet : (a : α) → WithUpperSet α) ((ofUpperSet : (a : WithUpperSet α) → α) a : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
a : α
⊢ (ofUpperSet : (a : WithUpperSet α) → α) ((toUpperSet : (a : α) → WithUpperSet α) a : WithUpperSet α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
a b : α
⊢ Eq (α := WithUpperSet α) ((toUpperSet : (a : α) → WithUpperSet α) a : WithUpperSet α)
      ((toUpperSet : (a : α) → WithUpperSet α) b : WithUpperSet α) ↔
    a = b

Tactic:
Iff.rfl

Premises used: Iff.rfl, Topology.WithUpperSet