-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Goal:
R : Type u_1
inst : CommRing R
m : Type u_3
n : Type u_4
inst_1 : DecidableEq m
inst_2 : DecidableEq n
inst_3 : Fintype m
inst_4 : Fintype n
A : Matrix m n R
B : Matrix n m R
M : Matrix (m ⊕ n) (m ⊕ n) R[X] :=
  fromBlocks ((scalar m : (a : R[X]) → Matrix m m R[X]) X) (A.map (⇑C : (a : R) → R[X])) (B.map (⇑C : (a : R) → R[X])) 1
N : Matrix (m ⊕ n) (m ⊕ n) R[X] :=
  fromBlocks (-1) 0 (B.map (⇑C : (a : R) → R[X])) (-(scalar n : (a : R[X]) → Matrix n n R[X]) X)
hMN :
  M * N =
    fromBlocks
      (HAdd.hAdd (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
        (-(scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
        ((A * B).map (⇑C : (a : R) → R[X])))
      (HSMul.hSMul (α := R[X]) (β := Matrix.{u_3, u_4, u_1} m n R[X]) (-X) (A.map (⇑C : (a : R) → R[X]))) 0
      (-(scalar n : (a : R[X]) → Matrix n n R[X]) X)
hNM :
  N * M =
    fromBlocks (-(scalar m : (a : R[X]) → Matrix m m R[X]) X) (-A.map (⇑C : (a : R) → R[X])) 0
      (HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X])
        ((B * A).map (⇑C : (a : R) → R[X]))
        ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{u_4, u_4, u_1} n n R[X]))
hdet_MN :
  (M * N).det =
    HPow.hPow (α := R[X]) (-1) (Fintype.card m + Fintype.card n) *
      (HPow.hPow (α := R[X]) X (Fintype.card n) *
        (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
            ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
            ((A * B).map (⇑C : (a : R) → R[X]))).det)
hdet_NM :
  (N * M).det =
    HPow.hPow (α := R[X]) (-1) (Fintype.card m + Fintype.card n) *
      (HPow.hPow (α := R[X]) X (Fintype.card m) *
        (HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X])
            ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{u_4, u_4, u_1} n n R[X])
            ((B * A).map (⇑C : (a : R) → R[X]))).det)
rw :
  HPow.hPow (α := R[X]) (-1) (Fintype.card m + Fintype.card n) *
      (HPow.hPow (α := R[X]) X (Fintype.card n) *
        (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
            ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
            ((A * B).map (⇑C : (a : R) → R[X]))).det) =
    HPow.hPow (α := R[X]) (-1) (Fintype.card m + Fintype.card n) *
      (HPow.hPow (α := R[X]) X (Fintype.card m) *
        (HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X])
            ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{u_4, u_4, u_1} n n R[X])
            ((B * A).map (⇑C : (a : R) → R[X]))).det)
rw₁ : ℕ
rw₂ :
  HPow.hPow (α := R[X]) (-1) (Fintype.card m + Fintype.card n) *
      (HPow.hPow (α := R[X]) X (Fintype.card n) *
        (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
            ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
            ((A * B).map (⇑C : (a : R) → R[X]))).det) =
    (N * M).det
rw₃ : (M * N).det = (N * M).det
rw₄ rw₅ : (N * M).det = (N * M).det
⊢ HPow.hPow (α := R[X]) X (Fintype.card n) *
      (HSub.hSub (α := Matrix.{u_3, u_3, u_1} m m R[X]) (β := Matrix.{u_3, u_3, u_1} m m R[X])
          ((scalar m : (a : R[X]) → Matrix m m R[X]) X : Matrix.{u_3, u_3, u_1} m m R[X])
          ((A * B).map (⇑C : (a : R) → R[X]))).det =
    HPow.hPow (α := R[X]) X (Fintype.card m) *
      (HSub.hSub (α := Matrix.{u_4, u_4, u_1} n n R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X])
          ((scalar n : (a : R[X]) → Matrix n n R[X]) X : Matrix.{u_4, u_4, u_1} n n R[X])
          ((B * A).map (⇑C : (a : R) → R[X]))).det

Tactic:
rw [← (isUnit_neg_one.pow _).isRegular.left.eq_iff, ← hdet_NM, ← hdet_MN, det_mul_comm]

Premises used: Function.Injective.eq_iff, IsUnit.pow, isUnit_neg_one, IsUnit.isRegular, Matrix.det_mul_comm, IsRegular.left