awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hab : Icc a b ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
inl : ∀ (h : x ≤ y), (Icc a b ∩ (s ∩ t)).Nonempty
inr : ∀ (h : y ≤ x), (Icc a b ∩ (s ∩ t)).Nonempty
⊢ (Icc a b ∩ (s ∩ t)).Nonempty

Tactic:
rcases le_total x y with h | h

Premises used: le_total
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hab : Icc a b ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : x ≤ y
⊢ (Icc a b ∩ (s ∩ t)).Nonempty

Tactic:
isPreconnected_Icc_aux x y s t h hs ht hab hx hy

Premises used: isPreconnected_Icc_aux
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hab : Icc a b ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : x ≤ y
⊢ (Icc a b ∩ (s ∩ t)).Nonempty

Tactic:
exact isPreconnected_Icc_aux x y s t h hs ht hab hx hy

Premises used: isPreconnected_Icc_aux
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hab : Icc a b ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : y ≤ x
inr : (Icc a b ∩ (t ∩ s)).Nonempty
⊢ (Icc a b ∩ (s ∩ t)).Nonempty

Tactic:
rw [inter_comm s t]

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hab : Icc a b ⊆ s ∪ t
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : y ≤ x
inr :
  ∀ (hab : Icc a b ⊆ t ∪ s) (x : α) (hx : x ∈ Icc a b ∩ s) (y : α) (hy : y ∈ Icc a b ∩ t) (h : y ≤ x),
    (Icc a b ∩ (t ∩ s)).Nonempty
⊢ (Icc a b ∩ (t ∩ s)).Nonempty

Tactic:
rw [union_comm s t] at hab

Premises used: Set.union_comm
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hab : Icc a b ⊆ t ∪ s
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : y ≤ x
⊢ (Icc a b ∩ (t ∩ s)).Nonempty

Tactic:
isPreconnected_Icc_aux y x t s h ht hs hab hy hx

Premises used: isPreconnected_Icc_aux
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
s t : Set α
hs : IsClosed[inst] s
ht : IsClosed[inst] t
hab : Icc a b ⊆ t ∪ s
x : α
hx : x ∈ Icc a b ∩ s
y : α
hy : y ∈ Icc a b ∩ t
h : y ≤ x
⊢ (Icc a b ∩ (t ∩ s)).Nonempty

Tactic:
exact isPreconnected_Icc_aux y x t s h ht hs hab hy hx

Premises used: isPreconnected_Icc_aux
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
⊢ IsPreconnected [[a, b]]

Tactic:
isPreconnected_Icc

Premises used: isPreconnected_Icc, Set.uIcc
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
h : s.OrdConnected
⊢ IsPreconnected s

Tactic:
isPreconnected_of_forall_pair fun x hx y hy =>
    ⟨[[x, y]], h.uIcc_subset hx hy, left_mem_uIcc, right_mem_uIcc, isPreconnected_uIcc⟩

Premises used: Set.OrdConnected.uIcc_subset, Set.right_mem_uIcc, Set.left_mem_uIcc, isPreconnected_uIcc, And.intro, Exists.intro, Set.uIcc, isPreconnected_of_forall_pair
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
⊢ IsPreconnected s ↔ s.OrdConnected

Tactic:
⟨IsPreconnected.ordConnected, Set.OrdConnected.isPreconnected⟩

Premises used: Set.OrdConnected.isPreconnected, IsPreconnected.ordConnected, Iff.intro
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
⊢ IsPreconnected (Ici a)

Tactic:
ordConnected_Ici.isPreconnected

Premises used: Set.ordConnected_Ici, Set.OrdConnected.isPreconnected
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
⊢ IsPreconnected (Iic a)

Tactic:
ordConnected_Iic.isPreconnected

Premises used: Set.ordConnected_Iic, Set.OrdConnected.isPreconnected
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
⊢ IsPreconnected (Iio a)

Tactic:
ordConnected_Iio.isPreconnected

Premises used: Set.OrdConnected.isPreconnected, Set.ordConnected_Iio
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
⊢ IsPreconnected (Ioi a)

Tactic:
ordConnected_Ioi.isPreconnected

Premises used: Set.ordConnected_Ioi, Set.OrdConnected.isPreconnected
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
⊢ IsPreconnected (Ioo a b)

Tactic:
ordConnected_Ioo.isPreconnected

Premises used: Set.OrdConnected.isPreconnected, Set.ordConnected_Ioo
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
⊢ IsPreconnected (uIoo a b)

Tactic:
isPreconnected_Ioo

Premises used: isPreconnected_Ioo, Set.uIoo
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
⊢ IsPreconnected (Ioc a b)

