chore(Finsupp/Lex): syntactically better data fields in Partial/LinearOrder instances (leanprover-community#7229)

Author: alreadydone

Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean

@@ -239,9 +239,8 @@ example : ¬CovariantClass (Lex (F →₀ F)) (Lex (F →₀ F)) (· + ·) (· 
   refine (not_lt (α := Lex (F →₀ F))).mpr (@h (Finsupp.single (0 : F) (1 : F))
     (Finsupp.single 1 1) (Finsupp.single 0 1) ?_) ⟨1, ?_⟩
   · exact Or.inr ⟨0, by simp [(by boom : ∀ j : F, j < 0 ↔ False)]⟩
-  · simp only [(by boom : ∀ j : F, j < 1 ↔ j = 0), Function.comp, ofLex_add, toDFinsupp_add,
-      toLex_add, ofLex_toLex, DFinsupp.coe_add, toDFinsupp_coe, Pi.toLex_apply, Pi.add_apply,
-      forall_eq, f010, f1, f110, add_zero, f011, f111, zero_add, and_self]
+  · simp only [(by boom : ∀ j : F, j < 1 ↔ j = 0), ofLex_add, coe_add, Pi.add_apply, forall_eq,
+      f010, f1, f110, add_zero, f011, f111, zero_add, and_self]
 
 example {α} [Ring α] [Nontrivial α] : ∃ f g : AddMonoidAlgebra α F, f ≠ 0 ∧ g ≠ 0 ∧ f * g = 0 :=
   zero_divisors_of_periodic (1 : F) le_rfl (by simp [two_smul]) z01.ne'

Mathlib/Algebra/Order/Group/Prod.lean

@@ -34,7 +34,7 @@ instance orderedCommGroup [OrderedCommGroup G] [OrderedCommGroup H] :
 @[to_additive]
 instance linearOrderedCommGroup [LinearOrderedCommGroup G] [LinearOrderedCommGroup H] :
     LinearOrderedCommGroup (G ×ₗ H) where
-  __ := (inferInstance : LinearOrder (G ×ₗ H))
+  __ : LinearOrder (G ×ₗ H) := inferInstance
   mul_le_mul_left _ _ := mul_le_mul_left'
 
 end Lex

Mathlib/Algebra/Order/Monoid/Prod.lean

@@ -63,8 +63,8 @@ instance orderedCancelCommMonoid [OrderedCancelCommMonoid α] [OrderedCancelComm
 @[to_additive]
 instance linearOrderedCancelCommMonoid [LinearOrderedCancelCommMonoid α]
     [LinearOrderedCancelCommMonoid β] : LinearOrderedCancelCommMonoid (α ×ₗ β) where
-  __ := (inferInstance : LinearOrder (α ×ₗ β))
-  __ := (inferInstance : OrderedCancelCommMonoid (α ×ₗ β))
+  __ : LinearOrder (α ×ₗ β) := inferInstance
+  __ : OrderedCancelCommMonoid (α ×ₗ β) := inferInstance
 
 end Lex
 

Mathlib/Data/DFinsupp/Lex.lean

@@ -63,20 +63,22 @@ theorem lex_lt_of_lt [∀ i, PartialOrder (α i)] (r) [IsStrictOrder ι r] {x y
   exact lex_lt_of_lt_of_preorder r hlt
 #align dfinsupp.lex_lt_of_lt DFinsupp.lex_lt_of_lt
 
-instance Lex.isStrictOrder [LinearOrder ι] [∀ i, PartialOrder (α i)] :
+variable [LinearOrder ι]
+
+instance Lex.isStrictOrder [∀ i, PartialOrder (α i)] :
     IsStrictOrder (Lex (Π₀ i, α i)) (· < ·) :=
   let i : IsStrictOrder (Lex (∀ i, α i)) (· < ·) := Pi.Lex.isStrictOrder
   { irrefl := toLex.surjective.forall.2 fun _ ↦ @irrefl _ _ i.toIsIrrefl _
     trans := toLex.surjective.forall₃.2 fun _ _ _ ↦ @trans _ _ i.toIsTrans _ _ _ }
 #align dfinsupp.lex.is_strict_order DFinsupp.Lex.isStrictOrder
 
-variable [LinearOrder ι]
-
 /-- The partial order on `DFinsupp`s obtained by the lexicographic ordering.
 See `DFinsupp.Lex.linearOrder` for a proof that this partial order is in fact linear. -/
-instance Lex.partialOrder [∀ i, PartialOrder (α i)] : PartialOrder (Lex (Π₀ i, α i)) :=
-  PartialOrder.lift (fun x ↦ toLex (⇑(ofLex x)))
-    (FunLike.coe_injective (F := DFinsupp fun i => α i))
+instance Lex.partialOrder [∀ i, PartialOrder (α i)] : PartialOrder (Lex (Π₀ i, α i)) where
+  lt := (· < ·)
+  le x y := ⇑(ofLex x) = ⇑(ofLex y) ∨ x < y
+  __ := PartialOrder.lift (fun x : Lex (Π₀ i, α i) ↦ toLex (⇑(ofLex x)))
+    (FunLike.coe_injective (F := DFinsupp α))
 #align dfinsupp.lex.partial_order DFinsupp.Lex.partialOrder
 
 section LinearOrder
@@ -100,7 +102,7 @@ private def lt_trichotomy_rec {P : Lex (Π₀ i, α i) → Lex (Π₀ i, α i) 
 /-- The less-or-equal relation for the lexicographic ordering is decidable. -/
 irreducible_def Lex.decidableLE : @DecidableRel (Lex (Π₀ i, α i)) (· ≤ ·) :=
   lt_trichotomy_rec (fun h ↦ isTrue <| Or.inr h)
-    (fun h ↦ isTrue <| Or.inl <| congr_arg _ <| congr_arg _ h)
+    (fun h ↦ isTrue <| Or.inl <| congr_arg _ h)
     fun h ↦ isFalse fun h' ↦ lt_irrefl _ (h.trans_le h')
 #align dfinsupp.lex.decidable_le DFinsupp.Lex.decidableLE
 
@@ -111,16 +113,16 @@ irreducible_def Lex.decidableLT : @DecidableRel (Lex (Π₀ i, α i)) (· < ·)
 
 -- Porting note: Added `DecidableEq` for `LinearOrder`.
 instance : DecidableEq (Lex (Π₀ i, α i)) :=
-  lt_trichotomy_rec (fun h ↦ isFalse fun h' => h'.not_lt h) (fun h ↦ isTrue h)
-    fun h ↦ isFalse fun h' => h'.symm.not_lt h
+  lt_trichotomy_rec (fun h ↦ isFalse fun h' ↦ h'.not_lt h) isTrue
+    fun h ↦ isFalse fun h' ↦ h'.symm.not_lt h
 
 /-- The linear order on `DFinsupp`s obtained by the lexicographic ordering. -/
-instance Lex.linearOrder : LinearOrder (Lex (Π₀ i, α i)) :=
-  { Lex.partialOrder with
-    le_total := lt_trichotomy_rec (fun h ↦ Or.inl h.le) (fun h ↦ Or.inl h.le) fun h ↦ Or.inr h.le
-    decidableLT := decidableLT
-    decidableLE := decidableLE
-    decidableEq := inferInstance }
+instance Lex.linearOrder : LinearOrder (Lex (Π₀ i, α i)) where
+  __ := Lex.partialOrder
+  le_total := lt_trichotomy_rec (fun h ↦ Or.inl h.le) (fun h ↦ Or.inl h.le) fun h ↦ Or.inr h.le
+  decidableLT := decidableLT
+  decidableLE := decidableLE
+  decidableEq := inferInstance
 #align dfinsupp.lex.linear_order DFinsupp.Lex.linearOrder
 
 end LinearOrder
@@ -208,12 +210,12 @@ instance Lex.orderedAddCommGroup [∀ i, OrderedAddCommGroup (α i)] :
 instance Lex.linearOrderedCancelAddCommMonoid
     [∀ i, LinearOrderedCancelAddCommMonoid (α i)] :
     LinearOrderedCancelAddCommMonoid (Lex (Π₀ i, α i)) where
-  __ := (inferInstance : LinearOrder (Lex (Π₀ i, α i)))
-  __ := (inferInstance : OrderedCancelAddCommMonoid (Lex (Π₀ i, α i)))
+  __ : LinearOrder (Lex (Π₀ i, α i)) := inferInstance
+  __ : OrderedCancelAddCommMonoid (Lex (Π₀ i, α i)) := inferInstance
 
 instance Lex.linearOrderedAddCommGroup [∀ i, LinearOrderedAddCommGroup (α i)] :
     LinearOrderedAddCommGroup (Lex (Π₀ i, α i)) where
-  __ := (inferInstance : LinearOrder (Lex (Π₀ i, α i)))
+  __ : LinearOrder (Lex (Π₀ i, α i)) := inferInstance
   add_le_add_left _ _ := add_le_add_left
 
 end OrderedAddMonoid

Mathlib/Data/Finsupp/Lex.lean

@@ -73,14 +73,18 @@ variable [LinearOrder α]
 
 /-- The partial order on `Finsupp`s obtained by the lexicographic ordering.
 See `Finsupp.Lex.linearOrder` for a proof that this partial order is in fact linear. -/
-instance Lex.partialOrder [PartialOrder N] : PartialOrder (Lex (α →₀ N)) :=
-  PartialOrder.lift (fun x ↦ toLex (⇑(ofLex x))) (FunLike.coe_injective (F := Finsupp α N))
+instance Lex.partialOrder [PartialOrder N] : PartialOrder (Lex (α →₀ N)) where
+  lt := (· < ·)
+  le x y := ⇑(ofLex x) = ⇑(ofLex y) ∨ x < y
+  __ := PartialOrder.lift (fun x : Lex (α →₀ N) ↦ toLex (⇑(ofLex x)))
+    (FunLike.coe_injective (F := Finsupp α N))
 #align finsupp.lex.partial_order Finsupp.Lex.partialOrder
 
 /-- The linear order on `Finsupp`s obtained by the lexicographic ordering. -/
-instance Lex.linearOrder [LinearOrder N] : LinearOrder (Lex (α →₀ N)) :=
-  { @Lex.partialOrder α N _ _ _,  -- Porting note: Added types to avoid typeclass inference problem.
-    LinearOrder.lift' (toLex ∘ toDFinsupp ∘ ofLex) finsuppEquivDFinsupp.injective with }
+instance Lex.linearOrder [LinearOrder N] : LinearOrder (Lex (α →₀ N)) where
+  lt := (· < ·)
+  le := (· ≤ ·)
+  __ := LinearOrder.lift' (toLex ∘ toDFinsupp ∘ ofLex) finsuppEquivDFinsupp.injective
 #align finsupp.lex.linear_order Finsupp.Lex.linearOrder
 
 variable [PartialOrder N]
@@ -162,12 +166,12 @@ noncomputable instance Lex.orderedAddCommGroup [OrderedAddCommGroup N] :
 
 noncomputable instance Lex.linearOrderedCancelAddCommMonoid [LinearOrderedCancelAddCommMonoid N] :
     LinearOrderedCancelAddCommMonoid (Lex (α →₀ N)) where
-  __ := (inferInstance : LinearOrder (Lex (α →₀ N)))
-  __ := (inferInstance: OrderedCancelAddCommMonoid (Lex (α →₀ N)))
+  __ : LinearOrder (Lex (α →₀ N)) := inferInstance
+  __ : OrderedCancelAddCommMonoid (Lex (α →₀ N)) := inferInstance
 
 noncomputable instance Lex.linearOrderedAddCommGroup [LinearOrderedAddCommGroup N] :
     LinearOrderedAddCommGroup (Lex (α →₀ N)) where
-  __ := (inferInstance : LinearOrder (Lex (α →₀ N)))
+  __ : LinearOrder (Lex (α →₀ N)) := inferInstance
   add_le_add_left _ _ := add_le_add_left
 
 end OrderedAddMonoid

Mathlib/Data/Pi/Lex.lean

@@ -245,14 +245,14 @@ instance Lex.orderedCommGroup [∀ i, OrderedCommGroup (β i)] :
 noncomputable instance Lex.linearOrderedCancelCommMonoid [IsWellOrder ι (· < ·)]
     [∀ i, LinearOrderedCancelCommMonoid (β i)] :
     LinearOrderedCancelCommMonoid (Lex (∀ i, β i)) where
-  __ := (inferInstance : LinearOrder (Lex (∀ i, β i)))
-  __ := (inferInstance: OrderedCancelCommMonoid (Lex (∀ i, β i)))
+  __ : LinearOrder (Lex (∀ i, β i)) := inferInstance
+  __ : OrderedCancelCommMonoid (Lex (∀ i, β i)) := inferInstance
 
 @[to_additive]
 noncomputable instance Lex.linearOrderedCommGroup [IsWellOrder ι (· < ·)]
     [∀ i, LinearOrderedCommGroup (β i)] :
     LinearOrderedCommGroup (Lex (∀ i, β i)) where
-  __ := (inferInstance : LinearOrder (Lex (∀ i, β i)))
+  __ : LinearOrder (Lex (∀ i, β i)) := inferInstance
   mul_le_mul_left _ _ := mul_le_mul_left'
 
 end OrderedMonoid