diff --git a/Mathlib/Data/Set/Lattice.lean b/Mathlib/Data/Set/Lattice.lean
index d3d588ff6e..9ff06b86e7 100644
--- a/Mathlib/Data/Set/Lattice.lean
+++ b/Mathlib/Data/Set/Lattice.lean
@@ -1734,6 +1734,15 @@ theorem preimage_iUnion₂ {f : α → β} {s : ∀ i, κ i → Set β} :
     (f ⁻¹' ⋃ (i) (j), s i j) = ⋃ (i) (j), f ⁻¹' s i j := by simp_rw [preimage_iUnion]
 #align set.preimage_Union₂ Set.preimage_iUnion₂
 
+theorem image_sUnion {f : α → β} {s : Set (Set α)} : (f '' ⋃₀ s) = ⋃₀ (image f '' s) := by
+  ext b
+  simp only [mem_image, mem_sUnion, exists_prop, sUnion_image, mem_iUnion]
+  constructor
+  · rintro ⟨a, ⟨t, ht₁, ht₂⟩, rfl⟩
+    exact ⟨t, ht₁, a, ht₂, rfl⟩
+  · rintro ⟨t, ht₁, a, ht₂, rfl⟩
+    exact ⟨a, ⟨t, ht₁, ht₂⟩, rfl⟩
+
 @[simp]
 theorem preimage_sUnion {f : α → β} {s : Set (Set β)} : f ⁻¹' ⋃₀s = ⋃ t ∈ s, f ⁻¹' t := by
   rw [sUnion_eq_biUnion, preimage_iUnion₂]
diff --git a/Mathlib/Order/Closure.lean b/Mathlib/Order/Closure.lean
index 040af5edb2..a409b0fc14 100644
--- a/Mathlib/Order/Closure.lean
+++ b/Mathlib/Order/Closure.lean
@@ -80,6 +80,28 @@ instance [Preorder α] : OrderHomClass (ClosureOperator α) α α where
 
 initialize_simps_projections ClosureOperator (toFun → apply, IsClosed → isClosed)
 
+
+/-- If `c` is a closure operator on `α` and `e` an order-isomorphism
+between `α` and `β` then `e ∘ c ∘ e⁻¹` is a closure operator on `β`. -/
+@[simps apply]
+def conjBy {α β} [Preorder α] [Preorder β] (c : ClosureOperator α)
+    (e : α ≃o β) : ClosureOperator β where
+  toFun := e.conj c
+  IsClosed b := c.IsClosed (e.symm b)
+  monotone' _ _ h :=
+    (map_le_map_iff e).mpr <| c.monotone <| (map_le_map_iff e.symm).mpr h
+  le_closure' _ := e.symm_apply_le.mp (c.le_closure' _)
+  idempotent' _ :=
+    congrArg e <| Eq.trans (congrArg c (e.symm_apply_apply _)) (c.idempotent' _)
+  isClosed_iff := Iff.trans c.isClosed_iff e.eq_symm_apply
+
+lemma conjBy_refl {α} [Preorder α] (c : ClosureOperator α) :
+    c.conjBy (OrderIso.refl α) = c := rfl
+
+lemma conjBy_trans {α β γ} [Preorder α] [Preorder β] [Preorder γ]
+    (e₁ : α ≃o β) (e₂ : β ≃o γ) (c : ClosureOperator α) :
+    c.conjBy (e₁.trans e₂) = (c.conjBy e₁).conjBy e₂ := rfl
+
 section PartialOrder
 
 variable [PartialOrder α]
@@ -102,9 +124,8 @@ instance : Inhabited (ClosureOperator α) :=
 variable {α} [PartialOrder α] (c : ClosureOperator α)
 
 @[ext]
-theorem ext : ∀ c₁ c₂ : ClosureOperator α, (c₁ : α → α) = (c₂ : α → α) → c₁ = c₂ :=
-  DFunLike.coe_injective
-#align closure_operator.ext ClosureOperator.ext
+theorem ext : ∀ c₁ c₂ : ClosureOperator α, (∀ x, c₁ x = c₂ x) → c₁ = c₂ :=
+  DFunLike.ext
 
 /-- Constructor for a closure operator using the weaker idempotency axiom: `f (f x) ≤ f x`. -/
 @[simps]
@@ -195,6 +216,15 @@ theorem IsClosed.closure_le_iff (hy : c.IsClosed y) : c x ≤ y ↔ x ≤ y := b
 
 lemma closure_min (hxy : x ≤ y) (hy : c.IsClosed y) : c x ≤ y := hy.closure_le_iff.2 hxy
 
+lemma closure_isGLB (x : α) : IsGLB { y | x ≤ y ∧ c.IsClosed y } (c x) where
+  left _ := and_imp.mpr closure_min
+  right _ h := h ⟨c.le_closure x, c.isClosed_closure x⟩
+
+theorem ext_isClosed (c₁ c₂ : ClosureOperator α)
+    (h : ∀ x, c₁.IsClosed x ↔ c₂.IsClosed x) : c₁ = c₂ :=
+  ext c₁ c₂ <| fun x => IsGLB.unique (c₁.closure_isGLB x) <|
+    (Set.ext (and_congr_right' <| h ·)).substr (c₂.closure_isGLB x)
+
 /-- A closure operator is equal to the closure operator obtained by feeding `c.closed` into the
 `ofPred` constructor. -/
 theorem eq_ofPred_closed (c : ClosureOperator α) :
@@ -262,6 +292,11 @@ def ofCompletePred (p : α → Prop) (hsinf : ∀ s, (∀ a ∈ s, p a) → p (s
     (fun a ↦ hsinf _ <| forall_mem_range.2 fun b ↦ b.2.2)
     (fun a b hab hb ↦ iInf_le_of_le ⟨b, hab, hb⟩ le_rfl)
 
+theorem sInf_isClosed {c : ClosureOperator α} {S : Set α}
+    (H : ∀ x ∈ S, c.IsClosed x) : c.IsClosed (sInf S) :=
+  isClosed_iff_closure_le.mpr <| le_of_le_of_eq c.monotone.map_sInf_le <|
+    Eq.trans (biInf_congr (c.isClosed_iff.mp <| H · ·)) sInf_eq_iInf.symm
+
 @[simp]
 theorem closure_iSup_closure (f : ι → α) : c (⨆ i, c (f i)) = c (⨆ i, f i) :=
   le_antisymm (le_closure_iff.1 <| iSup_le fun i => c.monotone <| le_iSup f i) <|
@@ -279,6 +314,18 @@ end CompleteLattice
 
 end ClosureOperator
 
+/-- Conjugating `ClosureOperators` on `α` and on `β` by a fixed isomorphism
+`e : α ≃o β` gives an equivalence `ClosureOperator α ≃ ClosureOperator β`. -/
+@[simps apply symm_apply]
+def OrderIso.equivClosureOperator {α β} [Preorder α] [Preorder β] (e : α ≃o β) :
+    ClosureOperator α ≃ ClosureOperator β where
+  toFun     c := c.conjBy e
+  invFun    c := c.conjBy e.symm
+  left_inv  c := Eq.trans (c.conjBy_trans _ _).symm
+                 <| Eq.trans (congrArg _ e.self_trans_symm) c.conjBy_refl
+  right_inv c := Eq.trans (c.conjBy_trans _ _).symm
+                 <| Eq.trans (congrArg _ e.symm_trans_self) c.conjBy_refl
+
 /-! ### Lower adjoint -/
 
 
diff --git a/Mathlib/Order/Hom/Basic.lean b/Mathlib/Order/Hom/Basic.lean
index 927c319d23..7e8b4b1546 100644
--- a/Mathlib/Order/Hom/Basic.lean
+++ b/Mathlib/Order/Hom/Basic.lean
@@ -935,6 +935,40 @@ theorem symm_trans (e₁ : α ≃o β) (e₂ : β ≃o γ) : (e₁.trans e₂).s
   rfl
 #align order_iso.symm_trans OrderIso.symm_trans
 
+@[simp]
+theorem self_trans_symm (e : α ≃o β) : e.trans e.symm = OrderIso.refl α :=
+  RelIso.self_trans_symm e
+
+@[simp]
+theorem symm_trans_self (e : α ≃o β) : e.symm.trans e = OrderIso.refl β :=
+  RelIso.symm_trans_self e
+
+/-- An order isomorphism between the domains and codomains of two prosets of
+order homomorphisms gives an order isomorphism between the two function prosets. -/
+@[simps apply symm_apply]
+def arrowCongr {α β γ δ} [Preorder α] [Preorder β] [Preorder γ] [Preorder δ]
+    (f : α ≃o γ) (g : β ≃o δ) : (α →o β) ≃o (γ →o δ) where
+  toFun  p := .comp g <| .comp p f.symm
+  invFun p := .comp g.symm <| .comp p f
+  left_inv p := DFunLike.coe_injective <| by
+    change (g.symm ∘ g) ∘ p ∘ (f.symm ∘ f) = p
+    simp only [← DFunLike.coe_eq_coe_fn, ← OrderIso.coe_trans, Function.id_comp,
+               OrderIso.self_trans_symm, OrderIso.coe_refl, Function.comp_id]
+  right_inv p := DFunLike.coe_injective <| by
+    change (g ∘ g.symm) ∘ p ∘ (f ∘ f.symm) = p
+    simp only [← DFunLike.coe_eq_coe_fn, ← OrderIso.coe_trans, Function.id_comp,
+               OrderIso.symm_trans_self, OrderIso.coe_refl, Function.comp_id]
+  map_rel_iff' {p q} := by
+    simp only [Equiv.coe_fn_mk, OrderHom.le_def, OrderHom.comp_coe,
+               OrderHomClass.coe_coe, Function.comp_apply, map_le_map_iff]
+    exact Iff.symm f.forall_congr_left'
+
+/-- If `α` and `β` are order-isomorphic then the two orders of order-homomorphisms
+from `α` and `β` to themselves are order-isomorphic. -/
+@[simps! apply symm_apply]
+def conj {α β} [Preorder α] [Preorder β] (f : α ≃o β) : (α →o α) ≃ (β →o β) :=
+  arrowCongr f f
+
 /-- `Prod.swap` as an `OrderIso`. -/
 def prodComm : α × β ≃o β × α where
   toEquiv := Equiv.prodComm α β
diff --git a/Mathlib/Order/Hom/CompleteLattice.lean b/Mathlib/Order/Hom/CompleteLattice.lean
index 19b678c33e..a76ec75237 100644
--- a/Mathlib/Order/Hom/CompleteLattice.lean
+++ b/Mathlib/Order/Hom/CompleteLattice.lean
@@ -946,14 +946,8 @@ theorem setPreimage_comp (g : β → γ) (f : α → β) :
 
 end CompleteLatticeHom
 
-theorem Set.image_sSup {f : α → β} (s : Set (Set α)) : f '' sSup s = sSup (image f '' s) := by
-  ext b
-  simp only [sSup_eq_sUnion, mem_image, mem_sUnion, exists_prop, sUnion_image, mem_iUnion]
-  constructor
-  · rintro ⟨a, ⟨t, ht₁, ht₂⟩, rfl⟩
-    exact ⟨t, ht₁, a, ht₂, rfl⟩
-  · rintro ⟨t, ht₁, a, ht₂, rfl⟩
-    exact ⟨a, ⟨t, ht₁, ht₂⟩, rfl⟩
+theorem Set.image_sSup {f : α → β} (s : Set (Set α)) : f '' sSup s = sSup (image f '' s) :=
+  Set.image_sUnion
 #align set.image_Sup Set.image_sSup
 
 /-- Using `Set.image`, a function between types yields a `sSupHom` between their lattices of
diff --git a/Mathlib/Order/RelIso/Basic.lean b/Mathlib/Order/RelIso/Basic.lean
index 66da443e24..ba24ad0d2a 100644
--- a/Mathlib/Order/RelIso/Basic.lean
+++ b/Mathlib/Order/RelIso/Basic.lean
@@ -798,6 +798,14 @@ theorem symm_apply_rel (e : r ≃r s) {x y} : r (e.symm x) y ↔ s x (e y) := by
   rw [← e.map_rel_iff, e.apply_symm_apply]
 #align rel_iso.symm_apply_rel RelIso.symm_apply_rel
 
+@[simp]
+theorem self_trans_symm (e : r ≃r s) : e.trans e.symm = RelIso.refl r :=
+  ext e.symm_apply_apply
+
+@[simp]
+theorem symm_trans_self (e : r ≃r s) : e.symm.trans e = RelIso.refl s :=
+  ext e.apply_symm_apply
+
 protected theorem bijective (e : r ≃r s) : Bijective e :=
   e.toEquiv.bijective
 #align rel_iso.bijective RelIso.bijective