chore(Order/Defs/Unbundled): deprecate def AntiSymmetric in favor of class Std.Antisymm (leanprover-community#35025)

Author: SnirBroshi

Mathlib/Analysis/Convex/Extreme.lean

@@ -89,13 +89,13 @@ protected theorem IsExtreme.trans (hAB : IsExtreme 𝕜 A B) (hBC : IsExtreme 
     (hAB.left_mem_of_mem_openSegment hx₁A hx₂A (hBC.subset hxC) hx)
     (hAB.right_mem_of_mem_openSegment hx₁A hx₂A (hBC.subset hxC) hx) hxC hx
 
-protected theorem IsExtreme.antisymm : AntiSymmetric (IsExtreme 𝕜 : Set E → Set E → Prop) :=
-  fun _ _ hAB hBA ↦ Subset.antisymm hBA.1 hAB.1
+protected theorem IsExtreme.antisymm : Std.Antisymm (IsExtreme 𝕜 : Set E → Set E → Prop) :=
+  ⟨fun _ _ hAB hBA ↦ Subset.antisymm hBA.1 hAB.1⟩
 
 instance : IsPartialOrder (Set E) (IsExtreme 𝕜) where
   refl := IsExtreme.refl 𝕜
   trans _ _ _ := IsExtreme.trans
-  antisymm := IsExtreme.antisymm
+  __ := IsExtreme.antisymm
 
 theorem IsExtreme.inter (hAB : IsExtreme 𝕜 A B) (hAC : IsExtreme 𝕜 A C) :
     IsExtreme 𝕜 A (B ∩ C) := by

Mathlib/ModelTheory/Order.lean

@@ -327,7 +327,7 @@ instance model_partialOrder [PartialOrder M] [L.OrderedStructure M] :
   simp only [partialOrderTheory, Theory.model_insert_iff, Relations.realize_antisymmetric,
     relMap_leSymb, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one,
     model_preorder, and_true]
-  exact fun _ _ => le_antisymm
+  infer_instance
 
 section LinearOrder
 
@@ -382,8 +382,8 @@ def preorderOfModels [h : M ⊨ L.preorderTheory] : Preorder M where
 /-- Any model of a theory of partial orders is a partial order. -/
 def partialOrderOfModels [h : M ⊨ L.partialOrderTheory] : PartialOrder M where
   __ := L.preorderOfModels M
-  le_antisymm := Relations.realize_antisymmetric.1 ((Theory.model_iff _).1 h _
-    (by simp only [partialOrderTheory, Set.mem_insert_iff, true_or]))
+  le_antisymm := (Relations.realize_antisymmetric.mp <|
+    Theory.model_iff _ |>.mp h _ <| by simp [partialOrderTheory]).antisymm
 
 /-- Any model of a theory of linear orders is a linear order. -/
 def linearOrderOfModels [h : M ⊨ L.linearOrderTheory]

Mathlib/ModelTheory/Semantics.lean

@@ -967,9 +967,9 @@ theorem realize_symmetric : M ⊨ r.symmetric ↔ Symmetric fun x y : M => RelMa
 
 @[simp]
 theorem realize_antisymmetric :
-    M ⊨ r.antisymmetric ↔ AntiSymmetric fun x y : M => RelMap r ![x, y] :=
-  forall_congr' fun _ =>
-    forall_congr' fun _ => imp_congr realize_rel₂ (imp_congr realize_rel₂ Iff.rfl)
+    M ⊨ r.antisymmetric ↔ Std.Antisymm fun x y : M => RelMap r ![x, y] := by
+  refine .trans ?_ ⟨Std.Antisymm.mk, (·.antisymm)⟩
+  exact forall₂_congr fun _ _ ↦ imp_congr realize_rel₂ <| imp_congr realize_rel₂ .rfl
 
 @[simp]
 theorem realize_transitive : M ⊨ r.transitive ↔ Transitive fun x y : M => RelMap r ![x, y] :=

Mathlib/Order/Defs/Unbundled.lean

@@ -188,6 +188,7 @@ def Transitive := ∀ ⦃x y z⦄, x ≺ y → y ≺ z → x ≺ z
 def Irreflexive := ∀ x, ¬x ≺ x
 
 /-- `Std.Antisymm` as a definition, suitable for use in proofs. -/
+@[deprecated Std.Antisymm (since := "2026-02-09")]
 def AntiSymmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x → x = y
 
 /-- `Std.Total` as a definition, suitable for use in proofs. -/