simp made no progress in finrank of matrix

Stream: Is there code for X?

[Edison Xie]

I have simp made no progress in proving Module.finrank F (Matrix (Fin n) (Fin n) F) = n ^ 2 is this suppose to happen?

[Edison Xie]

aesop also failed and the proof is rw[pow_two, Module.finrank_matrix] and then simp I thought this should be an easy simp lemma?

[Kim Morrison]

Please post a #mwe.

[Edison Xie]

import Mathlib

example (F : Type*) [Field F]: Module.finrank F (Matrix (Fin n) (Fin n) F) = n^2 := by
  simp

[Edison Xie]

this would give you the error

[Bhavik Mehta]

Edison Xie said:

is this suppose to happen?

This looks expected, both of the lemmas you cite for the rw proof are not marked simp, so I wouldn't expect simp to make progress here. I can see an argument for Module.finrank_matrix being a simp lemma though...

[Bhavik Mehta]

Actually, the rank version of this lemma is simp, so it probably makes sense for the finrank one to be too