chore(data/equiv/ring): add symm_symm and coe_symm_mk (#5227)

Also generalize `map_mul` and `map_add` to `[has_mul R] [has_add R]`
instead of `[semiring R]`.

Author: urkud

src/data/equiv/ring.lean

@@ -62,6 +62,12 @@ instance : has_coe_to_fun (R ≃+* S) := ⟨_, ring_equiv.to_fun⟩
 
 @[simp] lemma to_fun_eq_coe_fun (f : R ≃+* S) : f.to_fun = f := rfl
 
+/-- A ring isomorphism preserves multiplication. -/
+@[simp] lemma map_mul (e : R ≃+* S) (x y : R) : e (x * y) = e x * e y := e.map_mul' x y
+
+/-- A ring isomorphism preserves addition. -/
+@[simp] lemma map_add (e : R ≃+* S) (x y : R) : e (x + y) = e x + e y := e.map_add' x y
+
 /-- Two ring isomorphisms agree if they are defined by the
     same underlying function. -/
 @[ext] lemma ext {f g : R ≃+* S} (h : ∀ x, f x = g x) : f = g :=
@@ -106,6 +112,10 @@ def simps.inv_fun (e : R ≃+* S) : S → R := e.symm
 
 initialize_simps_projections ring_equiv (to_fun → apply, inv_fun → symm_apply)
 
+@[simp] lemma symm_symm (e : R ≃+* S) : e.symm.symm = e := ext $ λ x, rfl
+
+@[simp] lemma coe_symm_mk (f : R → S) (g h₁ h₂ h₃ h₄) : ⇑(mk f g h₁ h₂ h₃ h₄).symm = g := rfl
+
 /-- Transitivity of `ring_equiv`. -/
 @[trans] protected def trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') : R ≃+* S' :=
 { .. (e₁.to_mul_equiv.trans e₂.to_mul_equiv), .. (e₁.to_add_equiv.trans e₂.to_add_equiv) }
@@ -149,15 +159,9 @@ section semiring
 
 variables [semiring R] [semiring S] (f : R ≃+* S) (x y : R)
 
-/-- A ring isomorphism preserves multiplication. -/
-@[simp] lemma map_mul : f (x * y) = f x * f y := f.map_mul' x y
-
 /-- A ring isomorphism sends one to one. -/
 @[simp] lemma map_one : f 1 = 1 := (f : R ≃* S).map_one
 
-/-- A ring isomorphism preserves addition. -/
-@[simp] lemma map_add : f (x + y) = f x + f y := f.map_add' x y
-
 /-- A ring isomorphism sends zero to zero. -/
 @[simp] lemma map_zero : f 0 = 0 := (f : R ≃+ S).map_zero