awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (hypothesis)
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 M
      ((matPolyEquiv : (a : Matrix n n R[X]) → (Matrix n n R)[X])
        (HSMul.hSMul (α := R[X]) (β := Matrix.{u_4, u_4, u_1} n n R[X]) M.charpoly 1)) =
    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)
have h₁ : eval₂ (algebraMap R (Matrix n n R)) M M.charpoly = 0
Tactic: rw [matPolyEquiv_smul_one, eval_map] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (hypothesis)
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)
⊢ HPow.hPow (α := R[X]) X (Fintype.card n) * (A * B).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card m) * (B * A).charpoly
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (hypothesis)
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)
⊢ HPow.hPow (α := R[X]) X (Fintype.card n) * (A * B).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card m) * (B * A).charpoly
have 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]))
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
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)
have 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)
Tactic: rw [hMN, det_fromBlocks_zero₂₁, neg_add_eq_sub, ← neg_sub, det_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
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) *
        (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)
have 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)
Tactic: simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (hypothesis)
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]) X (Fintype.card n) * (A * B).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card m) * (B * A).charpoly
have 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)
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
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)
⊢ (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)
have 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)
Tactic: rw [hNM, det_fromBlocks_zero₂₁, ← neg_sub, det_neg (_ - _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (hypothesis)
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 n) * (A * B).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card m) * (B * A).charpoly
have 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)
Tactic: have hdet_NM : (N * M).det = (-1 : R[X]) ^ (Fintype.card m + Fintype.card n) *
      (X ^ Fintype.card m * (scalar n X - (B * A).map C).det) := by
    rw [hNM, det_fromBlocks_zero₂₁, ← neg_sub, det_neg (_ - _)]
    simp
    ring
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
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
hle : Fintype.card n ≤ Fintype.card m
⊢ (A * B).charpoly = HPow.hPow (α := R[X]) X (Fintype.card m - Fintype.card n) * (B * A).charpoly
have rw : HPow.hPow (α := R[X]) X (Fintype.card n) * (A * B).charpoly =
  HPow.hPow (α := R[X]) X (Fintype.card n) *
    (HPow.hPow (α := R[X]) X (Fintype.card m - Fintype.card n) * (B * A).charpoly)
Tactic: rw [← (isRegular_X_pow _).left.eq_iff, ← mul_assoc, ← pow_add,
    Nat.add_sub_cancel' hle, charpoly_mul_comm']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
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
hle : Fintype.card n ≤ Fintype.card m
rw :
  HPow.hPow (α := R[X]) X (Fintype.card n) * (A * B).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card n) *
      (HPow.hPow (α := R[X]) X (Fintype.card m - Fintype.card n) * (B * A).charpoly)
⊢ (A * B).charpoly = HPow.hPow (α := R[X]) X (Fintype.card m - Fintype.card n) * (B * A).charpoly
have rw₁ : ℕ
Tactic: rw [← (isRegular_X_pow _).left.eq_iff, ← mul_assoc, ← pow_add,
    Nat.add_sub_cancel' hle, charpoly_mul_comm']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
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
hle : Fintype.card n ≤ Fintype.card m
rw :
  HPow.hPow (α := R[X]) X (Fintype.card n) * (A * B).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card n) *
      (HPow.hPow (α := R[X]) X (Fintype.card m - Fintype.card n) * (B * A).charpoly)
rw₁ : ℕ
⊢ (A * B).charpoly = HPow.hPow (α := R[X]) X (Fintype.card m - Fintype.card n) * (B * A).charpoly
have rw₂ : HPow.hPow (α := R[X]) X (Fintype.card n) * (A * B).charpoly =
  HPow.hPow (α := R[X]) X (Fintype.card n) * HPow.hPow (α := R[X]) X (Fintype.card m - Fintype.card n) *
    (B * A).charpoly
Tactic: rw [← (isRegular_X_pow _).left.eq_iff, ← mul_assoc, ← pow_add,
    Nat.add_sub_cancel' hle, charpoly_mul_comm']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
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
hle : Fintype.card n ≤ Fintype.card m
rw :
  HPow.hPow (α := R[X]) X (Fintype.card n) * (A * B).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card n) *
      (HPow.hPow (α := R[X]) X (Fintype.card m - Fintype.card n) * (B * A).charpoly)
rw₁ : ℕ
rw₂ :
  HPow.hPow (α := R[X]) X (Fintype.card n) * (A * B).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card n) * HPow.hPow (α := R[X]) X (Fintype.card m - Fintype.card n) *
      (B * A).charpoly
rw₃ : ℕ
⊢ (A * B).charpoly = HPow.hPow (α := R[X]) X (Fintype.card m - Fintype.card n) * (B * A).charpoly
have rw₄ : HPow.hPow (α := R[X]) X (Fintype.card n) * (A * B).charpoly =
  HPow.hPow (α := R[X]) X (Fintype.card n + (Fintype.card m - Fintype.card n)) * (B * A).charpoly
Tactic: rw [← (isRegular_X_pow _).left.eq_iff, ← mul_assoc, ← pow_add,
    Nat.add_sub_cancel' hle, charpoly_mul_comm']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Basic (goal)
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
hle : Fintype.card n ≤ Fintype.card m
rw :
  HPow.hPow (α := R[X]) X (Fintype.card n) * (A * B).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card n) *
      (HPow.hPow (α := R[X]) X (Fintype.card m - Fintype.card n) * (B * A).charpoly)
rw₁ : ℕ
rw₂ :
  HPow.hPow (α := R[X]) X (Fintype.card n) * (A * B).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card n) * HPow.hPow (α := R[X]) X (Fintype.card m - Fintype.card n) *
      (B * A).charpoly
rw₃ : ℕ
rw₄ :
  HPow.hPow (α := R[X]) X (Fintype.card n) * (A * B).charpoly =
    HPow.hPow (α := R[X]) X (Fintype.card n + (Fintype.card m - Fintype.card n)) * (B * A).charpoly
m₁ : ℕ
⊢ (A * B).charpoly = HPow.hPow (α := R[X]) X (Fintype.card m - Fintype.card n) * (B * A).charpoly
have rw₅ : HPow.hPow (α := R[X]) X (Fintype.card n) * (A * B).charpoly =
  HPow.hPow (α := R[X]) X (Fintype.card m) * (B * A).charpoly
Tactic: rw [← (isRegular_X_pow _).left.eq_iff, ← mul_assoc, ← pow_add,
    Nat.add_sub_cancel' hle, charpoly_mul_comm']