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 : 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
⊢ 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 = 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: 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
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
⊢ 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 = 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: 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
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
⊢ 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 : 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
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_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, ∅}))
    s
have 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))
Tactic: rw [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_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, ∅}))
    s
have 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))
Tactic: rw [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_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, ∅}))
    s
have 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))
Tactic: rw [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_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, ∅}))
    s
have 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))
Tactic: rw [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_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, ∅}))
    s
have 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))
Tactic: rw [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_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, ∅}))
    s
have 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))
Tactic: rw [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_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, ∅}))
    s
have 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))
Tactic: rw [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_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, ∅}))
    s
have 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))
Tactic: rw [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_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, ∅}))
    s
have 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
Tactic: rw [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_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, ∅}))
    s
have 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, ∅}))
  ∅
Tactic: rw [hs]
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
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
⊢ b ∈ s
have ha₁ : a ∈ S
Tactic: replace ha : a ∈ S := ⟨ha, left_mem_Icc.2 hab⟩
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
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
⊢ b ∈ s
have Sbd : BddAbove S
Tactic: have Sbd : BddAbove S := ⟨b, fun z hz => hz.2.2⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
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)
⊢ b ∈ s
have c_mem : c ∈ S
Tactic: have c_mem : c ∈ S := hs.csSup_mem ⟨_, ha⟩ Sbd
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
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
⊢ b ∈ s
have c_le : c ≤ b
Tactic: have c_le : c ≤ b := csSup_le ⟨_, ha⟩ fun x hx => hx.2.2
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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
⊢ b ∈ s
have inl : ∀ (hc : c = b), b ∈ s
Tactic: rcases eq_or_lt_of_le c_le with hc | hc
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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
⊢ b ∈ s
have inr : ∀ (hc : c < b), b ∈ s
Tactic: rcases eq_or_lt_of_le c_le with hc | hc
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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
have inr : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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
⊢ False
have inr : ∀ (x : α) (xs : x ∈ s) (cx : c < x) (xb : x ≤ b), False
Tactic: rcases hgt c ⟨c_mem.1, c_mem.2.1, hc⟩ with ⟨x, xs, cx, xb⟩
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
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
hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty
y : α
hy : y ∈ Icc a b
⊢ IsClosed[inst] (s ∩ Icc a y)
have suffices : s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y
Tactic: suffices s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y from this ▸ hs.inter isClosed_Icc
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
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
hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty
y : α
hy : y ∈ Icc a b
⊢ y ∈ s
have this : IsClosed[inst] (s ∩ Icc a y)
Tactic: have : IsClosed (s ∩ Icc a y) := by
    suffices s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y from this ▸ hs.inter isClosed_Icc
    grind [inter_assoc, inter_eq_self_of_subset_right, Icc_subset_Icc_right]
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
hb : b ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
⊢ a ∈ s
have suffices : Membership.mem (α := αᵒᵈ) (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ)
Tactic: suffices OrderDual.toDual a ∈ ofDual ⁻¹' s by aesop
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
hb : b ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
⊢ Membership.mem (α := αᵒᵈ) (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ)
have this : IsClosed[instTopologicalSpace] ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (s ∩ Icc a b))
Tactic: have : IsClosed (OrderDual.ofDual ⁻¹' (s ∩ Icc a b)) := hs
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
hb : b ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
this : IsClosed[instTopologicalSpace] ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (s ∩ Icc a b))
⊢ Membership.mem (α := αᵒᵈ) (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ)
have this₁ : IsClosed[instTopologicalSpace]
  ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ)
Tactic: rw [preimage_inter, ← Icc_toDual] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
hb : b ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
this :
  IsClosed[instTopologicalSpace]
    ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ)
⊢ Membership.mem (α := αᵒᵈ) (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ)
have apply : ∀ (x : αᵒᵈ)
  (hx :
    Membership.mem (γ := Set αᵒᵈ)
      ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ) x),
  ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ioc x ((toDual : (a : α) → αᵒᵈ) a)).Nonempty
Tactic: apply this.mem_of_ge_of_forall_exists_gt (by simp_all) (by simp_all) (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.IntermediateValue (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
hb : b ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
this :
  IsClosed[instTopologicalSpace]
    ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ)
x : αᵒᵈ
hx :
  Membership.mem (γ := Set αᵒᵈ)
    ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ico ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ) x
⊢ ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ioc x ((toDual : (a : α) → αᵒᵈ) a)).Nonempty
have hx₁ : ∃ x_1 ∈ s ∩ Ioc a b, (Equiv.symm ofDual : (a : α) → αᵒᵈ) x_1 = x
Tactic: rw [Ico_toDual, ← preimage_inter, ← Equiv.image_symm_eq_preimage, mem_image] at hx
Cleared hypotheses: hx