α✝ : Type ?u.935
β : Type ?u.938
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → Ioo x y ⊆ s
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≤ y → Icc x y ⊆ s
α✝ : Type ?u.935
β : Type ?u.938
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → Ioo x y ⊆ s
⊢ OrdConnected s
rw [ordConnected_iff]
α✝ : Type ?u.935
β : Type ?u.938
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ Icc x y ⊆ s
α✝ : Type ?u.935
β : Type ?u.938
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → Ioo x y ⊆ s
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≤ y → Icc x y ⊆ s
intro x hx y hy hxy
case inl
α✝ : Type ?u.935
β : Type ?u.938
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → Ioo x y ⊆ s
x : α
hx hy : x ∈ s
hxy : x ≤ x
⊢ Icc x x ⊆ s

case inr
α✝ : Type ?u.935
β : Type ?u.938
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
⊢ Icc x y ⊆ s
α✝ : Type ?u.935
β : Type ?u.938
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ Icc x y ⊆ s
rcases eq_or_lt_of_le hxy with (rfl | hxy')
case inr
α✝ : Type ?u.935
β : Type ?u.938
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
⊢ insert x (insert y (Ioo x y)) ⊆ s
case inr
α✝ : Type ?u.935
β : Type ?u.938
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
⊢ Icc x y ⊆ s
rw [← Ioc_insert_left hxy, ← Ioo_insert_right hxy']
no goals
case inr
α✝ : Type ?u.935
β : Type ?u.938
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
⊢ insert x (insert y (Ioo x y)) ⊆ s
exact insert_subset.2 ⟨hx, insert_subset.2 ⟨hy, hs x hx y hy hxy'⟩⟩
no goals
case inl
α✝ : Type ?u.935
β : Type ?u.938
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → Ioo x y ⊆ s
x : α
hx hy : x ∈ s
hxy : x ≤ x
⊢ Icc x x ⊆ s
simpa