-- Mathlib/Order/Interval/Set/Basic.lean
theorem mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset {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} : Set (Set α))

Proof state:
case neg.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∉ s
⊢ s ⊆ Ico a b

Tactic:
rw [← Icc_diff_right]

Result:
case neg.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∉ s
⊢ s ⊆ Icc a b \ {b}

Proof state:
case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
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}

Tactic:
refine Or.inr <| Or.inr <| Or.inr <| Subset.antisymm ?_ ho

Result:
case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∉ s
hb : b ∉ s
⊢ s ⊆ Ioo a b

Proof state:
case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∉ s
hb : b ∉ s
⊢ s ⊆ (Icc a b \ {b}) \ {a}

Tactic:
apply_rules [subset_diff_singleton]

Result:
no goals

Proof state:
case neg.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∉ s
⊢ s ⊆ Icc a b \ {b}

Tactic:
exact subset_diff_singleton hc hb

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
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}

Tactic:
by_cases ha : a ∈ s <;> by_cases hb : b ∈ s

Result:
case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
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
inst✝ : PartialOrder α
a b : α
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
inst✝ : PartialOrder α
a b : α
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
inst✝ : PartialOrder α
a b : α
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}

Proof state:
case pos.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∉ s
hb : b ∈ s
⊢ s ⊆ Ioc a b

Tactic:
rw [← Icc_diff_left]

Result:
case pos.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∉ s
hb : b ∈ s
⊢ s ⊆ Icc a b \ {a}

Proof state:
case pos.refine_2
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∉ s
hb : b ∈ s
⊢ Ioc a b ⊆ s

Tactic:
rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s

Tactic:
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

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
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}

Tactic:
refine Or.inl (Subset.antisymm hc ?_)

Result:
case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∈ s
⊢ Icc a b ⊆ s

Proof state:
case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
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}

Tactic:
refine Or.inr <| Or.inl <| Subset.antisymm ?_ ?_

Result:
case neg.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
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
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∉ s
⊢ Ico a b ⊆ s

Proof state:
case pos.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∉ s
hb : b ∈ s
⊢ s ⊆ Icc a b \ {a}

Tactic:
exact subset_diff_singleton hc ha

Result:
no goals

Proof state:
case neg.refine_2
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : b ∉ s
⊢ Ico a b ⊆ s

Tactic:
rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] at ho

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∉ s
hb : b ∉ s
⊢ s ⊆ Ioo a b

Tactic:
rw [← Ico_diff_left, ← Icc_diff_right]

Result:
case neg
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∉ s
hb : b ∉ s
⊢ s ⊆ (Icc a b \ {b}) \ {a}

Proof state:
case pos
α : Type u_1
inst✝ : PartialOrder α
a b : α
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}

Tactic:
refine Or.inr <| Or.inr <| Or.inl <| Subset.antisymm ?_ ?_

Result:
case pos.refine_1
α : Type u_1
inst✝ : PartialOrder α
a b : α
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
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∉ s
hb : b ∈ s
⊢ Ioc a b ⊆ s