awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
h : eval₂ (algebraMap R (Matrix n n R)) M M.charpoly = 0
⊢ Eq (α := Matrix n n R) ((aeval M : (a : R[X]) → Matrix n n R) M.charpoly : Matrix n n R) (0 : Matrix n n R)

Tactic:
h

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, Matrix.diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Goal:
R : Type u_1
inst : CommRing R
n : Type u_4
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
h : eval₂ (algebraMap R (Matrix n n R)) M M.charpoly = 0
⊢ Eq (α := Matrix n n R) ((aeval M : (a : R[X]) → Matrix n n R) M.charpoly : Matrix n n R) (0 : Matrix n n R)

Tactic:
exact h
-- 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)
⊢ 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)

Tactic:
simp [M, N, fromBlocks_multiply, smul_eq_mul_diagonal, -diagonal_neg]

Premises used: Matrix.smul_eq_mul_diagonal, Matrix.diagonal_neg, Matrix.fromBlocks_multiply
-- 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)
⊢ 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)

Tactic:
have hMN :
      M * N = fromBlocks (-scalar m X + (A * B).map C) (-(X : R[X]) • A.map C) 0 (-scalar n X) := by
    simp [M, N, fromBlocks_multiply, smul_eq_mul_diagonal, -diagonal_neg]
-- 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)
⊢ 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]))

Tactic:
simp [M, N, fromBlocks_multiply, sub_eq_add_neg, -scalar_apply, scalar_comm, Commute.all]

Premises used: Matrix.scalar_comm, sub_eq_add_neg, Matrix.fromBlocks_multiply, Matrix.scalar_apply, Commute.all
-- 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)
⊢ 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]))

Tactic:
have hNM : N * M = fromBlocks (-scalar m X) (-A.map C) 0 ((B * A).map C - scalar n X) := by
    simp [M, N, fromBlocks_multiply, sub_eq_add_neg, -scalar_apply, scalar_comm, Commute.all]
-- 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]))
rw :
  HPow.hPow (α := R[X]) (-1) (Fintype.card m) *
        (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 *
      det.{u_1, u_4} (n := n) (-(scalar n : (a : R[X]) → Matrix n n R[X]) X) =
    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)
⊢ (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)

Tactic:
rw [hMN, det_fromBlocks_zero₂₁, neg_add_eq_sub, ← neg_sub, det_neg]

Premises used: neg_sub, neg_add_eq_sub, Matrix.det_neg, Matrix.det_fromBlocks_zero₂₁
-- 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]))
simp :
  HPow.hPow (α := R[X]) (-1) (Fintype.card m) *
        ((diagonal fun (x : m) ↦ X) -
            HMul.hMul (α := Matrix.{u_3, u_4, u_1} m n R[X]) (β := Matrix.{u_4, u_3, u_1} n m R[X])
              (A.map (⇑C : (a : R) → R[X])) (B.map (⇑C : (a : R) → R[X]))).det *
      HPow.hPow (α := R[X]) (-X) (Fintype.card n) =
    HPow.hPow (α := R[X]) (-1) (Fintype.card m + Fintype.card n) *
      (HPow.hPow (α := R[X]) X (Fintype.card n) *
        ((diagonal fun (x : m) ↦ X) -
            HMul.hMul (α := Matrix.{u_3, u_4, u_1} m n R[X]) (β := Matrix.{u_4, u_3, u_1} n m R[X])
              (A.map (⇑C : (a : R) → R[X])) (B.map (⇑C : (a : R) → R[X]))).det)
⊢ HPow.hPow (α := R[X]) (-1) (Fintype.card m) *
        (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 *
      det.{u_1, u_4} (n := n) (-(scalar n : (a : R[X]) → Matrix n n R[X]) X) =
    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)

Tactic:
simp
-- 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]))
⊢ HPow.hPow (α := R[X]) (-1) (Fintype.card m) *
        ((diagonal fun (x : m) ↦ X) -
            HMul.hMul (α := Matrix.{u_3, u_4, u_1} m n R[X]) (β := Matrix.{u_4, u_3, u_1} n m R[X])
              (A.map (⇑C : (a : R) → R[X])) (B.map (⇑C : (a : R) → R[X]))).det *
      HPow.hPow (α := R[X]) (-X) (Fintype.card n) =
    HPow.hPow (α := R[X]) (-1) (Fintype.card m + Fintype.card n) *
      (HPow.hPow (α := R[X]) X (Fintype.card n) *
        ((diagonal fun (x : m) ↦ X) -
            HMul.hMul (α := Matrix.{u_3, u_4, u_1} m n R[X]) (β := Matrix.{u_4, u_3, u_1} n m R[X])
              (A.map (⇑C : (a : R) → R[X])) (B.map (⇑C : (a : R) → R[X]))).det)

Tactic:
ring
-- 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]))
⊢ (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)

Tactic:
have hdet_MN : (M * N).det = (-1 : R[X]) ^ (Fintype.card m + Fintype.card n) *
      (X ^ Fintype.card n * (scalar m X - (A * B).map C).det) := by
    rw [hMN, det_fromBlocks_zero₂₁, neg_add_eq_sub, ← neg_sub, det_neg]
    simp
    ring
-- 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)
rw :
  det.{u_1, u_3} (n := m) (-(scalar m : (a : R[X]) → Matrix m m R[X]) X) *
      (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
        (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) =
    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)
⊢ (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)

Tactic:
rw [hNM, det_fromBlocks_zero₂₁, ← neg_sub, det_neg (_ - _)]

Premises used: neg_sub, HSub.hSub, Matrix.det_neg, Matrix.det_fromBlocks_zero₂₁
-- 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)
simp :
  HPow.hPow (α := R[X]) (-X) (Fintype.card m) *
      (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
        ((diagonal fun (x : n) ↦ X) -
            HMul.hMul (α := Matrix.{u_4, u_3, u_1} n m R[X]) (β := Matrix.{u_3, u_4, u_1} m n R[X])
              (B.map (⇑C : (a : R) → R[X])) (A.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) *
        ((diagonal fun (x : n) ↦ X) -
            HMul.hMul (α := Matrix.{u_4, u_3, u_1} n m R[X]) (β := Matrix.{u_3, u_4, u_1} m n R[X])
              (B.map (⇑C : (a : R) → R[X])) (A.map (⇑C : (a : R) → R[X]))).det)
⊢ det.{u_1, u_3} (n := m) (-(scalar m : (a : R[X]) → Matrix m m R[X]) X) *
      (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
        (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) =
    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)

Tactic:
simp
-- 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)
⊢ HPow.hPow (α := R[X]) (-X) (Fintype.card m) *
      (HPow.hPow (α := R[X]) (-1) (Fintype.card n) *
        ((diagonal fun (x : n) ↦ X) -
            HMul.hMul (α := Matrix.{u_4, u_3, u_1} n m R[X]) (β := Matrix.{u_3, u_4, u_1} m n R[X])
              (B.map (⇑C : (a : R) → R[X])) (A.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) *
        ((diagonal fun (x : n) ↦ X) -
            HMul.hMul (α := Matrix.{u_4, u_3, u_1} n m R[X]) (β := Matrix.{u_3, u_4, u_1} m n R[X])
              (B.map (⇑C : (a : R) → R[X])) (A.map (⇑C : (a : R) → R[X]))).det)

Tactic:
ring