symm attribute error

[winstonyin]

The following code produces an error on the symm attribute:

import Mathlib.Algebra.Hom.Group
import Mathlib.Logic.Equiv.Basic

def MulHom.inverse [Mul M] [Mul N] (f : M →ₙ* N) (g : N → M) (h₁ : Function.LeftInverse g f)
    (h₂ : Function.RightInverse g f) : N →ₙ* M where
  toFun := g
  map_mul' x y :=
    calc
      g (x * y) = g (f (g x) * f (g y)) := by rw [h₂ x, h₂ y]
      _ = g (f (g x * g y)) := by rw [f.map_mul]
      _ = g x * g y := h₁ _

structure MulEquiv (M N : Type _) [Mul M] [Mul N] extends M ≃ N, M →ₙ* N

infixl:25 " ≃* " => MulEquiv

@[symm]
-- @[symm] attribute only applies to lemmas proving x ∼ y → y ∼ x, got {M : Type u_1} →
--  {N : Type u_2} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → N ≃* M
def foo_symm {M N : Type _} [Mul M] [Mul N] (h : M ≃* N) : N ≃* M :=
  { h.toEquiv.symm with map_mul' := (h.toMulHom.inverse h.toEquiv.symm h.left_inv h.right_inv).map_mul }

It appears that trans is similarly having trouble recognising the structure of trans lemmas.

[siddhartha-gadgil]

This has been narrowed, but some expertise is needed to make decisions on correcting this (or simply correcting the code - I gathered there are other issues). Will add details in a WIP PR.

[kmill]

It looks like symm doesn't report an error anymore so I'll close this issue.

import Mathlib.Algebra.Hom.Group
import Mathlib.Logic.Equiv.Basic

def MulHom.inverse [Mul M] [Mul N] (f : M →ₙ* N) (g : N → M) (h₁ : Function.LeftInverse g f)
    (h₂ : Function.RightInverse g f) : N →ₙ* M where
  toFun := g
  map_mul' x y :=
    calc
      g (x * y) = g (f (g x) * f (g y)) := by rw [h₂ x, h₂ y]
      _ = g (f (g x * g y)) := by rw [f.map_mul]
      _ = g x * g y := h₁ _

structure MulEquiv (M N : Type _) [Mul M] [Mul N] extends M ≃ N, M →ₙ* N

infixl:25 " ≃* " => MulEquiv

@[symm]
def foo_symm {M N : Type _} [Mul M] [Mul N] (h : M ≃* N) : N ≃* M :=
  { h.toEquiv.symm with map_mul' := (h.toMulHom.inverse h.toEquiv.symm h.left_inv h.right_inv).map_mul }