[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x < y → Ioo x y ⊆ s
⊢ OrdConnected s
[PROOFSTEP]
rw [ordConnected_iff]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
α : Type u_3
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
[PROOFSTEP]
intro x hx y hy hxy
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
α : Type u_3
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
[PROOFSTEP]
rcases eq_or_lt_of_le hxy with (rfl | hxy')
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
α : Type u_3
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
[PROOFSTEP]
simpa
[GOAL]
case inr
α✝ : Type u_1
β : Type u_2
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
α : Type u_3
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
[PROOFSTEP]
rw [← Ioc_insert_left hxy, ← Ioo_insert_right hxy']
[GOAL]
case inr
α✝ : Type u_1
β : Type u_2
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s✝ t : Set α✝
α : Type u_3
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
[PROOFSTEP]
exact insert_subset_iff.2 ⟨hx, insert_subset_iff.2 ⟨hy, hs x hx y hy hxy'⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t s : Set α
h : OrdConnected (↑ofDual ⁻¹' s)
⊢ OrdConnected s
[PROOFSTEP]
simpa only [ordConnected_def] using h.dual
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s t : Set α✝
α : Type u_3
inst✝ : PartialOrder α
a : α
⊢ OrdConnected {a}
[PROOFSTEP]
rw [← Icc_self]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s t : Set α✝
α : Type u_3
inst✝ : PartialOrder α
a : α
⊢ OrdConnected (Icc a a)
[PROOFSTEP]
exact ordConnected_Icc
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
E : Type u_3
inst✝ : OrderIsoClass E α β
e : E
s : Set α
hs : OrdConnected s
⊢ OrdConnected (↑e '' s)
[PROOFSTEP]
erw [(e : α ≃o β).image_eq_preimage]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
s✝ t : Set α
E : Type u_3
inst✝ : OrderIsoClass E α β
e : E
s : Set α
hs : OrdConnected s
⊢ OrdConnected (↑(OrderIso.symm ↑e) ⁻¹' s)
[PROOFSTEP]
apply ordConnected_preimage (e : α ≃o β).symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
E : Type u_3
inst✝ : OrderIsoClass E α β
e : E
⊢ OrdConnected (range ↑e)
[PROOFSTEP]
simp_rw [← image_univ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
s t : Set α
E : Type u_3
inst✝ : OrderIsoClass E α β
e : E
⊢ OrdConnected (↑e '' univ)
[PROOFSTEP]
exact ordConnected_image (e : α ≃o β)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t s : Set α
⊢ OrdConnected (↑ofDual ⁻¹' s) ↔ OrdConnected s
[PROOFSTEP]
simp_rw [ordConnected_def, toDual.surjective.forall, dual_Icc, Subtype.forall']
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s✝ t s : Set α
⊢ (∀ (x x_1 : { a // ↑toDual a ∈ ↑ofDual ⁻¹' s }), ↑ofDual ⁻¹' Icc ↑x_1 ↑x ⊆ ↑ofDual ⁻¹' s) ↔
    ∀ (x x_1 : { a // a ∈ s }), Icc ↑x ↑x_1 ⊆ s
[PROOFSTEP]
exact forall_swap
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x x_1 => x ≤ x_1) s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : α
hz : z ∈ Icc x y
⊢ z ∈ s
[PROOFSTEP]
obtain rfl := hs.eq hx hy (hz.1.trans hz.2)
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x x_1 => x ≤ x_1) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z ∈ Icc x x
⊢ z ∈ s
[PROOFSTEP]
rw [Icc_self, mem_singleton_iff] at hz 
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x x_1 => x ≤ x_1) s
x : α
hx : x ∈ s
z : α
hy : x ∈ s
hz : z = x
⊢ z ∈ s
[PROOFSTEP]
rwa [hz]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
h : ∀ (y : α), y ∈ s → [[x, y]] ⊆ s
y : α
hy : y ∈ s
z : α
hz : z ∈ s
⊢ [[y, x]] ∪ [[x, z]] = [[x, y]] ∪ [[x, z]]
[PROOFSTEP]
rw [uIcc_comm]
[GOAL]
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
hx : x ∈ s
⊢ OrdConnected s ↔ ∀ ⦃y : α⦄, y ∈ s → [[y, x]] ⊆ s
[PROOFSTEP]
simp_rw [ordConnected_iff_uIcc_subset_left hx, uIcc_comm]
