Multiset spectrum relabel eq

lemma multiset_spectrum_relabel_eq {d₁ d₂ : Type*} [Fintype d₁] [DecidableEq d₁] [Fintype d₂] [DecidableEq d₂]    (ρ : MState d₁) (e : d₂ ≃ d₁) :    Multiset.map (ρ.relabel e).spectrum Finset.univ.val = Multiset.map ρ.spectrum Finset.univ.val := by  have h_charpoly : Matrix.charpoly (ρ.relabel e).m = Matrix.charpoly ρ.m := by    exact Matrix.charpoly_reindex e.symm ρ.m  have h_eigenvalues : Multiset.map (ρ.relabel e).M.H.eigenvalues Finset.univ.val = Multiset.map ρ.M.H.eigenvalues Finset.univ.val := by    have h_eigenvalues : Polynomial.roots (Matrix.charpoly (ρ.relabel e).m) = Polynomial.roots (Matrix.charpoly ρ.m) := by      rw [h_charpoly];    have := ρ.M.H.roots_charpoly_eq_eigenvalues    have := (ρ.relabel e).M.H.roots_charpoly_eq_eigenvalues    simp_all only [relabel_m, mat_M, Complex.coe_algebraMap, Function.comp_apply, relabel_M,      mat_reindex, Matrix.reindex_apply, Equiv.symm_symm]    replace this := congr_arg ( fun m => m.map ( fun x => x.re ) ) this    aesop;  unfold MState.spectrum;  ext  rename_i a  simp_all only [relabel_m, relabel_M, mat_reindex, mat_M, Matrix.reindex_apply, Equiv.symm_symm]  obtain ⟨val, property⟩ := a  obtain ⟨left, right⟩ := property  convert congr_arg ( fun m => Multiset.count val m ) h_eigenvalues using 1;  · rw [ Multiset.count_map, Multiset.count_map ];    simp [ Subtype.ext_iff ];    congr! 2;  · erw [ Multiset.count_map, Multiset.count_map ];    congr! 2;    exact beq_eq_beq.mp rfl