Replace simp; rfl with simp only; rfl

leanprover-community · Dec 2, 2024 · 867bc82 · 867bc82
1 parent d34a272
commit 867bc82
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 4 deletions.
diff --git a/Mathlib/Algebra/Category/ModuleCat/Tannaka.lean b/Mathlib/Algebra/Category/ModuleCat/Tannaka.lean
@@ -42,11 +42,13 @@ def ringEquivEndForget₂ (R : Type u) [Ring R] :
     intros
     apply NatTrans.ext
     ext
-    simp [add_smul]
+    simp only [AdditiveFunctor.of_fst, ModuleCat.forget₂_obj, AddCommGrp.coe_of,
+      AddCommGrp.ofHom_apply, DistribMulAction.toAddMonoidHom_apply, add_smul]
     rfl
   map_mul' := by
     intros
     apply NatTrans.ext
     ext
-    simp [mul_smul]
+    simp only [AdditiveFunctor.of_fst, ModuleCat.forget₂_obj, AddCommGrp.coe_of,
+      AddCommGrp.ofHom_apply, DistribMulAction.toAddMonoidHom_apply, mul_smul]
     rfl
diff --git a/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean b/Mathlib/RepresentationTheory/GroupCohomology/Basic.lean
@@ -193,8 +193,9 @@ noncomputable abbrev inhomogeneousCochains : CochainComplex (ModuleCat k) ℕ :=
     /- Porting note: I can see I need to rewrite `LinearEquiv.coe_coe` twice to at
       least reduce the need for `symm_apply_apply` to be an `erw`. However, even `erw` refuses to
       rewrite the second `coe_coe`... -/
-    erw [LinearEquiv.symm_apply_apply, this, LinearMap.zero_apply]
-    simp
+    erw [LinearEquiv.symm_apply_apply, this]
+    simp only [LinearMap.zero_apply, ChainComplex.linearYonedaObj_X, linearYoneda_obj_obj_carrier,
+      map_zero, Pi.zero_apply, LinearMap.zero_apply]
     rfl
 
 @[simp]