-- Mathlib/Topology/Order/IntermediateValue.lean
theorem IsPreconnected.mem_intervals {s : Set α} (hs : IsPreconnected s) :
    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, ∅} : Set (Set α))

Proof state:
case pos
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : BddAbove s
⊢ 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:
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)

Result:
case pos
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : BddAbove s
⊢ {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, ∅}

Proof state:
case pos
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
⊢ 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:
iterate 6 apply Or.inr

Result:
case pos.h.h.h.h.h.h
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
⊢ s ∈ {Iic (sSup s), Iio (sSup s), univ, ∅}

Proof state:
case inr
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
⊢ 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:
by_cases hb : BddBelow s <;> by_cases ha : BddAbove s

Result:
case pos
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : BddAbove s
⊢ 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, ∅}

case neg
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
⊢ 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, ∅}

case pos
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
⊢ 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, ∅}

case neg
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ 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, ∅}

Proof state:
case neg
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
⊢ s ∈ {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}

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

Result:
case neg.inl
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs✝ : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
hs : s = Ici (sInf s)
⊢ s ∈ {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}

case neg.inr
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs✝ : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
hs : s ∈ {Ioi (sInf s)}
⊢ s ∈ {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}

Proof state:
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
⊢ 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:
rcases s.eq_empty_or_nonempty with (rfl | hne)

Result:
case inl
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
hs : IsPreconnected ∅
⊢ ∅ ∈
    {Icc (sInf ∅) (sSup ∅), Ico (sInf ∅) (sSup ∅), Ioc (sInf ∅) (sSup ∅), Ioo (sInf ∅) (sSup ∅), Ici (sInf ∅),
      Ioi (sInf ∅), Iic (sSup ∅), Iio (sSup ∅), univ, ∅}

case inr
α : Type u
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
⊢ 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, ∅}