chore(CategoryTheory/Idempotents): fix simp direction in Karoubi (#24848)

Author: jcommelin

Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean

@@ -59,7 +59,7 @@ def map {F G : C ⥤ Karoubi D} (φ : F ⟶ G) : obj F ⟶ obj G where
         have h' := F.congr_map P.idem
         simp only [hom_ext_iff, Karoubi.comp_f, F.map_comp] at h h'
         simp only [obj_obj_p, assoc, ← h]
-        slice_rhs 1 3 => rw [h', h'] }
+        slice_lhs 1 3 => rw [h', h'] }
   naturality _ _ f := by
     ext
     dsimp [obj]
@@ -117,7 +117,7 @@ def KaroubiUniversal₁.counitIso :
                 comm := by
                   simpa only [hom_ext_iff, G.map_comp, G.map_id] using
                     G.congr_map
-                      (show P.decompId_p = (toKaroubi C).map P.p ≫ P.decompId_p ≫ 𝟙 _ by simp) }
+                      (show (toKaroubi C).map P.p ≫ P.decompId_p ≫ 𝟙 _ = P.decompId_p by simp) }
             naturality := fun P Q f => by
               simpa only [hom_ext_iff, G.map_comp]
                 using (G.congr_map (decompId_p_naturality f)).symm }
@@ -127,7 +127,7 @@ def KaroubiUniversal₁.counitIso :
                 comm := by
                   simpa only [hom_ext_iff, G.map_comp, G.map_id] using
                     G.congr_map
-                      (show P.decompId_i = 𝟙 _ ≫ P.decompId_i ≫ (toKaroubi C).map P.p by simp) }
+                      (show 𝟙 _ ≫ P.decompId_i ≫ (toKaroubi C).map P.p = P.decompId_i by simp) }
             naturality := fun P Q f => by
               simpa only [hom_ext_iff, G.map_comp] using G.congr_map (decompId_i_naturality f) }
         hom_inv_id := by

Mathlib/CategoryTheory/Idempotents/Karoubi.lean

@@ -69,23 +69,24 @@ structure Hom (P Q : Karoubi C) where
   /-- a morphism between the underlying objects -/
   f : P.X ⟶ Q.X
   /-- compatibility of the given morphism with the given idempotents -/
-  comm : f = P.p ≫ f ≫ Q.p := by aesop_cat
+  comm : P.p ≫ f ≫ Q.p = f := by aesop_cat
 
 instance [Preadditive C] (P Q : Karoubi C) : Inhabited (Hom P Q) :=
   ⟨⟨0, by rw [zero_comp, comp_zero]⟩⟩
 
 @[reassoc (attr := simp)]
-theorem p_comp {P Q : Karoubi C} (f : Hom P Q) : P.p ≫ f.f = f.f := by rw [f.comm, ← assoc, P.idem]
+theorem p_comp {P Q : Karoubi C} (f : Hom P Q) : P.p ≫ f.f = f.f := by
+  rw [← f.comm, ← assoc, P.idem]
 
 @[reassoc (attr := simp)]
 theorem comp_p {P Q : Karoubi C} (f : Hom P Q) : f.f ≫ Q.p = f.f := by
-  rw [f.comm, assoc, assoc, Q.idem]
+  rw [← f.comm, assoc, assoc, Q.idem]
 
 @[reassoc]
 theorem p_comm {P Q : Karoubi C} (f : Hom P Q) : P.p ≫ f.f = f.f ≫ Q.p := by rw [p_comp, comp_p]
 
 theorem comp_proof {P Q R : Karoubi C} (g : Hom Q R) (f : Hom P Q) :
-    f.f ≫ g.f = P.p ≫ (f.f ≫ g.f) ≫ R.p := by rw [assoc, comp_p, ← assoc, p_comp]
+    P.p ≫ (f.f ≫ g.f) ≫ R.p = f.f ≫ g.f := by simp
 
 /-- The category structure on the karoubi envelope of a category. -/
 instance : Category (Karoubi C) where
@@ -144,7 +145,7 @@ variable {C}
 
 @[simps add]
 instance instAdd [Preadditive C] {P Q : Karoubi C} : Add (P ⟶ Q) where
-  add f g := ⟨f.f + g.f, by rw [add_comp, comp_add, ← f.comm, ← g.comm]⟩
+  add f g := ⟨f.f + g.f, by rw [add_comp, comp_add, f.comm, g.comm]⟩
 
 @[simps neg]
 instance instNeg [Preadditive C] {P Q : Karoubi C} : Neg (P ⟶ Q) where