chore(algebra/algebra/basic): add a missing coe lemma (#6535)

This is just to stop the terrible pain of having to work with `⇑(e.to_ring_equiv) x` in goals.

In the long run, we should sort out the simp normal form, but for now I just want to stop the pain.

Author: eric-wieser

src/algebra/algebra/basic.lean

@@ -673,7 +673,9 @@ rfl
 
 @[simp] lemma to_fun_eq_coe (e : A₁ ≃ₐ[R] A₂) : e.to_fun = e := rfl
 
+-- TODO: decide on a simp-normal form so that only one of these two lemmas is needed
 @[simp, norm_cast] lemma coe_ring_equiv : ((e : A₁ ≃+* A₂) : A₁ → A₂) = e := rfl
+@[simp] lemma coe_ring_equiv' : (e.to_ring_equiv : A₁ → A₂) = e := rfl
 
 lemma coe_ring_equiv_injective : function.injective (λ e : A₁ ≃ₐ[R] A₂, (e : A₁ ≃+* A₂)) :=
 begin