no goals
l : Type ?u.175068
m : Type u_1
n : Type u_2
o : Type ?u.175077
R : Type u_3
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : Fintype m
e₁ e₂ : m ≃ n
A : Matrix m m R
⊢ rank (↑(reindex e₁ e₂) A) = rank A
rw [rank, rank, mulVecLin_reindex, LinearMap.range_comp, LinearMap.range_comp,
  LinearEquiv.range, Submodule.map_top, LinearEquiv.finrank_map_eq]