chore: remove an erw (leanprover-community#16445)

yoh-tanimoto · Sep 3, 2024 · 8525fd6 · 8525fd6
1 parent fa76f8b
commit 8525fd6
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/RingTheory/FractionalIdeal/Operations.lean b/Mathlib/RingTheory/FractionalIdeal/Operations.lean
@@ -226,7 +226,7 @@ theorem canonicalEquiv_symm : (canonicalEquiv S P P').symm = canonicalEquiv S P'
       exact ⟨fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩, fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩⟩
 
 theorem canonicalEquiv_flip (I) : canonicalEquiv S P P' (canonicalEquiv S P' P I) = I := by
-  rw [← canonicalEquiv_symm]; erw [RingEquiv.apply_symm_apply]
+  rw [← canonicalEquiv_symm, RingEquiv.symm_apply_apply]
 
 @[simp]
 theorem canonicalEquiv_canonicalEquiv (P'' : Type*) [CommRing P''] [Algebra R P'']