Lean4
/-- A type has an involutive inversion if it admits a surjective map that preserves `⁻¹` to a type
which has an involutive inversion. See note [reducible non-instances] -/
@[to_additive /-- A type has an involutive negation if it admits a surjective map that
preserves `-` to a type which has an involutive negation. -/
]
protected abbrev involutiveInv {M₁ : Type*} [Inv M₁] [InvolutiveInv M₂] (f : M₁ → M₂) (hf : Injective f)
(inv : ∀ x, f x⁻¹ = (f x)⁻¹) : InvolutiveInv M₁
where
inv := Inv.inv
inv_inv x := hf <| by rw [inv, inv, inv_inv]