Tactic:
ordConnected_Ioc.isPreconnected

Premises used: Set.OrdConnected.isPreconnected, Set.ordConnected_Ioc
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
⊢ IsPreconnected (Ι a b)

Tactic:
isPreconnected_Ioc

Premises used: Set.uIoc, isPreconnected_Ioc
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
⊢ IsPreconnected (Ico a b)

Tactic:
ordConnected_Ico.isPreconnected

Premises used: Set.ordConnected_Ico, Set.OrdConnected.isPreconnected
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
⊢ IsConnected (Ici a)

Tactic:
⟨nonempty_Ici, isPreconnected_Ici⟩

Premises used: isPreconnected_Ici, IsConnected, And.intro, Set.nonempty_Ici
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
⊢ IsConnected (Iic a)

Tactic:
⟨nonempty_Iic, isPreconnected_Iic⟩

Premises used: IsConnected, isPreconnected_Iic, And.intro, Set.nonempty_Iic
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
inst_4 : NoMaxOrder α
⊢ IsConnected (Ioi a)

Tactic:
⟨nonempty_Ioi, isPreconnected_Ioi⟩

Premises used: IsConnected, isPreconnected_Ioi, Set.nonempty_Ioi, And.intro
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a : α
inst_4 : NoMinOrder α
⊢ IsConnected (Iio a)

Tactic:
⟨nonempty_Iio, isPreconnected_Iio⟩

Premises used: IsConnected, isPreconnected_Iio, And.intro, Set.nonempty_Iio
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : a ≤ b
⊢ IsConnected (Icc a b)

Tactic:
⟨nonempty_Icc.2 h, isPreconnected_Icc⟩

Premises used: Iff.mpr, IsConnected, Set.nonempty_Icc, isPreconnected_Icc, And.intro
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : a < b
⊢ IsConnected (Ioo a b)

Tactic:
⟨nonempty_Ioo.2 h, isPreconnected_Ioo⟩

Premises used: Iff.mpr, IsConnected, Set.nonempty_Ioo, isPreconnected_Ioo, And.intro
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : a ≠ b
⊢ IsConnected (uIoo a b)

Tactic:
⟨nonempty_uIoo.2 h, isPreconnected_uIoo⟩

Premises used: Iff.mpr, isPreconnected_uIoo, IsConnected, Set.nonempty_uIoo, And.intro
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : a < b
⊢ IsConnected (Ioc a b)

Tactic:
⟨nonempty_Ioc.2 h, isPreconnected_Ioc⟩

Premises used: Iff.mpr, Set.nonempty_Ioc, IsConnected, isPreconnected_Ioc, And.intro
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : a ≠ b
⊢ IsConnected (Ι a b)

Tactic:
⟨nonempty_uIoc.2 h, isPreconnected_uIoc⟩

Premises used: Iff.mpr, Set.nonempty_uIoc, IsConnected, And.intro, isPreconnected_uIoc
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
h : a < b
⊢ IsConnected (Ico a b)

Tactic:
⟨nonempty_Ico.2 h, isPreconnected_Ico⟩

Premises used: Iff.mpr, IsConnected, isPreconnected_Ico, Set.nonempty_Ico, And.intro
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
⊢ PreconnectedSpace α

Tactic:
⟨ordConnected_univ.isPreconnected⟩

Premises used: PreconnectedSpace.mk, Set.OrdConnected.isPreconnected, Set.ordConnected_univ
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
⊢ Eq (α := Set (Set α)) {s : Set α | IsPreconnected s}
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))

Tactic:
Subset.antisymm setOf_isPreconnected_subset_of_ordered ?_

Premises used: Set.Subset.antisymm, setOf_isPreconnected_subset_of_ordered
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
refine :
  Subset (α := Set (Set α))
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
    {s : Set α | IsPreconnected s}
⊢ Eq (α := Set (Set α)) {s : Set α | IsPreconnected s}
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))

Tactic:
refine Subset.antisymm setOf_isPreconnected_subset_of_ordered ?_

Premises used: Set.Subset.antisymm, setOf_isPreconnected_subset_of_ordered
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
⊢ Subset (α := Set (Set α))
    (range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅}))
    {s : Set α | IsPreconnected s}

Tactic:
simp only [subset_def, forall_mem_range, uncurry, or_imp, forall_and, mem_union,
    mem_setOf_eq, insert_eq, mem_singleton_iff, forall_eq, forall_true_iff, and_true,
    isPreconnected_Icc, isPreconnected_Ico, isPreconnected_Ioc, isPreconnected_Ioo,
    isPreconnected_Ioi, isPreconnected_Iio, isPreconnected_Ici, isPreconnected_Iic,
    isPreconnected_univ, isPreconnected_empty]

