From 02beb48296c6978735b626fe7a23554c0d3c2595 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 2 Feb 2026 09:01:03 -0500
Subject: [PATCH] chore: `lake update` for 2026-02-02

---
 Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean | 3 +++
 lake-manifest.json                                     | 6 +++---
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean
index 971c4353..de64d08b 100644
--- a/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean
+++ b/Cslib/Logics/LinearLogic/CLL/PhaseSemantics/Basic.lean
@@ -11,6 +11,7 @@ public import Mathlib.Algebra.Group.Pointwise.Set.Basic
 public import Mathlib.Algebra.Group.Idempotent
 public import Mathlib.Data.Set.Basic
 public import Mathlib.Order.Closure
+public import Mathlib.Order.Defs.PartialOrder
 public import Cslib.Logics.LinearLogic.CLL.Basic
 
 @[expose] public section
@@ -157,6 +158,8 @@ instance : SetLike (Fact P) P where
   coe := Fact.carrier
   coe_injective' _ _ _ := by grind [cases Fact]
 
+instance : PartialOrder (Fact P) := PartialOrder.ofSetLike (Fact P) P
+
 instance : HasSubset (Fact P) :=
   ⟨fun A B => (A : Set P) ⊆ (B : Set P)⟩
 
diff --git a/lake-manifest.json b/lake-manifest.json
index 44be680b..81e9d07e 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d2c3d9b0b4b1b2ae1514347b11b2945c4cbb0df5",
+   "rev": "3735095a4f7df8ff4cf593fda4931844bee6acf0",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "875ad9d88ed684e39c16bdea260e6ecfa15afd60",
+   "rev": "a046f786a71218321831f28baffb067a1c056dd7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "cabbb5a025bfbbc50af9184ed2dfdde6ea4f53a7",
+   "rev": "1f22a4f44c1726b61fab3c2c75e0651f35c795dc",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",