refactor: avoid passing both directions of a lemma to simp

this only works by chance, in a way, and will break when leanprover/lean4#5870 lands
leanprover-community · Oct 29, 2024 · 0b01e55 · 0b01e55
1 parent 7bf2901
commit 0b01e55
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git a/Mathlib/CategoryTheory/Adjunction/Basic.lean b/Mathlib/CategoryTheory/Adjunction/Basic.lean
@@ -161,7 +161,9 @@ def homEquiv {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) (X : C) (Y : D) :
     rw [F.map_comp, assoc, ← Functor.comp_map, adj.counit.naturality, ← assoc]
     simp
   right_inv := fun g => by
-    simp [← assoc, ← Functor.comp_map, ← adj.unit.naturality, assoc]
+    simp only [Functor.comp_obj, Functor.map_comp]
+    rw [← assoc, ← Functor.comp_map, ← adj.unit.naturality]
+    simp
 
 alias homEquiv_unit := homEquiv_apply
 alias homEquiv_counit := homEquiv_symm_apply

diff --git a/Mathlib/NumberTheory/Bernoulli.lean b/Mathlib/NumberTheory/Bernoulli.lean
@@ -181,7 +181,7 @@ def bernoulli (n : ℕ) : ℚ :=
   (-1) ^ n * bernoulli' n
 
 theorem bernoulli'_eq_bernoulli (n : ℕ) : bernoulli' n = (-1) ^ n * bernoulli n := by
-  simp [bernoulli, ← mul_assoc, ← sq, ← pow_mul, mul_comm n 2, pow_mul]
+  simp [bernoulli, ← mul_assoc, ← sq, ← pow_mul, mul_comm n 2]
 
 @[simp]
 theorem bernoulli_zero : bernoulli 0 = 1 := by simp [bernoulli]