awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact hc ▸ c_mem.1
-- 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
inr : False
⊢ b ∈ s

Tactic:
exfalso
-- 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
inr : ∀ (x : α) (xs : x ∈ s) (cx : c < x) (xb : x ≤ b), False
⊢ False

Tactic:
rcases hgt c ⟨c_mem.1, c_mem.2.1, hc⟩ with ⟨x, xs, cx, xb⟩

Premises used: And.right, And.left, And.intro
-- 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
x : α
xs : x ∈ s
cx : c < x
xb : x ≤ b
⊢ False

Tactic:
not_lt_of_ge (le_csSup Sbd ⟨xs, le_trans (le_csSup Sbd ha) (le_of_lt cx), xb⟩) cx

Premises used: le_of_lt, And.intro, le_csSup, le_trans, not_lt_of_ge
-- 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
x : α
xs : x ∈ s
cx : c < x
xb : x ≤ b
⊢ False

Tactic:
exact not_lt_of_ge (le_csSup Sbd ⟨xs, le_trans (le_csSup Sbd ha) (le_of_lt cx), xb⟩) cx

Premises used: le_of_lt, And.intro, le_csSup, le_trans, not_lt_of_ge
-- 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
hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty
y : α
hy : y ∈ Icc a b
suffices : s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y
⊢ IsClosed[inst] (s ∩ Icc a y)

Tactic:
suffices s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y from this ▸ hs.inter isClosed_Icc
-- 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
hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty
y : α
hy : y ∈ Icc a b
⊢ s ∩ Icc a y = s ∩ Icc a b ∩ Icc a y

Tactic:
grind [inter_assoc, inter_eq_self_of_subset_right, Icc_subset_Icc_right]

Premises used: Set.Icc_subset_Icc_right, Set.inter_eq_self_of_subset_right, Set.inter_assoc
-- 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
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)

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]
-- 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
hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty
y : α
hy : y ∈ Icc a b
this : IsClosed[inst] (s ∩ Icc a y)
⊢ y ∈ s

Tactic:
IsClosed.mem_of_ge_of_forall_exists_gt this ha hy.1 fun x hx ↦
    hgt x ⟨hx.1, Ico_subset_Ico_right hy.2 hx.2⟩ y hx.2.2

Premises used: And.right, And.left, And.intro, IsClosed.mem_of_ge_of_forall_exists_gt, Set.Ico_subset_Ico_right
-- 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
hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty
y : α
hy : y ∈ Icc a b
this : IsClosed[inst] (s ∩ Icc a y)
⊢ y ∈ s

Tactic:
exact IsClosed.mem_of_ge_of_forall_exists_gt this ha hy.1 fun x hx ↦
    hgt x ⟨hx.1, Ico_subset_Ico_right hy.2 hx.2⟩ y hx.2.2

Premises used: And.right, And.left, And.intro, IsClosed.mem_of_ge_of_forall_exists_gt, Set.Ico_subset_Ico_right
-- 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)
hb : b ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
this : Membership.mem (α := αᵒᵈ) (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ)
⊢ a ∈ s

Tactic:
aesop
-- 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)
hb : b ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
suffices : Membership.mem (α := αᵒᵈ) (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ)
⊢ a ∈ s

Tactic:
suffices OrderDual.toDual a ∈ ofDual ⁻¹' s by aesop
-- 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)
hb : b ∈ s
hab : a ≤ b
hgt : ∀ x ∈ s ∩ Ioc a b, (s ∩ Ico a x).Nonempty
⊢ IsClosed[instTopologicalSpace] ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' (s ∩ Icc a b))

Tactic:
have : IsClosed (OrderDual.ofDual ⁻¹' (s ∩ Icc a b)) := hs
-- 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)
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))
⊢ IsClosed[instTopologicalSpace]
    ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ)

Tactic:
rw [preimage_inter, ← Icc_toDual] at this

Premises used: Set.preimage_inter, Set.Icc_toDual
-- 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)
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 : α) → αᵒᵈ) b : αᵒᵈ)

Tactic:
simp_all
-- 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)
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 αᵒᵈ)
⊢ LE.le (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ)

Tactic:
simp_all
-- 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)
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 αᵒᵈ)
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
⊢ Membership.mem (α := αᵒᵈ) (γ := Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ)

Tactic:
apply this.mem_of_ge_of_forall_exists_gt (by simp_all) (by simp_all) (fun x hx ↦ ?_)

Premises used: IsClosed.mem_of_ge_of_forall_exists_gt
-- 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)
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
⊢ ∃ 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

