[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
⊢ ↑e ⁻¹' Iic b = Iic (↑(symm e) b)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
x : α
⊢ x ∈ ↑e ⁻¹' Iic b ↔ x ∈ Iic (↑(symm e) b)
[PROOFSTEP]
simp [← e.le_iff_le]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
⊢ ↑e ⁻¹' Ici b = Ici (↑(symm e) b)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
x : α
⊢ x ∈ ↑e ⁻¹' Ici b ↔ x ∈ Ici (↑(symm e) b)
[PROOFSTEP]
simp [← e.le_iff_le]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
⊢ ↑e ⁻¹' Iio b = Iio (↑(symm e) b)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
x : α
⊢ x ∈ ↑e ⁻¹' Iio b ↔ x ∈ Iio (↑(symm e) b)
[PROOFSTEP]
simp [← e.lt_iff_lt]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
⊢ ↑e ⁻¹' Ioi b = Ioi (↑(symm e) b)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
x : α
⊢ x ∈ ↑e ⁻¹' Ioi b ↔ x ∈ Ioi (↑(symm e) b)
[PROOFSTEP]
simp [← e.lt_iff_lt]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : β
⊢ ↑e ⁻¹' Icc a b = Icc (↑(symm e) a) (↑(symm e) b)
[PROOFSTEP]
simp [← Ici_inter_Iic]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : β
⊢ ↑e ⁻¹' Ico a b = Ico (↑(symm e) a) (↑(symm e) b)
[PROOFSTEP]
simp [← Ici_inter_Iio]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : β
⊢ ↑e ⁻¹' Ioc a b = Ioc (↑(symm e) a) (↑(symm e) b)
[PROOFSTEP]
simp [← Ioi_inter_Iic]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : β
⊢ ↑e ⁻¹' Ioo a b = Ioo (↑(symm e) a) (↑(symm e) b)
[PROOFSTEP]
simp [← Ioi_inter_Iio]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a : α
⊢ ↑e '' Iic a = Iic (↑e a)
[PROOFSTEP]
rw [e.image_eq_preimage, e.symm.preimage_Iic, e.symm_symm]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a : α
⊢ ↑e '' Iio a = Iio (↑e a)
[PROOFSTEP]
rw [e.image_eq_preimage, e.symm.preimage_Iio, e.symm_symm]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ ↑e '' Ioo a b = Ioo (↑e a) (↑e b)
[PROOFSTEP]
rw [e.image_eq_preimage, e.symm.preimage_Ioo, e.symm_symm]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ ↑e '' Ioc a b = Ioc (↑e a) (↑e b)
[PROOFSTEP]
rw [e.image_eq_preimage, e.symm.preimage_Ioc, e.symm_symm]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ ↑e '' Ico a b = Ico (↑e a) (↑e b)
[PROOFSTEP]
rw [e.image_eq_preimage, e.symm.preimage_Ico, e.symm_symm]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ ↑e '' Icc a b = Icc (↑e a) (↑e b)
[PROOFSTEP]
rw [e.image_eq_preimage, e.symm.preimage_Icc, e.symm_symm]
[GOAL]
α : Type ?u.15052
inst✝¹ : Preorder α
inst✝ : OrderTop α
src✝ : Subtype (Iic ⊤) ≃ α := Equiv.subtypeUnivEquiv (_ : ∀ (x : α), x ≤ ⊤)
x y : ↑(Iic ⊤)
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        x ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        y ↔
    x ≤ y
[PROOFSTEP]
rfl
[GOAL]
α : Type ?u.15647
inst✝¹ : Preorder α
inst✝ : OrderBot α
src✝ : Subtype (Ici ⊥) ≃ α := Equiv.subtypeUnivEquiv (_ : ∀ (x : α), ⊥ ≤ x)
x y : ↑(Ici ⊥)
⊢ ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        x ≤
      ↑{ toFun := src✝.toFun, invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        y ↔
    x ≤ y
[PROOFSTEP]
rfl
