From 3943c68981515ad8eae76e463553768db300973b Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Fri, 6 Feb 2026 18:34:10 -0500
Subject: [PATCH] chore: `lake update` for 2026-02-06

---
 Cslib/Foundations/Data/Relation.lean | 12 +++++-------
 lake-manifest.json                   |  6 +++---
 2 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/Cslib/Foundations/Data/Relation.lean b/Cslib/Foundations/Data/Relation.lean
index 9fd9005c77..6946819b8d 100644
--- a/Cslib/Foundations/Data/Relation.lean
+++ b/Cslib/Foundations/Data/Relation.lean
@@ -45,13 +45,11 @@ theorem TransGen.to_eqvGen (h : TransGen r a b) : EqvGen r a b := by
 theorem ReflTransGen.to_eqvGen (h : ReflTransGen r a b) : EqvGen r a b := by
   induction h <;> grind
 
--- TODO: topNamespace environment linter fails for CompRel.to_eqvGen
-@[nolint topNamespace]
-theorem _root_.CompRel.to_eqvGen (h : CompRel r a b) : EqvGen r a b := by
+theorem SymmGen.to_eqvGen (h : SymmGen r a b) : EqvGen r a b := by
   induction h <;> grind
 
 attribute [scoped grind →] ReflGen.to_eqvGen TransGen.to_eqvGen ReflTransGen.to_eqvGen
-  CompRel.to_eqvGen
+  SymmGen.to_eqvGen
 
 /-- The relation `r` 'up to' the relation `s`. -/
 def UpTo (r s : α → α → Prop) : α → α → Prop := Comp s (Comp r s)
@@ -381,13 +379,13 @@ theorem reflTransGen_mono_closed (h₁ : Subrelation r₁ r₂) (h₂ : Subrelat
   ext
   exact ⟨ReflTransGen.mono @h₁, reflTransGen_closed @h₂⟩
 
-lemma ReflGen.compRel_symm : ReflGen (CompRel r) a b → ReflGen (CompRel r) b a
+lemma ReflGen.compRel_symm : ReflGen (SymmGen r) a b → ReflGen (SymmGen r) b a
 | .refl => .refl
 | .single (.inl h) => .single (.inr h)
 | .single (.inr h) => .single (.inl h)
 
 @[simp, grind =]
-theorem reflTransGen_compRel : ReflTransGen (CompRel r) = EqvGen r := by
+theorem reflTransGen_compRel : ReflTransGen (SymmGen r) = EqvGen r := by
   ext a b
   constructor
   · intro h
@@ -402,7 +400,7 @@ theorem reflTransGen_compRel : ReflTransGen (CompRel r) = EqvGen r := by
     | rel _ _ ih => exact .single (.inl ih)
     | refl x => exact .refl
     | symm x y eq ih =>
-      rw [compRel_swap]
+      rw [symmGen_swap]
       exact reflTransGen_swap.mp ih
     | trans _ _ _ _ _ ih₁ ih₂ => exact ih₁.trans ih₂
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 81e9d07e6c..80720e872a 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3735095a4f7df8ff4cf593fda4931844bee6acf0",
+   "rev": "cb53e58ea430de47cd7260f808b50187cac6a61c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a046f786a71218321831f28baffb067a1c056dd7",
+   "rev": "14107dc03e4540e534621b3af3804c06dfd480f1",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1f22a4f44c1726b61fab3c2c75e0651f35c795dc",
+   "rev": "f0440aecee888582922e892d573b8726c09a1f6f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",