chore: bump mathlib to 73b2611, fix breaking changes (#640)

Bump `mathlib` dependency to
[73b2611](leanprover-community/mathlib4@73b2611):
chore(Order/Defs/Unbundled): deprecate `def Symmetric` in favor of
`class Std.Symm` (#38092) (2026-06-10)
Previously at:
[8589236](leanprover-community/mathlib4@8589236):
chore: move Data/Nat/Lattice to Order (#39990) (2026-06-09)

Closes #639

Failure log from the validation run:
[download](https://github.com/leanprover-community/downstream-reports/actions/runs/27427486135/artifacts/7596930467)
_(link expires after 1 year)_

---

This PR bumps `mathlib` to an identified incompatible (first-known-bad)
commit (`73b2611`) so you can reproduce and fix the incompatibility
locally by checking out this branch.

_Opened automatically by
[downstream-reports/track-incompatibility](https://github.com/leanprover-community/downstream-reports)
via [this workflow
run](https://github.com/leanprover/cslib/actions/runs/27442101619)._

---------

Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: Chris Henson <chrishenson.net@gmail.com>

Author: mathlib-nightly-testing[bot]

Cslib/Foundations/Data/Relation.lean

@@ -138,8 +138,6 @@ abbrev MJoin (r : α → α → Prop) := Join (ReflTransGen r)
 theorem MJoin.refl (a : α) : MJoin r a a := by
   use a
 
-theorem MJoin.symm : Symmetric (MJoin r) := Relation.symmetric_join
-
 theorem MJoin.single (h : ReflTransGen r a b) : MJoin r a b := by
   use b
 
@@ -420,7 +418,7 @@ theorem Confluent.toChurchRosser (h : Confluent r) : ChurchRosser r := by
   induction h_eqv with
   | rel _ b => exists b; grind [ReflTransGen.single]
   | refl a => exists a
-  | symm a b _ ih => exact symmetric_join ih
+  | symm a b _ ih => exact symm ih
   | trans _ _ _ _ _ ih1 ih2 =>
       obtain ⟨u, _, hbu⟩ := ih1
       obtain ⟨v, hbv, _⟩ := ih2
@@ -681,10 +679,8 @@ abbrev StronglyConfluent (r : α → α → Prop) :=
 def Commute (r₁ r₂ : α → α → Prop) := ∀ {x y₁ y₂},
   ReflTransGen r₁ x y₁ → ReflTransGen r₂ x y₂ → ∃ z, ReflTransGen r₂ y₁ z ∧ ReflTransGen r₁ y₂ z
 
-theorem Commute.symmetric : Symmetric (@Commute α) := by
-  intro r₁ r₂ h x y₁ y₂ x_y₁ x_y₂
-  obtain ⟨_, _, _⟩ := h x_y₂ x_y₁
-  grind
+instance : Std.Symm (@Commute α) where
+  symm r₁ r₂ h x y₁ y₂ x_y₁ x_y₂ := by grind [h x_y₂ x_y₁]
 
 theorem Commute.toConfluent : Commute r r = Confluent r := rfl
 
@@ -760,7 +756,7 @@ theorem Commute.join_confluent (c₁ : Confluent r₁) (c₂ : Confluent r₂) (
   induction ab generalizing c with
   | refl => exists c
   | @tail x y ax xy ih =>
-    have h_comm : Commute (r₁ ⊔ r₂) (r₁ ⊔ r₂) := by apply_rules [join_left, symmetric]
+    have h_comm : Commute (r₁ ⊔ r₂) (r₁ ⊔ r₂) := by apply_rules [join_left, symm]
     obtain ⟨z, xz, cz⟩ := ih ac
     obtain ⟨w, yw, zw⟩ := h_comm (.single xy) xz
     exact ⟨w, yw, cz.trans zw⟩

Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBetaEtaConfluence.lean

@@ -96,7 +96,8 @@ theorem confluent_beta_eta : Confluent (@FullBetaEta Var) := by
   apply join_confluent
   · exact confluence_beta
   · exact stronglyConfluent_eta.toConfluent
-  exact symmetric stronglyCommute_eta_beta.toCommute
+  apply symm
+  exact stronglyCommute_eta_beta.toCommute
 
 end LambdaCalculus.LocallyNameless.Untyped.Term
 

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8589236b8b8cc82492e3306df39c0fb308e0523c",
+   "rev": "73b2611ac34fe053446b21322ee51d19cb27b3e7",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "8589236b8b8cc82492e3306df39c0fb308e0523c",
+   "inputRev": "73b2611ac34fe053446b21322ee51d19cb27b3e7",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0bbac0a875ac0fd9366cb5bd4211da92d960ac84",
+   "rev": "5dd219c775e402f818b42cd3997b5cf21017babf",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.toml

@@ -18,7 +18,7 @@ weak.linter.unicodeLinter = false
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "8589236b8b8cc82492e3306df39c0fb308e0523c"
+rev = "73b2611ac34fe053446b21322ee51d19cb27b3e7"
 
 [[lean_lib]]
 name = "Cslib"