chore(data/equiv/ring): make ring_aut reducible (leanprover-community…

…#2563)

This makes the coercion to fun work. This is the same approach as we used for `perm` and it worked okay for `perm`.

Related Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/ring_aut.20coerce.20to.20function

src/data/equiv/ring.lean

@@ -221,7 +221,7 @@ protected def integral_domain {A : Type*} (B : Type*) [ring A] [integral_domain
 end ring_equiv
 
 /-- The group of ring automorphisms. -/
-def ring_aut (R : Type*) [has_mul R] [has_add R] := ring_equiv R R
+@[reducible] def ring_aut (R : Type*) [has_mul R] [has_add R] := ring_equiv R R
 
 namespace ring_aut