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 : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
neg : Membership.mem (γ := Set (Set α)) {Iio (sSup s), univ, ∅} s
⊢ Membership.mem (γ := Set (Set α)) {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 α)) {univ, ∅} s
⊢ Membership.mem (γ := Set (Set α)) {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 α)) {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 8 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
⊢ Membership.mem (γ := Set (Set α)) {univ, ∅} s

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

Premises used: Set.insert, IsPreconnected.eq_univ_of_unbounded, Set.Mem, setOf, Or.inl
-- 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 α)) {univ, ∅} s

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

Premises used: IsPreconnected.eq_univ_of_unbounded, Or.inl
-- Module: Mathlib.Topology.Order.IntermediateValue
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
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
inr₆ :
  ∀ (hs : s = Iio (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 = univ),
    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 : Membership.mem (γ := Set (Set α)) {∅} 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

Tactic:
rcases hs.mem_intervals with (hs | hs | hs | hs | hs | hs | hs | hs | hs | hs)

Premises used: IsPreconnected.mem_intervals
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
hs : s = Icc (sInf s) (sSup s)
inl :
  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, ∅}))
    (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:
rw [hs]
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
hs : s = Ico (sInf s) (sSup s)
inr :
  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, ∅}))
    (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:
rw [hs]
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
hs : s = Ioc (sInf s) (sSup s)
inr :
  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, ∅}))
    (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:
rw [hs]
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
hs : s = Ioo (sInf s) (sSup s)
inr :
  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, ∅}))
    (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:
rw [hs]
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
hs : s = Ici (sInf s)
inr :
  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, ∅}))
    (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:
rw [hs]
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
hs : s = Ioi (sInf s)
inr :
  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, ∅}))
    (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:
rw [hs]
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
hs : s = Iic (sSup s)
inr :
  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, ∅}))
    (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:
rw [hs]
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
hs : s = Iio (sSup s)
inr :
  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, ∅}))
    (Iio (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:
rw [hs]
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
hs : s = univ
inr :
  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, ∅}))
    univ
⊢ 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:
rw [hs]
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
hs : Membership.mem (γ := Set (Set α)) {∅} s
inr :
  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, ∅}))
    ∅
⊢ 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:
rw [hs]
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
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, ∅}))
    (Icc (sInf s) (sSup s))

Tactic:
simp only [union_insert, union_singleton, mem_insert_iff, mem_union, mem_range, Prod.exists,
      uncurry_apply_pair, exists_apply_eq_apply, true_or, or_true, exists_apply_eq_apply2]

Premises used: Set.mem_union, Set.mem_range, true_or, Set.union_insert, exists_apply_eq_apply2, Set.mem_insert_iff, Prod.exists, or_true, Set.union_singleton, Function.uncurry_apply_pair, exists_apply_eq_apply
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
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, ∅}))
    (Ico (sInf s) (sSup s))

Tactic:
simp only [union_insert, union_singleton, mem_insert_iff, mem_union, mem_range, Prod.exists,
      uncurry_apply_pair, exists_apply_eq_apply, true_or, or_true, exists_apply_eq_apply2]

Premises used: Set.mem_union, Set.mem_range, true_or, Set.union_insert, exists_apply_eq_apply2, Set.mem_insert_iff, Prod.exists, or_true, Set.union_singleton, Function.uncurry_apply_pair, exists_apply_eq_apply
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
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, ∅}))
    (Ioc (sInf s) (sSup s))

Tactic:
simp only [union_insert, union_singleton, mem_insert_iff, mem_union, mem_range, Prod.exists,
      uncurry_apply_pair, exists_apply_eq_apply, true_or, or_true, exists_apply_eq_apply2]

Premises used: Set.mem_union, Set.mem_range, true_or, Set.union_insert, exists_apply_eq_apply2, Set.mem_insert_iff, Prod.exists, or_true, Set.union_singleton, Function.uncurry_apply_pair, exists_apply_eq_apply
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
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, ∅}))
    (Ioo (sInf s) (sSup s))

Tactic:
simp only [union_insert, union_singleton, mem_insert_iff, mem_union, mem_range, Prod.exists,
      uncurry_apply_pair, exists_apply_eq_apply, true_or, or_true, exists_apply_eq_apply2]

Premises used: Set.mem_union, Set.mem_range, true_or, Set.union_insert, exists_apply_eq_apply2, Set.mem_insert_iff, Prod.exists, or_true, Set.union_singleton, Function.uncurry_apply_pair, exists_apply_eq_apply
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
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, ∅}))
    (Ici (sInf s))

