simps generates wrong lemma for OrderIso symm_apply

Since OrderIso is defined as an abbrev of RelIso, @[simps!] automatically uses RelIso.symm for the symm_apply projection, so in the code below the automatically generated lemma foo_symm_apply actually has type (RelIso.symm foo) a✝ = f a✝, which is undesirable (and doesn't use OrderIso.symm.

Unfortunately, there are no easy ways to fix this, since we have 52 automatically generated lemmas involving RelIso.symm _ _ = _ and 59 manually proved lemmas involving e.symm _ = _.

The possible solutions are:

1. Go through each of the 52 lemmas generated by simps, manually remove them and prove the OrderIso.symm version, and then add a linter against using @[simps!] on OrderIso. Resistance: the smallest.
2. Remove OrderIso.symm entirely, and just use RelIso.symm. Resistance: this is still defeq abuse, and the resulting term would not have the correct type, i.e. the resulting term will have type RelIso instead of OrderIso.
3. Allow simps to be configured on definitions, not just structure. Resistance: probably will take a long time until this actually happens.
4. Have a simp lemma e.symm x = RelIso.symm e x. Resistance: this will break the 59 simp lemmas above.
5. Have a simp lemma RelIso.symm e x = e.symm x. Resistance: this doesn't actually fix the problem, because @[simps!] will still generate the wrong lemma.

For now, 1. seems to be the least of the evils.

import Mathlib

axiom f : ℕ → ℕ
axiom f_eq {n} : f n = n

@[simps!] noncomputable def foo : ℕ ≃o ℕ where
  toFun := f
  invFun := f
  left_inv _ := by simp [f_eq]
  right_inv _ := by simp [f_eq]
  map_rel_iff' := by simp [f_eq]

#check foo_symm_apply -- (RelIso.symm foo) a✝ = f a✝

example (n) : foo.symm n = sorry := by simp -- no progress

(Link to web editor)

Start with the minimal reproduction using @[simps!] on the OrderIso definition and inspect the generated foo_symm_apply type. Review the 52 generated RelIso.symm lemmas and 59 manual OrderIso.symm lemmas mentioned in the issue, then determine which listed approach keeps the affected lemmas consistent and makes the reproduction use OrderIso.symm.