awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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
⊢ Membership.mem (γ := Set (Set α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
have 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
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
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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
have 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
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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 α))
    {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
have 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
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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 α))
    {Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
have pos : 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
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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 α))
    {Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
have pos : Membership.mem (γ := Set (Set α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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 α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
have pos : Membership.mem (γ := Set (Set α)) {Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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 α)) {Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
have pos : Membership.mem (γ := Set (Set α)) {Iic (sSup s), Iio (sSup s), univ, ∅} s
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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
have pos : Membership.mem (γ := Set (Set α)) {Iic (sSup s), Iio (sSup s), univ, ∅} s
Tactic: iterate 6 apply Or.inr
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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 α)) {Iic (sSup s), Iio (sSup s), univ, ∅} s
have pos : ∀ (hs : s = Iic (sSup 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
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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
⊢ Membership.mem (γ := Set (Set α)) {Iic (sSup s), Iio (sSup s), univ, ∅} s
have pos₁ : ∀ (hs : Membership.mem (γ := Set (Set α)) {Iio (sSup s)} 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
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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
have 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
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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 α))
    {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
have 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
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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 α))
    {Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
have neg : 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
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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 α))
    {Ioo (sInf s) (sSup s), Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
have neg : Membership.mem (γ := Set (Set α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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 α)) {Ici (sInf s), Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
have neg : Membership.mem (γ := Set (Set α)) {Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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 α)) {Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅} s
have neg : Membership.mem (γ := Set (Set α)) {Iic (sSup s), Iio (sSup s), univ, ∅} s
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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 α)) {Iic (sSup s), Iio (sSup s), univ, ∅} s
have neg : Membership.mem (γ := Set (Set α)) {Iio (sSup s), univ, ∅} s
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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 α)) {Iio (sSup s), univ, ∅} s
have neg : Membership.mem (γ := Set (Set α)) {univ, ∅} s
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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
have neg : Membership.mem (γ := Set (Set α)) {univ, ∅} s
Tactic: iterate 8 apply Or.inr
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
⊢ Membership.mem (γ := Set (Set α))
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
    s
have inl : ∀ (hs : s = Icc (sInf s) (sSup s)),
  Membership.mem (γ := Set (Set α))
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
    s
Tactic: rcases hs.mem_intervals with (hs | hs | hs | hs | hs | hs | hs | hs | hs | hs)
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
inl :
  ∀ (hs : s = Icc (sInf s) (sSup s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
⊢ Membership.mem (γ := Set (Set α))
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
    s
have inr : ∀ (hs : s = Ico (sInf s) (sSup s)),
  Membership.mem (γ := Set (Set α))
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
    s
Tactic: rcases hs.mem_intervals with (hs | hs | hs | hs | hs | hs | hs | hs | hs | hs)
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
inl :
  ∀ (hs : s = Icc (sInf s) (sSup s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
inr :
  ∀ (hs : s = Ico (sInf s) (sSup s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
⊢ Membership.mem (γ := Set (Set α))
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
    s
have inr₁ : ∀ (hs : s = Ioc (sInf s) (sSup s)),
  Membership.mem (γ := Set (Set α))
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
    s
Tactic: rcases hs.mem_intervals with (hs | hs | hs | hs | hs | hs | hs | hs | hs | hs)
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
inl :
  ∀ (hs : s = Icc (sInf s) (sSup s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
inr :
  ∀ (hs : s = Ico (sInf s) (sSup s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
inr₁ :
  ∀ (hs : s = Ioc (sInf s) (sSup s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
⊢ Membership.mem (γ := Set (Set α))
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
    s
have inr₂ : ∀ (hs : s = Ioo (sInf s) (sSup s)),
  Membership.mem (γ := Set (Set α))
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
    s
Tactic: rcases hs.mem_intervals with (hs | hs | hs | hs | hs | hs | hs | hs | hs | hs)
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
inl :
  ∀ (hs : s = Icc (sInf s) (sSup s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
inr :
  ∀ (hs : s = Ico (sInf s) (sSup s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
inr₁ :
  ∀ (hs : s = Ioc (sInf s) (sSup s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
inr₂ :
  ∀ (hs : s = Ioo (sInf s) (sSup s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
⊢ Membership.mem (γ := Set (Set α))
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
    s
have inr₃ : ∀ (hs : s = Ici (sInf s)),
  Membership.mem (γ := Set (Set α))
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
    s
Tactic: rcases hs.mem_intervals with (hs | hs | hs | hs | hs | hs | hs | hs | hs | hs)
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
inl :
  ∀ (hs : s = Icc (sInf s) (sSup s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
inr :
  ∀ (hs : s = Ico (sInf s) (sSup s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
inr₁ :
  ∀ (hs : s = Ioc (sInf s) (sSup s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
inr₂ :
  ∀ (hs : s = Ioo (sInf s) (sSup s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
inr₃ :
  ∀ (hs : s = Ici (sInf s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
⊢ Membership.mem (γ := Set (Set α))
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
    s
have inr₄ : ∀ (hs : s = Ioi (sInf s)),
  Membership.mem (γ := Set (Set α))
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
    s
Tactic: rcases hs.mem_intervals with (hs | hs | hs | hs | hs | hs | hs | hs | hs | hs)
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
inl :
  ∀ (hs : s = Icc (sInf s) (sSup s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
inr :
  ∀ (hs : s = Ico (sInf s) (sSup s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
inr₁ :
  ∀ (hs : s = Ioc (sInf s) (sSup s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
inr₂ :
  ∀ (hs : s = Ioo (sInf s) (sSup s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
inr₃ :
  ∀ (hs : s = Ici (sInf s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
inr₄ :
  ∀ (hs : s = Ioi (sInf s)),
    Membership.mem (γ := Set (Set α))
      (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
      s
⊢ Membership.mem (γ := Set (Set α))
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
    s
have inr₅ : ∀ (hs : s = Iic (sSup s)),
  Membership.mem (γ := Set (Set α))
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
    s
Tactic: rcases hs.mem_intervals with (hs | hs | hs | hs | hs | hs | hs | hs | hs | hs)