chore(Order/WithBot): add to_dual attributes (part 2)

Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

@@ -278,7 +278,7 @@ lemma unbot_le_iff (hx : x ≠ 0) : unzero hx ≤ b ↔ x ≤ b := WithBot.unbot
 @[simp, norm_cast] lemma coe_le_one [One α] : (a : WithZero α) ≤ 1 ↔ a ≤ 1 := coe_le_coe
 
 @[simp] lemma unzero_le_unzero (hx : x ≠ 0) (hy : y ≠ 0) : unzero hx ≤ unzero hy ↔ x ≤ y :=
-  WithBot.unbot_le_unbot ..
+  WithBot.unbot_le_unbot_iff ..
 
 end LE
 

Mathlib/Order/BoundedOrder/Basic.lean

@@ -245,6 +245,7 @@ end OrderBot
   denoted `⊤` and `⊥` respectively. -/
 class BoundedOrder (α : Type u) [LE α] extends OrderTop α, OrderBot α
 
+attribute [to_dual self (reorder := 3 4)] BoundedOrder.mk
 attribute [to_dual existing] BoundedOrder.toOrderTop
 
 instance OrderDual.instBoundedOrder (α : Type u) [LE α] [BoundedOrder α] : BoundedOrder αᵒᵈ where

Mathlib/Order/Defs/PartialOrder.lean

@@ -48,6 +48,14 @@ class Preorder (α : Type*) extends LE α, LT α where
   lt := fun a b => a ≤ b ∧ ¬b ≤ a
   protected lt_iff_le_not_ge : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬b ≤ a := by intros; rfl
 
+@[to_dual existing mk]
+def Preorder.mk' [LE α] [LT α] (le_refl : ∀ a : α, a ≤ a)
+    (ge_trans : ∀ a b c : α, b ≤ a → c ≤ b → c ≤ a)
+    (lt_iff_le_not_ge : ∀ a b : α, b < a ↔ b ≤ a ∧ ¬a ≤ b) : Preorder α where
+  le_refl := le_refl
+  le_trans a b c h₁ h₂ := ge_trans c b a h₂ h₁
+  lt_iff_le_not_ge a b := lt_iff_le_not_ge b a
+
 instance [Preorder α] : Std.LawfulOrderLT α where
   lt_iff := Preorder.lt_iff_le_not_ge
 
@@ -178,6 +186,11 @@ section PartialOrder
 class PartialOrder (α : Type*) extends Preorder α where
   protected le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b
 
+@[to_dual existing mk]
+def PartialOrder.mk' [Preorder α] (le_antisymm : ∀ a b : α, b ≤ a → a ≤ b → a = b) :
+    PartialOrder α where
+  le_antisymm a b h₁ h₂ := (le_antisymm b a h₁ h₂).symm
+
 instance [PartialOrder α] : Std.IsPartialOrder α where
   le_antisymm := PartialOrder.le_antisymm