diff --git a/Mathlib/CategoryTheory/Shift/Adjunction.lean b/Mathlib/CategoryTheory/Shift/Adjunction.lean
index d1a9ba68aa2ef..8f6a5a6ddc1f9 100644
--- a/Mathlib/CategoryTheory/Shift/Adjunction.lean
+++ b/Mathlib/CategoryTheory/Shift/Adjunction.lean
@@ -197,8 +197,8 @@ The property for `CommShift` structures on `F` and `G` to be compatible with an
 adjunction `F ⊣ G`.
 -/
 class CommShift : Prop where
-  commShift_unit' : NatTrans.CommShift adj.unit A := by infer_instance
-  commShift_counit' : NatTrans.CommShift adj.counit A := by infer_instance
+  commShift_unit : NatTrans.CommShift adj.unit A := by infer_instance
+  commShift_counit : NatTrans.CommShift adj.counit A := by infer_instance
 
 open CommShift in
 attribute [instance] commShift_unit commShift_counit
@@ -229,7 +229,7 @@ namespace CommShift
 /-- Constructor for `Adjunction.CommShift`. -/
 lemma mk' (h : NatTrans.CommShift adj.unit A) :
     adj.CommShift A where
-  commShift_counit' := ⟨fun a ↦ by
+  commShift_counit := ⟨fun a ↦ by
     ext
     simp only [Functor.comp_obj, Functor.id_obj, NatTrans.comp_app,
       Functor.commShiftIso_comp_hom_app, whiskerRight_app, assoc, whiskerLeft_app,
@@ -512,8 +512,8 @@ instance [h : E.inverse.CommShift A] : E.symm.functor.CommShift A := h
 /-- Constructor for `Equivalence.CommShift`. -/
 lemma mk' (h : NatTrans.CommShift E.unitIso.hom A) :
     E.CommShift A where
-  commShift_unit' := h
-  commShift_counit' := (Adjunction.CommShift.mk' E.toAdjunction A h).commShift_counit
+  commShift_unit := h
+  commShift_counit := (Adjunction.CommShift.mk' E.toAdjunction A h).commShift_counit
 
 /--
 The forward functor of the identity equivalence is compatible with shifts.