awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsConnected s
hb : BddBelow s
ha : BddAbove s
⊢ Ioo (sInf s) (sSup s) ⊆ s

Tactic:
fun _x hx =>
  let ⟨_y, ys, hy⟩ := (isGLB_lt_iff (isGLB_csInf hs.nonempty hb)).1 hx.1
  let ⟨_z, zs, hz⟩ := (lt_isLUB_iff (isLUB_csSup hs.nonempty ha)).1 hx.2
  hs.Icc_subset ys zs ⟨hy.le, hz.le⟩

Premises used: _private.0.IsConnected.Ioo_csInf_csSup_subset.match_1, _private.0.IsConnected.Ioo_csInf_csSup_subset.match_2, lt_isLUB_iff, Membership.mem, isGLB_lt_iff, LT.lt.le, Set.Subset, IsConnected.Icc_subset, IsConnected.nonempty, isGLB_csInf, And.right, And.left, And.intro, Iff.mp, isLUB_csSup
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hc : IsConnected s
hb : BddBelow s
ha : BddAbove s
hcl : IsClosed[inst] s
⊢ s = Icc (sInf s) (sSup s)

Tactic:
(subset_Icc_csInf_csSup hb ha).antisymm <|
    hc.Icc_subset (hcl.csInf_mem hc.nonempty hb) (hcl.csSup_mem hc.nonempty ha)

Premises used: IsConnected.Icc_subset, IsClosed.csSup_mem, IsConnected.nonempty, HasSubset.Subset.antisymm, subset_Icc_csInf_csSup, IsClosed.csInf_mem
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hb : BddBelow s
ha : ¬BddAbove s
⊢ Ioi (sInf s) ⊆ s

Tactic:
fun x hx =>
  have sne : s.Nonempty := nonempty_of_not_bddAbove ha
  let ⟨_y, ys, hy⟩ : ∃ y ∈ s, y < x := (isGLB_lt_iff (isGLB_csInf sne hb)).1 hx
  let ⟨_z, zs, hz⟩ : ∃ z ∈ s, x < z := not_bddAbove_iff.1 ha x
  hs.Icc_subset ys zs ⟨hy.le, hz.le⟩

Premises used: _private.0.IsConnected.Ioo_csInf_csSup_subset.match_1, _private.0.IsConnected.Ioo_csInf_csSup_subset.match_2, Membership.mem, isGLB_lt_iff, LT.lt.le, Set.Subset, isGLB_csInf, And.intro, Iff.mp, not_bddAbove_iff, IsPreconnected.Icc_subset, nonempty_of_not_bddAbove
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : BddAbove s
⊢ Iio (sSup s) ⊆ s

Tactic:
IsPreconnected.Ioi_csInf_subset (α := αᵒᵈ) hs ha hb

Premises used: setOf, OrderDual, Set.Iio, IsPreconnected.Ioi_csInf_subset
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
inl :
  ∀ (hs : IsPreconnected.{u} (α := α) ∅),
    Membership.mem (γ := Set (Set α))
      {Icc (sInf ∅) (sSup ∅), Ico (sInf ∅) (sSup ∅), Ioc (sInf ∅) (sSup ∅), Ioo (sInf ∅) (sSup ∅), Ici (sInf ∅),
        Ioi (sInf ∅), Iic (sSup ∅), Iio (sSup ∅), univ, ∅}
      ∅
inr :
  ∀ (hne : s.Nonempty),
    Membership.mem (γ := Set (Set α))
      {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
        Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
      s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hne)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
hs : IsPreconnected.{u} (α := α) ∅
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf ∅) (sSup ∅), Ico (sInf ∅) (sSup ∅), Ioc (sInf ∅) (sSup ∅), Ioo (sInf ∅) (sSup ∅), Ici (sInf ∅),
      Ioi (sInf ∅), Iic (sSup ∅), Iio (sSup ∅), univ, ∅}
    ∅

Tactic:
apply_rules [Or.inr, mem_singleton]

Premises used: Set.mem_singleton, Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
⊢ IsConnected s

