no goals
k : Type ?u.16360
l : Type ?u.16363
m✝ : Type ?u.16366
n✝ : Type ?u.16369
α✝ : Type v
m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : Semiring α
f : n ≃ n
M : Matrix m n α
i : m
j : n
⊢ (M ⬝ toMatrix (Equiv.toPEquiv f)) i j = submatrix M id (↑f.symm) i j
rw [PEquiv.matrix_mul_apply, ← Equiv.toPEquiv_symm, Equiv.toPEquiv_apply,
  Matrix.submatrix_apply, id.def]