Tactic:
simp only [union_insert, union_singleton, mem_insert_iff, mem_union, mem_range, Prod.exists,
      uncurry_apply_pair, exists_apply_eq_apply, true_or, or_true, exists_apply_eq_apply2]

Premises used: Set.mem_union, Set.mem_range, true_or, Set.union_insert, exists_apply_eq_apply2, Set.mem_insert_iff, Prod.exists, or_true, Set.union_singleton, Function.uncurry_apply_pair, exists_apply_eq_apply
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
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, ∅}))
    (Ioi (sInf s))

Tactic:
simp only [union_insert, union_singleton, mem_insert_iff, mem_union, mem_range, Prod.exists,
      uncurry_apply_pair, exists_apply_eq_apply, true_or, or_true, exists_apply_eq_apply2]

Premises used: Set.mem_union, Set.mem_range, true_or, Set.union_insert, exists_apply_eq_apply2, Set.mem_insert_iff, Prod.exists, or_true, Set.union_singleton, Function.uncurry_apply_pair, exists_apply_eq_apply
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
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, ∅}))
    (Iic (sSup s))

Tactic:
simp only [union_insert, union_singleton, mem_insert_iff, mem_union, mem_range, Prod.exists,
      uncurry_apply_pair, exists_apply_eq_apply, true_or, or_true, exists_apply_eq_apply2]

Premises used: Set.mem_union, Set.mem_range, true_or, Set.union_insert, exists_apply_eq_apply2, Set.mem_insert_iff, Prod.exists, or_true, Set.union_singleton, Function.uncurry_apply_pair, exists_apply_eq_apply
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
hs : s = Iio (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, ∅}))
    (Iio (sSup s))

Tactic:
simp only [union_insert, union_singleton, mem_insert_iff, mem_union, mem_range, Prod.exists,
      uncurry_apply_pair, exists_apply_eq_apply, true_or, or_true, exists_apply_eq_apply2]

Premises used: Set.mem_union, Set.mem_range, true_or, Set.union_insert, exists_apply_eq_apply2, Set.mem_insert_iff, Prod.exists, or_true, Set.union_singleton, Function.uncurry_apply_pair, exists_apply_eq_apply
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
hs : s = univ
⊢ 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, ∅}))
    univ

Tactic:
simp only [union_insert, union_singleton, mem_insert_iff, mem_union, mem_range, Prod.exists,
      uncurry_apply_pair, exists_apply_eq_apply, true_or, or_true, exists_apply_eq_apply2]

Premises used: Set.mem_union, Set.mem_range, true_or, Set.union_insert, exists_apply_eq_apply2, Set.mem_insert_iff, Prod.exists, or_true, Set.union_singleton, Function.uncurry_apply_pair, exists_apply_eq_apply
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
s : Set α
hs_1 : Membership.mem (γ := Set (Set α)) {s : Set α | IsPreconnected s} s
hs : Membership.mem (γ := Set (Set α)) {∅} 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, ∅}))
    ∅

Tactic:
simp only [union_insert, union_singleton, mem_insert_iff, mem_union, mem_range, Prod.exists,
      uncurry_apply_pair, exists_apply_eq_apply, true_or, or_true, exists_apply_eq_apply2]

Premises used: Set.mem_union, Set.mem_range, true_or, Set.union_insert, exists_apply_eq_apply2, Set.mem_insert_iff, Prod.exists, or_true, Set.union_singleton, Function.uncurry_apply_pair, exists_apply_eq_apply
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
⊢ a ∈ S

Tactic:
replace ha : a ∈ S := ⟨ha, left_mem_Icc.2 hab⟩
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
⊢ BddAbove S

Tactic:
have Sbd : BddAbove S := ⟨b, fun z hz => hz.2.2⟩
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
⊢ c ∈ S

Tactic:
have c_mem : c ∈ S := hs.csSup_mem ⟨_, ha⟩ Sbd
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
⊢ c ≤ b

Tactic:
have c_le : c ≤ b := csSup_le ⟨_, ha⟩ fun x hx => hx.2.2
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
inl : ∀ (hc : c = b), b ∈ s
inr : ∀ (hc : c < b), b ∈ s
⊢ b ∈ s

Tactic:
rcases eq_or_lt_of_le c_le with hc | hc

Premises used: eq_or_lt_of_le
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ico a b, (s ∩ Ioc x b).Nonempty
S : Set α := s ∩ Icc a b
ha : a ∈ S
Sbd : BddAbove S
c : α := sSup (s ∩ Icc a b)
c_mem : c ∈ S
c_le : c ≤ b
hc : c = b
⊢ b ∈ s

Tactic:
hc ▸ c_mem.1

Premises used: Eq.rec, And.left