feat(order/*): a bunch of lemmas about order_iso (#8451)

src/data/equiv/basic.lean

@@ -391,7 +391,7 @@ e.symm.symm_image_image s
 e.surjective.image_preimage s
 
 @[simp] lemma preimage_image {α β} (e : α ≃ β) (s : set α) : e ⁻¹' (e '' s) = s :=
-set.preimage_image_eq s e.injective
+e.injective.preimage_image s
 
 protected lemma image_compl {α β} (f : equiv α β) (s : set α) :
   f '' sᶜ = (f '' s)ᶜ :=

src/order/bounds.lean

@@ -772,3 +772,26 @@ lemma is_lub.of_image [preorder α] [preorder β] {f : α → β} (hf : ∀ {x y
   {s : set α} {x : α} (hx : is_lub (f '' s) (f x)) :
   is_lub s x :=
 @is_glb.of_image (order_dual α) (order_dual β) _ _ f (λ x y, hf) _ _ hx
+
+namespace order_iso
+
+variables [preorder α] [preorder β]
+
+@[simp] lemma is_lub_image (f : α ≃o β) {s : set α} {x : β} :
+  is_lub (f '' s) x ↔ is_lub s (f.symm x) :=
+⟨λ h, is_lub.of_image (λ _ _, f.le_iff_le) ((f.apply_symm_apply x).symm ▸ h),
+  λ h, is_lub.of_image (λ _ _, f.symm.le_iff_le) $ (f.symm_image_image s).symm ▸ h⟩
+
+@[simp] lemma is_glb_image (f : α ≃o β) {s : set α} {x : β} :
+  is_glb (f '' s) x ↔ is_glb s (f.symm x) :=
+f.dual.is_lub_image
+
+@[simp] lemma is_lub_preimage (f : α ≃o β) {s : set β} {x : α} :
+  is_lub (f ⁻¹' s) x ↔ is_lub s (f x) :=
+by rw [← f.symm_symm, ← image_eq_preimage, is_lub_image]
+
+@[simp] lemma is_glb_preimage (f : α ≃o β) {s : set β} {x : α} :
+  is_glb (f ⁻¹' s) x ↔ is_glb s (f x) :=
+f.dual.is_lub_preimage
+
+end order_iso

src/order/rel_iso.lean

@@ -605,6 +605,27 @@ lemma symm_injective : injective (symm : (α ≃o β) → (β ≃o α)) :=
 
 @[simp] lemma to_equiv_symm (e : α ≃o β) : e.to_equiv.symm = e.symm.to_equiv := rfl
 
+@[simp] lemma symm_image_image (e : α ≃o β) (s : set α) : e.symm '' (e '' s) = s :=
+e.to_equiv.symm_image_image s
+
+@[simp] lemma image_symm_image (e : α ≃o β) (s : set β) : e '' (e.symm '' s) = s :=
+e.to_equiv.image_symm_image s
+
+lemma image_eq_preimage (e : α ≃o β) (s : set α) : e '' s = e.symm ⁻¹' s :=
+e.to_equiv.image_eq_preimage s
+
+@[simp] lemma preimage_symm_preimage (e : α ≃o β) (s : set α) : e ⁻¹' (e.symm ⁻¹' s) = s :=
+e.to_equiv.preimage_symm_preimage s
+
+@[simp] lemma symm_preimage_preimage (e : α ≃o β) (s : set β) : e.symm ⁻¹' (e ⁻¹' s) = s :=
+e.to_equiv.symm_preimage_preimage s
+
+@[simp] lemma image_preimage (e : α ≃o β) (s : set β) : e '' (e ⁻¹' s) = s :=
+e.to_equiv.image_preimage s
+
+@[simp] lemma preimage_image (e : α ≃o β) (s : set α) : e ⁻¹' (e '' s) = s :=
+e.to_equiv.preimage_image s
+
 /-- Composition of two order isomorphisms is an order isomorphism. -/
 @[trans] def trans (e : α ≃o β) (e' : β ≃o γ) : α ≃o γ := e.trans e'
 
@@ -631,6 +652,9 @@ protected lemma strict_mono (e : α ≃o β) : strict_mono e := e.to_order_embed
 @[simp] lemma lt_iff_lt (e : α ≃o β) {x y : α} : e x < e y ↔ x < y :=
 e.to_order_embedding.lt_iff_lt
 
+lemma le_symm_apply (e : α ≃o β) {x : α} {y : β} : x ≤ e.symm y ↔ e x ≤ y :=
+e.rel_symm_apply
+
 /-- To show that `f : α → β`, `g : β → α` make up an order isomorphism of linear orders,
     it suffices to prove `cmp a (g b) = cmp (f a) b`. --/
 def of_cmp_eq_cmp {α β} [linear_order α] [linear_order β] (f : α → β) (g : β → α)

src/order/semiconj_Sup.lean

@@ -29,7 +29,7 @@ homeomorphisms of the circle, so in order to apply results from this file one ha
 homeomorphisms to the real line first.
 -/
 
-variables {α : Type*} {β : Type*}
+variables {α β γ : Type*}
 
 open set
 
@@ -44,20 +44,39 @@ lemma is_order_right_adjoint_Sup [complete_lattice α] [preorder β] (f : α →
 λ y, is_lub_Sup _
 
 lemma is_order_right_adjoint_cSup [conditionally_complete_lattice α] [preorder β] (f : α → β)
-  (hne : ∀ y, ∃ x, f x ≤ y) (hbdd : ∀ y, ∃ b, ∀ x, f x ≤ y → x ≤ b) :
+  (hne : ∀ y, ∃ x, f x ≤ y) (hbdd : ∀ y, bdd_above {x | f x ≤ y}) :
   is_order_right_adjoint f (λ y, Sup {x | f x ≤ y}) :=
 λ y, is_lub_cSup (hne y) (hbdd y)
 
-lemma is_order_right_adjoint.unique [partial_order α] [preorder β] {f : α → β} {g₁ g₂ : β → α}
+namespace is_order_right_adjoint
+
+protected lemma unique [partial_order α] [preorder β] {f : α → β} {g₁ g₂ : β → α}
   (h₁ : is_order_right_adjoint f g₁) (h₂ : is_order_right_adjoint f g₂) :
   g₁ = g₂ :=
 funext $ λ y, (h₁ y).unique (h₂ y)
 
-lemma is_order_right_adjoint.right_mono [preorder α] [preorder β] {f : α → β} {g : β → α}
+lemma right_mono [preorder α] [preorder β] {f : α → β} {g : β → α}
   (h : is_order_right_adjoint f g) :
   monotone g :=
 λ y₁ y₂ hy, (h y₁).mono (h y₂) $ λ x hx, le_trans hx hy
 
+lemma order_iso_comp [preorder α] [preorder β] [preorder γ] {f : α → β} {g : β → α}
+  (h : is_order_right_adjoint f g) (e : β ≃o γ) :
+  is_order_right_adjoint (e ∘ f) (g ∘ e.symm) :=
+λ y, by simpa [e.le_symm_apply] using h (e.symm y)
+
+lemma comp_order_iso [preorder α] [preorder β] [preorder γ] {f : α → β} {g : β → α}
+  (h : is_order_right_adjoint f g) (e : γ ≃o α) :
+  is_order_right_adjoint (f ∘ e) (e.symm ∘ g) :=
+begin
+  intro y,
+  change is_lub (e ⁻¹' {x | f x ≤ y}) (e.symm (g y)),
+  rw [e.is_lub_preimage, e.apply_symm_apply],
+  exact h y
+end
+
+end is_order_right_adjoint
+
 namespace function
 
 /-- If an order automorphism `fa` is semiconjugate to an order embedding `fb` by a function `g`