chore(CategoryTheory/Adjunction/Basic): missing dsimp lemmas (#7361)

leanprover-community · Sep 28, 2023 · 4b23a87 · 4b23a87
1 parent 7101b4c
commit 4b23a87
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 13 deletions.
diff --git a/Mathlib/CategoryTheory/Adjunction/Basic.lean b/Mathlib/CategoryTheory/Adjunction/Basic.lean
@@ -610,6 +610,7 @@ namespace Equivalence
 
 /-- The adjunction given by an equivalence of categories. (To obtain the opposite adjunction,
 simply use `e.symm.toAdjunction`. -/
+@[pp_dot, simps! unit counit]
 def toAdjunction (e : C ≌ D) : e.functor ⊣ e.inverse :=
   mkOfUnitCounit
     ⟨e.unit, e.counit, by
@@ -623,17 +624,8 @@ def toAdjunction (e : C ≌ D) : e.functor ⊣ e.inverse :=
       exact e.unit_inverse_comp _⟩
 #align category_theory.equivalence.to_adjunction CategoryTheory.Equivalence.toAdjunction
 
-@[simp]
-theorem asEquivalence_toAdjunction_unit {e : C ≌ D} :
-    e.functor.asEquivalence.toAdjunction.unit = e.unit :=
-  rfl
-#align category_theory.equivalence.as_equivalence_to_adjunction_unit CategoryTheory.Equivalence.asEquivalence_toAdjunction_unit
-
-@[simp]
-theorem asEquivalence_toAdjunction_counit {e : C ≌ D} :
-    e.functor.asEquivalence.toAdjunction.counit = e.counit :=
-  rfl
-#align category_theory.equivalence.as_equivalence_to_adjunction_counit CategoryTheory.Equivalence.asEquivalence_toAdjunction_counit
+#align category_theory.equivalence.as_equivalence_to_adjunction_unit CategoryTheory.Equivalence.toAdjunction_unitₓ
+#align category_theory.equivalence.as_equivalence_to_adjunction_counit CategoryTheory.Equivalence.toAdjunction_counitₓ
 
 end Equivalence
 

diff --git a/Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean b/Mathlib/CategoryTheory/Monoidal/NaturalTransformation.lean
@@ -233,8 +233,7 @@ def monoidalCounit (F : MonoidalFunctor C D) [IsEquivalence F.toFunctor] :
       erw [Iso.hom_inv_id_app, CategoryTheory.Functor.map_id]
       simp only [id_comp, CategoryTheory.Iso.inv_hom_id_app,
         CategoryTheory.IsIso.hom_inv_id_assoc]
-      erw [comp_id]
-      rfl }
+      erw [comp_id] }
 #align category_theory.monoidal_counit CategoryTheory.monoidalCounit
 
 instance (F : MonoidalFunctor C D) [IsEquivalence F.toFunctor] : IsIso (monoidalCounit F) :=