Tactic:
have hs' : IsConnected s := ⟨hne, hs⟩
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
pos :
  ∀ (hb : BddBelow s),
    Membership.mem (γ := Set (Set α))
      {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
        Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
      s
neg :
  ∀ (hb : ¬BddBelow s),
    Membership.mem (γ := Set (Set α))
      {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
        Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
      s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s

Tactic:
by_cases hb : BddBelow s

Premises used: BddBelow
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
pos :
  ∀ (ha : BddAbove s),
    Membership.mem (γ := Set (Set α))
      {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
        Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
      s
neg :
  ∀ (ha : ¬BddAbove s),
    Membership.mem (γ := Set (Set α))
      {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
        Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
      s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s

Tactic:
by_cases ha : BddAbove s

Premises used: BddAbove
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
pos :
  ∀ (ha : BddAbove s),
    Membership.mem (γ := Set (Set α))
      {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
        Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
      s
neg :
  ∀ (ha : ¬BddAbove s),
    Membership.mem (γ := Set (Set α))
      {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
        Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
      s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s

Tactic:
by_cases ha : BddAbove s

Premises used: BddAbove
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : BddAbove s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s

Tactic:
mem_of_subset_of_mem ?_ <| mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset
      (hs'.Ioo_csInf_csSup_subset hb ha) (subset_Icc_csInf_csSup hb ha)

Premises used: IsConnected.Ioo_csInf_csSup_subset, Set.mem_of_subset_of_mem, Set.mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset, subset_Icc_csInf_csSup
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : BddAbove s
pos :
  Subset (α := Set (Set α)) {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s)}
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s

Tactic:
refine mem_of_subset_of_mem ?_ <| mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset
      (hs'.Ioo_csInf_csSup_subset hb ha) (subset_Icc_csInf_csSup hb ha)

Premises used: IsConnected.Ioo_csInf_csSup_subset, Set.mem_of_subset_of_mem, Set.mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset, subset_Icc_csInf_csSup
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : BddAbove s
⊢ Subset (α := Set (Set α)) {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s)}
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}

Tactic:
simp only [insert_subset_iff, mem_insert_iff, mem_singleton_iff, true_or, or_true,
      singleton_subset_iff, and_self]

Premises used: Set.singleton_subset_iff, and_self, true_or, Set.insert_subset_iff, Set.mem_singleton_iff, Set.mem_insert_iff, or_true
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s

Tactic:
Or.inr <| Or.inr <| Or.inr <| Or.inr ?_

Premises used: Set.insert, Set.Mem, setOf, Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
neg : Membership.mem (γ := Set (Set α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s

Tactic:
refine Or.inr <| Or.inr <| Or.inr <| Or.inr ?_

Premises used: Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
neg :
  ∀ (hs : s = Ici (sInf s)),
    Membership.mem (γ := Set (Set α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
neg₁ :
  ∀ (hs : Membership.mem (γ := Set (Set α)) {Ioi (sInf s)} s),
    Membership.mem (γ := Set (Set α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
⊢ Membership.mem (γ := Set (Set α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s

Tactic:
rcases mem_Ici_Ioi_of_subset_of_subset (hs.Ioi_csInf_subset hb ha) fun x hx ↦
      csInf_le hb hx with hs | hs

Premises used: Set.mem_Ici_Ioi_of_subset_of_subset, csInf_le, IsPreconnected.Ioi_csInf_subset
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
hs : s = Ici (sInf s)
⊢ Membership.mem (γ := Set (Set α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s

Tactic:
Or.inl hs

Premises used: Set.insert, Set.Mem, setOf, Or.inl
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
hs : s = Ici (sInf s)
⊢ Membership.mem (γ := Set (Set α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s

Tactic:
exact Or.inl hs

Premises used: Or.inl
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
hs : Membership.mem (γ := Set (Set α)) {Ioi (sInf s)} s
⊢ Membership.mem (γ := Set (Set α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s

Tactic:
Or.inr (Or.inl hs)

Premises used: Set.insert, Set.Mem, setOf, Or.inl, Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
hs : Membership.mem (γ := Set (Set α)) {Ioi (sInf s)} s
⊢ Membership.mem (γ := Set (Set α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s

Tactic:
exact Or.inr (Or.inl hs)

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
pos :
  Membership.mem (γ := Set (Set α))
    {Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s),
      Iio (sSup s), univ, ∅}
    s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
pos :
  Membership.mem (γ := Set (Set α))
    {Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
⊢ Membership.mem (γ := Set (Set α))
    {Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s),
      Iio (sSup s), univ, ∅}
    s

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
pos :
  Membership.mem (γ := Set (Set α))
    {Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
⊢ Membership.mem (γ := Set (Set α))
    {Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
pos : Membership.mem (γ := Set (Set α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
⊢ Membership.mem (γ := Set (Set α))
    {Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
pos : Membership.mem (γ := Set (Set α)) {Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
⊢ Membership.mem (γ := Set (Set α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
pos : Membership.mem (γ := Set (Set α)) {Iic (sSup s), Iio (sSup s), univ, ∅} s
⊢ Membership.mem (γ := Set (Set α)) {Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
pos : Membership.mem (γ := Set (Set α)) {Iic (sSup s), Iio (sSup s), univ, ∅} s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s

Tactic:
iterate 6 apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
pos : ∀ (hs : s = Iic (sSup s)), Membership.mem (γ := Set (Set α)) {Iic (sSup s), Iio (sSup s), univ, ∅} s
pos₁ :
  ∀ (hs : Membership.mem (γ := Set (Set α)) {Iio (sSup s)} s),
    Membership.mem (γ := Set (Set α)) {Iic (sSup s), Iio (sSup s), univ, ∅} s
⊢ Membership.mem (γ := Set (Set α)) {Iic (sSup s), Iio (sSup s), univ, ∅} s

Tactic:
rcases mem_Iic_Iio_of_subset_of_subset (hs.Iio_csSup_subset hb ha) fun x hx ↦
      le_csSup ha hx with hs | hs

Premises used: IsPreconnected.Iio_csSup_subset, Set.mem_Iic_Iio_of_subset_of_subset, le_csSup
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
hs : s = Iic (sSup s)
⊢ Membership.mem (γ := Set (Set α)) {Iic (sSup s), Iio (sSup s), univ, ∅} s

Tactic:
Or.inl hs

Premises used: Set.insert, Set.Mem, setOf, Or.inl
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
hs : s = Iic (sSup s)
⊢ Membership.mem (γ := Set (Set α)) {Iic (sSup s), Iio (sSup s), univ, ∅} s

Tactic:
exact Or.inl hs

Premises used: Or.inl
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
hs : Membership.mem (γ := Set (Set α)) {Iio (sSup s)} s
⊢ Membership.mem (γ := Set (Set α)) {Iic (sSup s), Iio (sSup s), univ, ∅} s

Tactic:
Or.inr (Or.inl hs)

Premises used: Set.insert, Set.Mem, setOf, Or.inl, Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
hs : Membership.mem (γ := Set (Set α)) {Iio (sSup s)} s
⊢ Membership.mem (γ := Set (Set α)) {Iic (sSup s), Iio (sSup s), univ, ∅} s

Tactic:
exact Or.inr (Or.inl hs)

Premises used: Or.inl, Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
neg :
  Membership.mem (γ := Set (Set α))
    {Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s),
      Iio (sSup s), univ, ∅}
    s
⊢ Membership.mem (γ := Set (Set α))
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
    s

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
neg :
  Membership.mem (γ := Set (Set α))
    {Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
⊢ Membership.mem (γ := Set (Set α))
    {Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s),
      Iio (sSup s), univ, ∅}
    s

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
neg :
  Membership.mem (γ := Set (Set α))
    {Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
⊢ Membership.mem (γ := Set (Set α))
    {Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
neg : Membership.mem (γ := Set (Set α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
⊢ Membership.mem (γ := Set (Set α))
    {Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
neg : Membership.mem (γ := Set (Set α)) {Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
⊢ Membership.mem (γ := Set (Set α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
neg : Membership.mem (γ := Set (Set α)) {Iic (sSup s), Iio (sSup s), univ, ∅} s
⊢ Membership.mem (γ := Set (Set α)) {Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s

Tactic:
apply Or.inr

Premises used: Or.inr