-- 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.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 ∈ {Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}

Tactic:
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 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, ∅}

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

Result:
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, ∅}

Proof state:
case pos.h.h.h.h.h.h.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 = Iic (sSup s)
⊢ s ∈ {Iic (sSup s), Iio (sSup s), univ, ∅}

Tactic:
exact Or.inl hs

Result:
no goals

Proof state:
case neg.h.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 ∈ {Iio (sSup s), univ, ∅}

Tactic:
apply Or.inr

Result:
case neg.h.h.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 ∈ {univ, ∅}

Proof state:
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, ∅}

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

Result:
case pos.h.h.h.h.h.h.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 = Iic (sSup s)
⊢ s ∈ {Iic (sSup s), Iio (sSup s), univ, ∅}

case pos.h.h.h.h.h.h.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 ∈ {Iio (sSup 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
⊢ 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:
have hs' : IsConnected s := ⟨hne, hs⟩

Result:
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, ∅}

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
⊢ {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]

Result:
no goals

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 ∈
    {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 8 apply Or.inr

Result:
case neg.h.h.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 ∈ {univ, ∅}

Proof state:
case pos.h.h.h.h.h.h.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 ∈ {Iio (sSup s)}
⊢ s ∈ {Iic (sSup s), Iio (sSup s), univ, ∅}

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

Result:
no goals

Proof state:
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, ∅}

Tactic:
apply_rules [Or.inr, mem_singleton]

Result:
no goals

Proof state:
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, ∅}

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

Result:
no goals

Proof state:
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, ∅}

Tactic:
exact Or.inl hs

Result:
no goals

Proof state:
case neg.h.h.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 ∈ {univ, ∅}

Tactic:
exact Or.inl (hs.eq_univ_of_unbounded hb ha)

Result:
no goals