[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ range some = Iio ⊤
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝ : PartialOrder α
a b : α
x : WithTop α
⊢ x ∈ range some ↔ x ∈ Iio ⊤
[PROOFSTEP]
rw [mem_Iio, lt_top_iff_ne_top, mem_range, ← none_eq_top, Option.ne_none_iff_exists]
[GOAL]
case h
α : Type u_1
inst✝ : PartialOrder α
a b : α
x : WithTop α
⊢ (∃ y, ↑y = x) ↔ ∃ x_1, Option.some x_1 = x
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Icc ↑a ↑b = Icc a b
[PROOFSTEP]
simp [← Ici_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ico ↑a ↑b = Ico a b
[PROOFSTEP]
simp [← Ici_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ioc ↑a ↑b = Ioc a b
[PROOFSTEP]
simp [← Ioi_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ioo ↑a ↑b = Ioo a b
[PROOFSTEP]
simp [← Ioi_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Iio ⊤ = univ
[PROOFSTEP]
rw [← range_coe, preimage_range]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ico ↑a ⊤ = Ici a
[PROOFSTEP]
simp [← Ici_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ioo ↑a ⊤ = Ioi a
[PROOFSTEP]
simp [← Ioi_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ioi a = Ioo ↑a ⊤
[PROOFSTEP]
rw [← preimage_coe_Ioi, image_preimage_eq_inter_range, range_coe, Ioi_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ici a = Ico ↑a ⊤
[PROOFSTEP]
rw [← preimage_coe_Ici, image_preimage_eq_inter_range, range_coe, Ici_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Iio a = Iio ↑a
[PROOFSTEP]
rw [← preimage_coe_Iio, image_preimage_eq_inter_range, range_coe, inter_eq_self_of_subset_left (Iio_subset_Iio le_top)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Iic a = Iic ↑a
[PROOFSTEP]
rw [← preimage_coe_Iic, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Iic_subset_Iio.2 <| coe_lt_top a)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Icc a b = Icc ↑a ↑b
[PROOFSTEP]
rw [← preimage_coe_Icc, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Icc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ico a b = Ico ↑a ↑b
[PROOFSTEP]
rw [← preimage_coe_Ico, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Ico_subset_Iio_self <| Iio_subset_Iio le_top)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ioc a b = Ioc ↑a ↑b
[PROOFSTEP]
rw [← preimage_coe_Ioc, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Ioc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ioo a b = Ioo ↑a ↑b
[PROOFSTEP]
rw [← preimage_coe_Ioo, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Ioo_subset_Iio_self <| Iio_subset_Iio le_top)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Icc ↑a ↑b = Icc a b
[PROOFSTEP]
simp [← Ici_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ico ↑a ↑b = Ico a b
[PROOFSTEP]
simp [← Ici_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ioc ↑a ↑b = Ioc a b
[PROOFSTEP]
simp [← Ioi_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ioo ↑a ↑b = Ioo a b
[PROOFSTEP]
simp [← Ioi_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ioi ⊥ = univ
[PROOFSTEP]
rw [← range_coe, preimage_range]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ioc ⊥ ↑a = Iic a
[PROOFSTEP]
simp [← Ioi_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some ⁻¹' Ioo ⊥ ↑a = Iio a
[PROOFSTEP]
simp [← Ioi_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Iio a = Ioo ⊥ ↑a
[PROOFSTEP]
rw [← preimage_coe_Iio, image_preimage_eq_inter_range, range_coe, inter_comm, Ioi_inter_Iio]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Iic a = Ioc ⊥ ↑a
[PROOFSTEP]
rw [← preimage_coe_Iic, image_preimage_eq_inter_range, range_coe, inter_comm, Ioi_inter_Iic]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ioi a = Ioi ↑a
[PROOFSTEP]
rw [← preimage_coe_Ioi, image_preimage_eq_inter_range, range_coe, inter_eq_self_of_subset_left (Ioi_subset_Ioi bot_le)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ici a = Ici ↑a
[PROOFSTEP]
rw [← preimage_coe_Ici, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Ici_subset_Ioi.2 <| bot_lt_coe a)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Icc a b = Icc ↑a ↑b
[PROOFSTEP]
rw [← preimage_coe_Icc, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Icc_subset_Ici_self <| Ici_subset_Ioi.2 <| bot_lt_coe a)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ioc a b = Ioc ↑a ↑b
[PROOFSTEP]
rw [← preimage_coe_Ioc, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Ioc_subset_Ioi_self <| Ioi_subset_Ioi bot_le)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ico a b = Ico ↑a ↑b
[PROOFSTEP]
rw [← preimage_coe_Ico, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Ico_subset_Ici_self <| Ici_subset_Ioi.2 <| bot_lt_coe a)]
[GOAL]
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ some '' Ioo a b = Ioo ↑a ↑b
[PROOFSTEP]
rw [← preimage_coe_Ioo, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left (Subset.trans Ioo_subset_Ioi_self <| Ioi_subset_Ioi bot_le)]