Premises used: Set.preimage_inter, Set.mem_image, Set.Ico_toDual, Equiv.image_symm_eq_preimage
-- 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)
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 : ∃ x_1 ∈ s ∩ Ioc a b, (Equiv.symm ofDual : (a : α) → αᵒᵈ) x_1 = x
⊢ ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s ∩ Ioc x ((toDual : (a : α) → αᵒᵈ) a)).Nonempty

Tactic:
aesop
-- 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)
hb : b ∈ s
hgt : ∀ x ∈ s ∩ Ioc a b, ∀ y ∈ Iio x, (s ∩ Ico y x).Nonempty
y : α
hy : y ∈ Icc a b
suffices : s ∩ Icc y b = s ∩ Icc a b ∩ Icc y b
⊢ IsClosed[inst] (s ∩ Icc y b)

Tactic:
suffices s ∩ Icc y b = s ∩ Icc a b ∩ Icc y b from this ▸ hs.inter isClosed_Icc
-- 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)
hb : b ∈ s
hgt : ∀ x ∈ s ∩ Ioc a b, ∀ y ∈ Iio x, (s ∩ Ico y x).Nonempty
y : α
hy : y ∈ Icc a b
⊢ s ∩ Icc y b = s ∩ Icc a b ∩ Icc y b

Tactic:
grind [Icc_subset_Icc_left, inter_eq_self_of_subset_right, inter_assoc]

Premises used: Set.Icc_subset_Icc_left, Set.inter_eq_self_of_subset_right, Set.inter_assoc
-- 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)
hb : b ∈ s
hgt : ∀ x ∈ s ∩ Ioc a b, ∀ y ∈ Iio x, (s ∩ Ico y x).Nonempty
y : α
hy : y ∈ Icc a b
⊢ IsClosed[inst] (s ∩ Icc y b)

Tactic:
have : IsClosed (s ∩ Icc y b) := by
    suffices s ∩ Icc y b = s ∩ Icc a b ∩ Icc y b from this ▸ hs.inter isClosed_Icc
    grind [Icc_subset_Icc_left, inter_eq_self_of_subset_right, inter_assoc]
-- 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)
hb : b ∈ s
hgt : ∀ x ∈ s ∩ Ioc a b, ∀ y ∈ Iio x, (s ∩ Ico y x).Nonempty
y : α
hy : y ∈ Icc a b
this : IsClosed[inst] (s ∩ Icc y b)
⊢ y ∈ s

Tactic:
IsClosed.mem_of_ge_of_forall_exists_lt this hb hy.2 fun x hx ↦
    hgt x ⟨hx.1, Ioc_subset_Ioc_left hy.1 hx.2⟩ y hx.2.1

Premises used: Set.Ioc_subset_Ioc_left, IsClosed.mem_of_ge_of_forall_exists_lt, And.right, And.left, And.intro
-- 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)
hb : b ∈ s
hgt : ∀ x ∈ s ∩ Ioc a b, ∀ y ∈ Iio x, (s ∩ Ico y x).Nonempty
y : α
hy : y ∈ Icc a b
this : IsClosed[inst] (s ∩ Icc y b)
⊢ y ∈ s

Tactic:
exact IsClosed.mem_of_ge_of_forall_exists_lt this hb hy.2 fun x hx ↦
    hgt x ⟨hx.1, Ioc_subset_Ioc_left hy.1 hx.2⟩ y hx.2.1

Premises used: Set.Ioc_subset_Ioc_left, IsClosed.mem_of_ge_of_forall_exists_lt, And.right, And.left, And.intro
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
inl : ∀ (hab : b < a), Icc a b ⊆ s
inr : ∀ (hab : a ≤ b), Icc a b ⊆ s
⊢ Icc a b ⊆ s

Tactic:
rcases lt_or_ge b a with hab | hab

Premises used: lt_or_ge
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : b < a
⊢ Icc a b ⊆ s

Tactic:
simp_all
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t : α | t ∈ Icc a b ∧ Icc a t ⊆ s}
⊢ Icc a a ⊆ s

Tactic:
simp [ha]
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t : α | t ∈ Icc a b ∧ Icc a t ⊆ s}
⊢ a ∈ A

Tactic:
have a_mem : a ∈ A := ⟨left_mem_Icc.mpr hab, by simp [ha]⟩
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t : α | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
⊢ BddAbove A

Tactic:
have bdd_A : BddAbove A := ⟨b, fun t ht ↦ ht.1.2⟩
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t : α | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
⊢ t₁ ∈ Icc a b

