Theorem: MatrixCookbook.eq_478 (MatrixCookbook/9SpecialMatrices.lean)

State before:
R : Type u_2
l : Type ?u.206287
m : Type u_1
n : Type ?u.206293
p : Type ?u.206296
q : Type ?u.206299
r : Type ?u.206302
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
e : Equiv.Perm m
⊢ (Equiv.toPEquiv e).toMatrix * (Equiv.toPEquiv e).toMatrixᵀ = 1
Tactic:
rw [← PEquiv.toMatrix_symm, ← PEquiv.toMatrix_trans, ← Equiv.toPEquiv_symm, ←
  Equiv.toPEquiv_trans, Equiv.self_trans_symm, Equiv.toPEquiv_refl, PEquiv.toMatrix_refl]
State after:
no goals