From ec2dfcae3677bcdc0d8e906831b1d251dfcbc0f1 Mon Sep 17 00:00:00 2001
From: Lukas Miaskiwskyi <lukas.mias@gmail.com>
Date: Mon, 16 Jan 2023 10:17:33 +0000
Subject: [PATCH] feat(ring_theory/ring_invo): add ring_invo_class (#18175)

By its docstring, `ring_equiv_class` yearns to be extended whenever `ring_equiv` is. The `ring_invo` structure fails to heed its call. This file is currently being ported to mathlib4, and this will help, I believe.
---
 src/ring_theory/ring_invo.lean | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/src/ring_theory/ring_invo.lean b/src/ring_theory/ring_invo.lean
index 01324030be5c7..2d8a7bb246d2d 100644
--- a/src/ring_theory/ring_invo.lean
+++ b/src/ring_theory/ring_invo.lean
@@ -27,13 +27,34 @@ Ring involution
 
 variables (R : Type*)
 
+set_option old_structure_cmd true
+
 /-- A ring involution -/
 structure ring_invo [semiring R] extends R ≃+* Rᵐᵒᵖ :=
 (involution' : ∀ x, (to_fun (to_fun x).unop).unop = x)
 
+/-- The equivalence of rings underlying a ring involution. -/
+add_decl_doc ring_invo.to_ring_equiv
+
+/-- `ring_invo_class F R S` states that `F` is a type of ring involutions.
+You should extend this class when you extend `ring_invo`. -/
+class ring_invo_class (F : Type*) (R : out_param Type*) [semiring R]
+  extends ring_equiv_class F R Rᵐᵒᵖ :=
+(involution : ∀ (f : F) (x), (f (f x).unop).unop = x)
+
 namespace ring_invo
 variables {R} [semiring R]
 
+instance (R : Type*) [semiring R] : ring_invo_class (ring_invo R) R :=
+{ coe := to_fun,
+  inv :=  inv_fun,
+  coe_injective' := λ e f h₁ h₂, by { cases e, cases f, congr' },
+  map_add := map_add',
+  map_mul := map_mul',
+  left_inv := left_inv,
+  right_inv := right_inv,
+  involution := involution' }
+
 /-- Construct a ring involution from a ring homomorphism. -/
 def mk' (f : R →+* Rᵐᵒᵖ) (involution : ∀ r, (f (f r).unop).unop = r) :
   ring_invo R :=
@@ -43,6 +64,8 @@ def mk' (f : R →+* Rᵐᵒᵖ) (involution : ∀ r, (f (f r).unop).unop = r) :
   involution' := involution,
   .. f }
 
+/-- Helper instance for when there's too many metavariables to apply
+`fun_like.has_coe_to_fun` directly. -/
 instance : has_coe_to_fun (ring_invo R) (λ _, R → Rᵐᵒᵖ) := ⟨λ f, f.to_ring_equiv.to_fun⟩
 
 @[simp]