Tactic:
have t₁_mem : t₁ ∈ Icc a b := ⟨le_csSup bdd_A a_mem, csSup_le ⟨a, a_mem⟩ (fun t ht ↦ ht.1.2)⟩
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t : α | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
⊢ t₁ ∈ A

Tactic:
⟨t₁_mem, fun t ht ↦ ?_⟩

Premises used: Set.Mem, setOf, And.intro
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t : α | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
refine : ∀ (t : α) (ht : t ∈ Icc a t₁), t ∈ s
⊢ t₁ ∈ A

Tactic:
refine ⟨t₁_mem, fun t ht ↦ ?_⟩
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t : α | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
t : α
ht : t ∈ Icc a t₁
inl : ∀ (ht : t₁ ∈ Icc a t₁), t₁ ∈ s
inr : ∀ (h : t < t₁), t ∈ s
⊢ t ∈ s

Tactic:
rcases ht.2.eq_or_lt with rfl | h

Premises used: LE.le.eq_or_lt, And.right, rfl
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t : α | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht : t₁ ∈ Icc a t₁
apply : ∀ (t : α) (ht : t ∈ A), t ∈ s
⊢ closure[inst] A ⊆ s ∩ Icc a b

Tactic:
apply (closure_subset_iff hs).2 (fun t ht ↦ ⟨?_, ht.1⟩)

Premises used: Iff.mpr, IsClosed.closure_subset_iff, And.intro
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t : α | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht_1 : t₁ ∈ Icc a t₁
t : α
ht : t ∈ A
⊢ t ∈ Icc a t

Tactic:
have : t ∈ Icc a t := ⟨ht.1.1, le_rfl⟩
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t : α | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht_1 : t₁ ∈ Icc a t₁
t : α
ht : t ∈ A
this : t ∈ Icc a t
⊢ t ∈ s

Tactic:
ht.2 this

Premises used: And.right
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t : α | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht_1 : t₁ ∈ Icc a t₁
t : α
ht : t ∈ A
this : t ∈ Icc a t
⊢ t ∈ s

Tactic:
exact ht.2 this

Premises used: And.right
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t : α | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht : t₁ ∈ Icc a t₁
⊢ closure[inst] A ⊆ s ∩ Icc a b

Tactic:
have : closure A ⊆ s ∩ Icc a b := by
        apply (closure_subset_iff hs).2 (fun t ht ↦ ⟨?_, ht.1⟩)
        have : t ∈ Icc a t := ⟨ht.1.1, le_rfl⟩
        exact ht.2 this
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t : α | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht : t₁ ∈ Icc a t₁
this : closure[inst] A ⊆ s ∩ Icc a b
inl : t₁ ∈ closure[inst] A
⊢ t₁ ∈ s

Tactic:
apply this.trans inter_subset_left

Premises used: HasSubset.Subset.trans, Set.inter_subset_left
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t : α | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht : t₁ ∈ Icc a t₁
this : closure[inst] A ⊆ s ∩ Icc a b
⊢ t₁ ∈ closure[inst] A

Tactic:
csSup_mem_closure ⟨a, a_mem⟩ bdd_A

Premises used: Set.Mem, Exists.intro, csSup_mem_closure
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t : α | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
ht : t₁ ∈ Icc a t₁
this : closure[inst] A ⊆ s ∩ Icc a b
⊢ t₁ ∈ closure[inst] A

Tactic:
exact csSup_mem_closure ⟨a, a_mem⟩ bdd_A

Premises used: Exists.intro, csSup_mem_closure
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h_1 : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t : α | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
t : α
ht : t ∈ Icc a t₁
h : t < t₁
⊢ ∃ c ∈ A, t < c

Tactic:
(lt_csSup_iff bdd_A ⟨a, a_mem⟩).1 h

Premises used: lt_csSup_iff, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst] (s ∩ Icc a b)
ha : a ∈ s
h_1 : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
hab : a ≤ b
A : Set α := {t : α | t ∈ Icc a b ∧ Icc a t ⊆ s}
a_mem : a ∈ A
bdd_A : BddAbove A
t₁ : α := sSup A
t₁_mem : t₁ ∈ Icc a b
t : α
ht : t ∈ Icc a t₁
h : t < t₁
inr : ∀ (c : α) (cA : c ∈ A) (tc : t < c), t ∈ s
⊢ t ∈ s

Tactic:
obtain ⟨c, cA, tc⟩ : ∃ c ∈ A, t < c := (lt_csSup_iff bdd_A ⟨a, a_mem⟩).1 h

Premises used: lt_csSup_iff, Exists.intro, Iff.mp