case pos
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

case neg
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

case pos
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}

case neg
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
by_cases ha : a ∈ s <;> by_cases hb : b ∈ s
case pos
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s
case pos
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
refine' Or.inl (Subset.antisymm hc _)
no goals
case pos
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s
rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha, ← Icc_diff_right,
  diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
case neg.refine'_1
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Ico a b

case neg.refine'_2
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ Ico a b ⊆ s
case neg
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
refine' Or.inr <| Or.inl <| Subset.antisymm _ _
case neg.refine'_1
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Icc a b \ {b}
case neg.refine'_1
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Ico a b
rw [← Icc_diff_right]
no goals
case neg.refine'_1
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Icc a b \ {b}
exact subset_diff_singleton hc hb
no goals
case neg.refine'_2
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ Ico a b ⊆ s
rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] at ho
case pos.refine'_1
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ⊆ Ioc a b

case pos.refine'_2
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ Ioc a b ⊆ s
case pos
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
refine' Or.inr <| Or.inr <| Or.inl <| Subset.antisymm _ _
case pos.refine'_1
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ⊆ Icc a b \ {a}
case pos.refine'_1
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ⊆ Ioc a b
rw [← Icc_diff_left]
no goals
case pos.refine'_1
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ s ⊆ Icc a b \ {a}
exact subset_diff_singleton hc ha
no goals
case pos.refine'_2
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ Ioc a b ⊆ s
rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
case neg
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Ioo a b
case neg
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ∈ {Icc a b, Ico a b, Ioc a b, Ioo a b}
refine' Or.inr <| Or.inr <| Or.inr <| Subset.antisymm _ ho
case neg
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ (Icc a b \ {b}) \ {a}
case neg
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Ioo a b
rw [← Ico_diff_left, ← Icc_diff_right]
no goals
case neg
α : Type u_1
β : Type ?u.49808
inst✝ : PartialOrder α
a b c : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ (Icc a b \ {b}) \ {a}
apply_rules [subset_diff_singleton]