feat port: order.complete_lattice (#1053)

aba57d4d3dae35460225919dcd82fe91355162f9

~~Depends on #1040~~

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib.lean

@@ -336,6 +336,7 @@ import Mathlib.Order.BoundedOrder
 import Mathlib.Order.Bounds.Basic
 import Mathlib.Order.Bounds.OrderIso
 import Mathlib.Order.Compare
+import Mathlib.Order.CompleteLattice
 import Mathlib.Order.Directed
 import Mathlib.Order.Disjoint
 import Mathlib.Order.GameAdd

Mathlib/Algebra/Order/Group/Instances.lean

@@ -15,11 +15,11 @@ import Mathlib.Algebra.Order.Monoid.OrderDual
 variable {α : Type _}
 
 @[to_additive]
-instance [OrderedCommGroup α] : OrderedCommGroup αᵒᵈ :=
-  { OrderDual.instOrderedCommMonoidOrderDual, instGroupOrderDual with }
-#align order_dual.ordered_comm_group instOrderedCommGroupOrderDual
-#align order_dual.ordered_add_comm_group instOrderedAddCommGroupOrderDual
+instance OrderDual.orderedCommGroup [OrderedCommGroup α] : OrderedCommGroup αᵒᵈ :=
+  { OrderDual.orderedCommMonoid, instGroupOrderDual with }
+#align order_dual.ordered_comm_group OrderDual.orderedCommGroup
+#align order_dual.ordered_add_comm_group OrderDual.orderedAddCommGroup
 
 @[to_additive]
-instance [LinearOrderedCommGroup α] : LinearOrderedCommGroup αᵒᵈ :=
-  { instOrderedCommGroupOrderDual, OrderDual.instLinearOrderOrderDual α with }
+instance OrderDual.linearOrderedCommGroup [LinearOrderedCommGroup α] : LinearOrderedCommGroup αᵒᵈ :=
+  { OrderDual.orderedCommGroup, OrderDual.linearOrder α with }

Mathlib/Algebra/Order/Monoid/OrderDual.lean

@@ -78,11 +78,11 @@ instance covariantClass_swap_mul_lt [LT α] [Mul α]
 #align order_dual.covariant_class_swap_mul_lt OrderDual.covariantClass_swap_mul_lt
 
 @[to_additive]
-instance [OrderedCommMonoid α] : OrderedCommMonoid αᵒᵈ :=
-  { OrderDual.instPartialOrderOrderDual α, instCommMonoidOrderDual with
+instance orderedCommMonoid [OrderedCommMonoid α] : OrderedCommMonoid αᵒᵈ :=
+  { OrderDual.partialOrder α, instCommMonoidOrderDual with
     mul_le_mul_left := fun _ _ h c => mul_le_mul_left' h c }
-#align order_dual.ordered_comm_monoid OrderDual.instOrderedCommMonoidOrderDual
-#align order_dual.ordered_add_comm_monoid OrderDual.instOrderedAddCommMonoidOrderDual
+#align order_dual.ordered_comm_monoid OrderDual.orderedCommMonoid
+#align order_dual.ordered_add_comm_monoid OrderDual.orderedAddCommMonoid
 
 @[to_additive OrderDual.OrderedCancelAddCommMonoid.to_contravariantClass]
 instance OrderedCancelCommMonoid.to_contravariantClass [OrderedCancelCommMonoid α] :
@@ -99,16 +99,17 @@ instance OrderedCancelCommMonoid.to_contravariantClass [OrderedCancelCommMonoid
   OrderDual.OrderedCancelCommMonoid.to_contravariantClass
 
 @[to_additive]
-instance [OrderedCancelCommMonoid α] : OrderedCancelCommMonoid αᵒᵈ :=
-  { instOrderedCommMonoidOrderDual, @instCancelCommMonoidOrderDual α _ with
+instance orderedCancelCommMonoid [OrderedCancelCommMonoid α] : OrderedCancelCommMonoid αᵒᵈ :=
+  { OrderDual.orderedCommMonoid, @instCancelCommMonoidOrderDual α _ with
     le_of_mul_le_mul_left := fun _ _ _ : α => le_of_mul_le_mul_left' }
 
 @[to_additive]
-instance [LinearOrderedCancelCommMonoid α] : LinearOrderedCancelCommMonoid αᵒᵈ :=
-  { instLinearOrderOrderDual α, instOrderedCancelCommMonoidOrderDual with }
+instance linearOrderedCancelCommMonoid [LinearOrderedCancelCommMonoid α] :
+    LinearOrderedCancelCommMonoid αᵒᵈ :=
+  { OrderDual.linearOrder α, OrderDual.orderedCancelCommMonoid with }
 
 @[to_additive]
-instance [LinearOrderedCommMonoid α] : LinearOrderedCommMonoid αᵒᵈ :=
-  { instLinearOrderOrderDual α, instOrderedCommMonoidOrderDual with }
+instance linearOrderedCommMonoid [LinearOrderedCommMonoid α] : LinearOrderedCommMonoid αᵒᵈ :=
+  { OrderDual.linearOrder α, OrderDual.orderedCommMonoid with }
 
 end OrderDual

Mathlib/Order/Basic.lean

@@ -545,16 +545,16 @@ instance (α : Type _) [LE α] : LE αᵒᵈ :=
 instance (α : Type _) [LT α] : LT αᵒᵈ :=
   ⟨fun a b => @LT.lt α _ b a⟩
 
-instance (α : Type _) [Preorder α] : Preorder αᵒᵈ where
+instance preorder (α : Type _) [Preorder α] : Preorder αᵒᵈ where
   le_refl := fun _ ↦ le_refl _
   le_trans := fun _ _ _ hab hbc ↦ hbc.trans hab
   lt_iff_le_not_le := fun _ _ ↦ lt_iff_le_not_le
 
-instance (α : Type _) [PartialOrder α] : PartialOrder αᵒᵈ where
+instance partialOrder (α : Type _) [PartialOrder α] : PartialOrder αᵒᵈ where
   __ := inferInstanceAs (Preorder αᵒᵈ)
   le_antisymm := fun a b hab hba ↦ @le_antisymm α _ a b hba hab
 
-instance (α : Type _) [LinearOrder α] : LinearOrder αᵒᵈ where
+instance linearOrder (α : Type _) [LinearOrder α] : LinearOrder αᵒᵈ where
   __ := inferInstanceAs (PartialOrder αᵒᵈ)
   le_total     := λ a b : α => le_total b a
   max := fun a b ↦ (min a b : α)
@@ -563,19 +563,19 @@ instance (α : Type _) [LinearOrder α] : LinearOrder αᵒᵈ where
   max_def := fun a b ↦ show (min .. : α) = _ by rw [min_comm, min_def]; rfl
   decidable_le := (inferInstance : DecidableRel (λ a b : α => b ≤ a))
   decidable_lt := (inferInstance : DecidableRel (λ a b : α => b < a))
-#align order_dual.linear_order OrderDual.instLinearOrderOrderDual
+#align order_dual.linear_order OrderDual.linearOrder
 
 instance : ∀ [Inhabited α], Inhabited αᵒᵈ := λ [x: Inhabited α] => x
 
 
-theorem Preorder.dual_dual (α : Type _) [H : Preorder α] : instPreorderOrderDual αᵒᵈ = H :=
+theorem Preorder.dual_dual (α : Type _) [H : Preorder α] : OrderDual.preorder αᵒᵈ = H :=
   Preorder.ext fun _ _ ↦ Iff.rfl
 
 theorem partialOrder.dual_dual (α : Type _) [H : PartialOrder α] :
-    instPartialOrderOrderDual αᵒᵈ = H :=
+    OrderDual.partialOrder αᵒᵈ = H :=
   PartialOrder.ext fun _ _ ↦ Iff.rfl
 
-theorem linearOrder.dual_dual (α : Type _) [H : LinearOrder α] : instLinearOrderOrderDual αᵒᵈ = H :=
+theorem linearOrder.dual_dual (α : Type _) [H : LinearOrder α] : OrderDual.linearOrder αᵒᵈ = H :=
   LinearOrder.ext fun _ _ ↦ Iff.rfl
 
 end OrderDual