Motive Not Type Correct Nth

Stream: new members

[MohanadAhmed]

In the code below the rewrite in rank_eq_rank_diagonal fails. Weirdly enough, if I replace the RHS side with the zero matrix it does not fail.
The error message says "motive is not type correct". In full the error message is below the code. Checking some threads here I found suggest ions to try using: simp_rw: it fails. I also tried erewrite: it also fails.

The error message for simp_rw after setting set_option trace.simp_lemmas true is
[simp_lemmas.invalid] LHS of rule derived from '[anonymous]' occurs in RHS

import data.complex.basic
import linear_algebra.matrix.hermitian
import linear_algebra.matrix.pos_def
import linear_algebra.matrix.determinant
import linear_algebra.matrix.spectrum
import linear_algebra.matrix.nonsingular_inverse
import linear_algebra.matrix.diagonal
import data.matrix.basic
import data.matrix.rank
--import rank_surj_inv
import algebra.star.basic

open matrix complex
open_locale matrix big_operators

variables {m n R: Type*}
variables [fintype m][fintype n][decidable_eq m][decidable_eq n]
variables [field R][is_R_or_C R][partial_order R][star_ordered_ring R]

lemma modified_spectral_theorem (A: matrix n n ℂ)(hA: A.is_hermitian) :
  A = (hA.eigenvector_matrix) ⬝
    (matrix.diagonal (coe ∘ hA.eigenvalues)) ⬝ hA.eigenvector_matrix_inv :=
begin
  have h := hA.spectral_theorem,
  replace h := congr_arg (λ x, hA.eigenvector_matrix ⬝  x) h,
  simp only at h,
  rw [← matrix.mul_assoc, hA.eigenvector_matrix_mul_inv, matrix.one_mul] at h,
  rwa matrix.mul_assoc,
end

lemma rank_eq_rank_diagonal (A: matrix n n ℂ)(hA: A.is_hermitian) :
  A.rank = (matrix.diagonal ((coe ∘ hA.eigenvalues): n → ℂ)).rank :=
    -- A.rank = (0: matrix n n ℂ).rank := -- This line makes rewrite work!!
begin
  rw modified_spectral_theorem A hA,

end

rewrite tactic failed, motive is not type correct
  λ (_a : matrix n n ℂ),
    A.rank = (diagonal (coe ∘ hA.eigenvalues)).rank = (_a.rank = (diagonal (coe ∘ hA.eigenvalues)).rank)
state:
n : Type u_2,
_inst_2 : fintype n,
_inst_4 : decidable_eq n,
A : matrix n n ℂ,
hA : A.is_hermitian
⊢ A.rank = (diagonal (coe ∘ hA.eigenvalues)).rank

[MohanadAhmed]

The trick suggested here to use nth_rewrite 0 also does not work. nth_rewrite_lhs 0 works.

[MohanadAhmed]

I guess this is because there is an A hiding inside hA.eigenvalues but what if I had another A on the lhs? Why is nth_rewrite not working but nth_rewrite_lhs working?