Premises used: Set.mem_union, isPreconnected_Ici, Set.insert_eq, Set.forall_mem_range, and_true, Set.subset_def, isPreconnected_Iic, forall_eq, isPreconnected_Icc, or_imp, Set.mem_setOf_eq, isPreconnected_Ioi, isPreconnected_Ico, isPreconnected_Ioc, isPreconnected_Ioo, Set.mem_singleton_iff, isPreconnected_Iio, isPreconnected_empty, forall_true_iff, PreconnectedSpace.isPreconnected_univ, Function.uncurry, forall_and
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
simp : (∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1) ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y
⊢ IsTotallyDisconnected s ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y

Tactic:
simp only [IsTotallyDisconnected, isPreconnected_iff_ordConnected, ← not_nontrivial_iff,
    nontrivial_iff_exists_lt, not_exists, not_and]

Premises used: isPreconnected_iff_ordConnected, not_exists, Set.not_nontrivial_iff, Set.nontrivial_iff_exists_lt, not_and, IsTotallyDisconnected
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
⊢ (∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1) ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y

Tactic:
⟨fun h x hx y hy hxy ↦ ?_, fun h t hts ht x hx y hy hxy ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
refine_1 :
  ∀ (h : ∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1) (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s)
    (hxy : x < y), ∃ z ∉ s, z ∈ Ioo x y
refine_2 :
  ∀ (h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y) (t : Set α) (hts : t ⊆ s) (ht : t.OrdConnected) (x : α)
    (hx : x ∈ t) (y : α) (hy : y ∈ t) (hxy : x < y), False
⊢ (∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1) ↔ ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y

Tactic:
refine ⟨fun h x hx y hy hxy ↦ ?_, fun h t hts ht x hx y hy hxy ↦ ?_⟩
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
h : ∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
refine_1 : ¬(s ∩ Icc x y).OrdConnected
⊢ ∃ z ∉ s, z ∈ Ioo x y

Tactic:
simp_rw [← not_ordConnected_inter_Icc_iff hx hy]

Premises used: Set.not_ordConnected_inter_Icc_iff
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
h : ∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
⊢ ¬(s ∩ Icc x y).OrdConnected

Tactic:
fun hs ↦ h _ inter_subset_left hs _ ⟨hx, le_rfl, hxy.le⟩ _ ⟨hy, hxy.le, le_rfl⟩ hxy

Premises used: le_rfl, LT.lt.le, Set.inter_subset_left, Inter.inter, Set.Icc, And.intro, Not
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
h : ∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
⊢ ¬(s ∩ Icc x y).OrdConnected

Tactic:
exact fun hs ↦ h _ inter_subset_left hs _ ⟨hx, le_rfl, hxy.le⟩ _ ⟨hy, hxy.le, le_rfl⟩ hxy
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y
t : Set α
hts : t ⊆ s
ht : t.OrdConnected
x : α
hx : x ∈ t
y : α
hy : y ∈ t
hxy : x < y
refine_2 : ∀ (z : α) (h1z : z ∉ s) (h2z : z ∈ Ioo x y), False
⊢ False

Tactic:
obtain ⟨z, h1z, h2z⟩ := h x (hts hx) y (hts hy) hxy
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y
t : Set α
hts : t ⊆ s
ht : t.OrdConnected
x : α
hx : x ∈ t
y : α
hy : y ∈ t
hxy : x < y
z : α
h1z : z ∉ s
h2z : z ∈ Ioo x y
⊢ False

Tactic:
h1z <| hts <| ht.1 hx hy ⟨h2z.1.le, h2z.2.le⟩

Premises used: LT.lt.le, And.right, And.left, Set.OrdConnected.out', And.intro
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
s : Set α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∉ s, z ∈ Ioo x y
t : Set α
hts : t ⊆ s
ht : t.OrdConnected
x : α
hx : x ∈ t
y : α
hy : y ∈ t
hxy : x < y
z : α
h1z : z ∉ s
h2z : z ∈ Ioo x y
⊢ False

Tactic:
exact h1z <| hts <| ht.1 hx hy ⟨h2z.1.le, h2z.2.le⟩

Premises used: LT.lt.le, And.right, And.left, Set.OrdConnected.out', And.intro
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
hab : a ≤ b
f : α → δ
hf : ContinuousOn f (Icc a b)
⊢ Icc (f a) (f b) ⊆ f '' Icc a b

Tactic:
isPreconnected_Icc.intermediate_value (left_mem_Icc.2 hab) (right_mem_Icc.2 hab) hf

