perf(Algebra/Algebra/Equiv): mark coe_ringEquiv with defeq again (#40873)

This PR reverts the proof of `coe_ringEquiv` back to `:= rfl` after #40834, which apparently is necessary for performance reasons.

Author: JovanGerb

Mathlib/Algebra/Algebra/Equiv.lean

@@ -160,7 +160,7 @@ theorem toRingEquiv_eq_coe : e.toRingEquiv = e :=
 lemma toRingEquiv_toRingHom : ((e : A₁ ≃+* A₂) : A₁ →+* A₂) = e :=
   rfl
 
-theorem coe_ringEquiv : ((e : A₁ ≃+* A₂) : A₁ → A₂) = e := by simp
+theorem coe_ringEquiv : ((e : A₁ ≃+* A₂) : A₁ → A₂) = e := rfl
 
 @[deprecated (since := "2026-06-21")] alias coe_ringEquiv' := coe_ringEquiv