Remove line from proof

ericluap · Nov 6, 2024 · da05b71 · da05b71
1 parent 2fc2318
commit da05b71
Showing 1 changed file with 0 additions and 1 deletion.
diff --git 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