Quickfix: symm version missing from `semilinearEquiv`

Stream: mathlib4

[Kenny Lau]

import Mathlib

variable (R M : Type*) [CommRing R] [CommRing M] [Algebra R M] (S₁ : Submodule R M)

def foo (r : R) : M ≃ₐ[R] M := sorry

@[simps!] noncomputable def fooSub (r : R) : S₁ ≃ₗ[R] S₁ :=
  (foo R M r : M ≃ₗ[R] M).ofSubmodules S₁ S₁ sorry

#check fooSub_apply_coe -- no weird arrow
#check fooSub_symm_apply_coe -- RHS has weird arrow

example {r} (x : M) : (foo R M r : M ≃ₗ[R] M) x = x := by simp?
-- correctly simplifies to (foo R M r) x = x
-- uses SemilinearEquivClass.semilinearEquiv_apply

example {r} (x : M) : (foo R M r : M ≃ₗ[R] M).symm x = x := by simp -- simp made no progress

[Kenny Lau]

So I noticed that in one of my PR's, an autogenerated simp lemma was a bit weird, so I minimised it as above, where the coercion from M ≃ₐ[R] M to M ≃ₗ[R] M actually has the forward simp lemma but is missing the backward simp lemma (see "RHS has weird arrow")

[Kenny Lau]

I did more digging and isolated the issue as SemilinearEquivClass.semilinearEquiv_apply missing the corresponding symm version (see "simp made no progress")

[Kenny Lau]

is this diagnosis correct, and if so, who should I ping for this issue who might be interested?