From da05b71c9182fb4319a7acbe20760e45fef005b9 Mon Sep 17 00:00:00 2001
From: Eric <eric.1334@icloud.com>
Date: Wed, 6 Nov 2024 14:03:52 -0800
Subject: [PATCH] Remove line from proof

---
 OrderedSemigroups/OrderedGroup/Basic.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/OrderedSemigroups/OrderedGroup/Basic.lean b/OrderedSemigroups/OrderedGroup/Basic.lean
index eca3fa1..7b3d465 100644
--- a/OrderedSemigroups/OrderedGroup/Basic.lean
+++ b/OrderedSemigroups/OrderedGroup/Basic.lean
@@ -32,7 +32,6 @@ theorem pos_neg_disjoint :
     Disjoint (SetLike.coe (PositiveCone α)) (SetLike.coe (NegativeCone α)) := by
   simp [Disjoint, PositiveCone, NegativeCone]
   intro S S_subset_pos S_subset_neg
-  unfold_projs at *
   ext x
   constructor
   · intro x_in_S