case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
x : α
⊢ x ∈ ↑e ⁻¹' Ici b ↔ x ∈ Ici (↑(symm e) b)
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
⊢ ↑e ⁻¹' Ici b = Ici (↑(symm e) b)
ext x
no goals
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
x : α
⊢ x ∈ ↑e ⁻¹' Ici b ↔ x ∈ Ici (↑(symm e) b)
simp [← e.le_iff_le]