Premises used: Iff.mpr, Set.right_mem_Icc, isPreconnected_Icc, Set.left_mem_Icc, IsPreconnected.intermediate_value
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
hab : a ≤ b
f : α → δ
hf : ContinuousOn f (Icc a b)
⊢ Icc (f b) (f a) ⊆ f '' Icc a b

Tactic:
isPreconnected_Icc.intermediate_value (right_mem_Icc.2 hab) (left_mem_Icc.2 hab) hf

Premises used: Iff.mpr, Set.right_mem_Icc, isPreconnected_Icc, Set.left_mem_Icc, IsPreconnected.intermediate_value
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hf : ContinuousOn f [[a, b]]
inl : f a ≤ f b → [[f a, f b]] ⊆ f '' [[a, b]]
inr : f b ≤ f a → [[f a, f b]] ⊆ f '' [[a, b]]
⊢ [[f a, f b]] ⊆ f '' [[a, b]]

Tactic:
cases le_total (f a) (f b)

Premises used: le_total
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hf : ContinuousOn f [[a, b]]
h : f a ≤ f b
⊢ [[f a, f b]] ⊆ f '' [[a, b]]

Tactic:
simp [*, isPreconnected_uIcc.intermediate_value]

Premises used: isPreconnected_uIcc, IsPreconnected.intermediate_value
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
f : α → δ
hf : ContinuousOn f [[a, b]]
h : f b ≤ f a
⊢ [[f a, f b]] ⊆ f '' [[a, b]]

Tactic:
simp [*, isPreconnected_uIcc.intermediate_value]

Premises used: isPreconnected_uIcc, IsPreconnected.intermediate_value
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
f : α → α
hf : ContinuousOn f [[a, b]]
ha : a ≤ f a
hb : f b ≤ b
⊢ ∃ c ∈ [[a, b]], IsFixedPt f c

Tactic:
isPreconnected_uIcc.intermediate_value₂ right_mem_uIcc left_mem_uIcc hf continuousOn_id hb ha

Premises used: Set.right_mem_uIcc, IsPreconnected.intermediate_value₂, Set.left_mem_uIcc, isPreconnected_uIcc, Function.IsFixedPt, continuousOn_id
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
f : α → α
hf : ContinuousOn f (Icc a b)
hle : a ≤ b
ha : a ≤ f a
hb : f b ≤ b
⊢ ∃ c ∈ Icc a b, IsFixedPt f c

Tactic:
isPreconnected_Icc.intermediate_value₂
    (right_mem_Icc.2 hle) (left_mem_Icc.2 hle) hf continuousOn_id hb ha

Premises used: Iff.mpr, Set.right_mem_Icc, IsPreconnected.intermediate_value₂, isPreconnected_Icc, Set.left_mem_Icc, Function.IsFixedPt, continuousOn_id
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
a b : α
f : α → α
hf : ContinuousOn f (Icc a b)
hle : a ≤ b
hmaps : MapsTo f (Icc a b) (Icc a b)
⊢ ∃ c ∈ Icc a b, IsFixedPt f c

Tactic:
exists_mem_Icc_isFixedPt hf hle (hmaps <| left_mem_Icc.2 hle).1 (hmaps <| right_mem_Icc.2 hle).2

Premises used: Iff.mpr, Set.right_mem_Icc, exists_mem_Icc_isFixedPt, And.right, And.left, Set.left_mem_Icc
-- Module: Mathlib.Topology.Order.IntermediateValue
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : OrderTopology α
inst_3 : DenselyOrdered α
δ : Type u_1
inst_4 : LinearOrder δ
inst_5 : TopologicalSpace δ
inst_6 : OrderClosedTopology δ
a b : α
hab : a ≤ b
f : α → δ
hf : ContinuousOn f (Icc a b)
⊢ Ico (f a) (f b) ⊆ f '' Ico a b

Tactic:
Or.elim (eq_or_lt_of_le hab) (fun he _ h => absurd h.2 (not_lt_of_ge (he ▸ h.1))) fun hlt =>
    @IsPreconnected.intermediate_value_Ico _ _ _ _ _ _ _ isPreconnected_Ico _ _ ⟨refl a, hlt⟩
      (right_nhdsWithin_Ico_neBot hlt) inf_le_right _ (hf.mono Ico_subset_Icc_self) _
      ((hf.continuousWithinAt ⟨hab, refl b⟩).mono Ico_subset_Icc_self)

Premises used: IsPreconnected.intermediate_value_Ico, Set.Ico_subset_Icc_self, inf_le_right, Eq.rec, isPreconnected_Ico, eq_or_lt_of_le, absurd, And.right, ContinuousWithinAt.mono, And.left, And.intro, ContinuousOn.mono, Or.elim, refl, ContinuousOn.continuousWithinAt, not_lt_of_ge