awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
h : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
rw :
  Eq (α := R[X])
    (HMul.hMul (β := Matrix.{u_2, w, u_1} (ChooseBasisIndex R M) ι R)
        (HMul.hMul (α := Matrix.{w, u_2, u_1} ι (ChooseBasisIndex R M) R) (β :=
          Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
          (b.toMatrix (⇑b' : (a : ChooseBasisIndex R M) → M))
          ((toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f :
            Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R))
        (b'.toMatrix (⇑b : (a : ι) → M))).charpoly
    (Matrix.charpoly.{u_1, u_2} (n := ChooseBasisIndex R M)
      ((toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f))
⊢ Eq.{u_1 + 1} (α := R[X]) (Matrix.charpoly.{u_1, w} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f))
    (Matrix.charpoly.{u_1, u_2} (n := ChooseBasisIndex R M)
      ((toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f))

Tactic:
rw [← basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix b b' b b']

Premises used: basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix
-- Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
h : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
set :
  let P : Matrix.{w, u_2, u_1} ι (ChooseBasisIndex R M) R := b.toMatrix (⇑b' : (a : ChooseBasisIndex R M) → M);
  Eq (α := R[X])
    (HMul.hMul (β := Matrix.{u_2, w, u_1} (ChooseBasisIndex R M) ι R)
        (HMul.hMul (β := Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) P
          ((toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f :
            Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R))
        (b'.toMatrix (⇑b : (a : ι) → M))).charpoly
    (Matrix.charpoly.{u_1, u_2} (n := ChooseBasisIndex R M)
      ((toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f))
⊢ Eq (α := R[X])
    (HMul.hMul (β := Matrix.{u_2, w, u_1} (ChooseBasisIndex R M) ι R)
        (HMul.hMul (α := Matrix.{w, u_2, u_1} ι (ChooseBasisIndex R M) R) (β :=
          Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
          (b.toMatrix (⇑b' : (a : ChooseBasisIndex R M) → M))
          ((toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f :
            Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R))
        (b'.toMatrix (⇑b : (a : ι) → M))).charpoly
    (Matrix.charpoly.{u_1, u_2} (n := ChooseBasisIndex R M)
      ((toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f))

Tactic:
set P := b.toMatrix b'

Premises used: Module.Basis.toMatrix, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
h : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix.{w, u_2, u_1} ι (ChooseBasisIndex R M) R := b.toMatrix (⇑b' : (a : ChooseBasisIndex R M) → M)
set :
  let A : Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R :=
    (toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f;
  Eq (α := R[X])
    (HMul.hMul (β := Matrix.{u_2, w, u_1} (ChooseBasisIndex R M) ι R) (P * A) (b'.toMatrix (⇑b : (a : ι) → M))).charpoly
    A.charpoly
⊢ Eq (α := R[X])
    (HMul.hMul (β := Matrix.{u_2, w, u_1} (ChooseBasisIndex R M) ι R)
        (HMul.hMul (β := Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) P
          ((toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f :
            Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R))
        (b'.toMatrix (⇑b : (a : ι) → M))).charpoly
    (Matrix.charpoly.{u_1, u_2} (n := ChooseBasisIndex R M)
      ((toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f))

Tactic:
set A := toMatrix b' b' f

Premises used: DFunLike.coe, LinearMap.toMatrix
-- Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
h : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix.{w, u_2, u_1} ι (ChooseBasisIndex R M) R := b.toMatrix (⇑b' : (a : ChooseBasisIndex R M) → M)
A : Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R :=
  (toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f
set :
  let Q : Matrix.{u_2, w, u_1} (ChooseBasisIndex R M) ι R := b'.toMatrix (⇑b : (a : ι) → M);
  Eq (α := R[X]) (P * A * Q).charpoly A.charpoly
⊢ Eq (α := R[X])
    (HMul.hMul (β := Matrix.{u_2, w, u_1} (ChooseBasisIndex R M) ι R) (P * A) (b'.toMatrix (⇑b : (a : ι) → M))).charpoly
    A.charpoly

Tactic:
set Q := b'.toMatrix b

Premises used: Module.Basis.toMatrix, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
h : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix.{w, u_2, u_1} ι (ChooseBasisIndex R M) R := b.toMatrix (⇑b' : (a : ChooseBasisIndex R M) → M)
A : Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R :=
  (toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f
Q : Matrix.{u_2, w, u_1} (ChooseBasisIndex R M) ι R := b'.toMatrix (⇑b : (a : ι) → M)
e : Equiv.{w + 1, u_2 + 1} ι (ChooseBasisIndex R M) := b.indexEquiv b'
ι' : Type u_2 := ChooseBasisIndex R M
φ : Matrix ι ι R ≃ₗ[R] Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R :=
  reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
⊢ Eq (α := R[X]) (P * A * Q).charpoly
    (Matrix.charpoly.{u_1, u_2} (n := ChooseBasisIndex R M)
      ((φ : (a : Matrix ι ι R) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) (P * A * Q)))

Tactic:
(charpoly_reindex ..).symm

Premises used: Multiset.sum, Multiset.foldr, Matrix.submatrix, dotProduct, Matrix.charpoly_reindex, Eq.symm, Finset.sum
-- Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
h : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix.{w, u_2, u_1} ι (ChooseBasisIndex R M) R := b.toMatrix (⇑b' : (a : ChooseBasisIndex R M) → M)
A : Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R :=
  (toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f
Q : Matrix.{u_2, w, u_1} (ChooseBasisIndex R M) ι R := b'.toMatrix (⇑b : (a : ι) → M)
e : Equiv.{w + 1, u_2 + 1} ι (ChooseBasisIndex R M) := b.indexEquiv b'
ι' : Type u_2 := ChooseBasisIndex R M
φ : Matrix ι ι R ≃ₗ[R] Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R :=
  reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
rw :
  Eq (α := R[X])
    (Matrix.charpoly.{u_1, u_2} (n := ChooseBasisIndex R M)
      ((φ : (a : Matrix ι ι R) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) (P * A * Q)))
    (HMul.hMul (α := Matrix (ChooseBasisIndex R M) ι' R) (β := Matrix ι' (ChooseBasisIndex R M) R)
        ((reindexLinearEquiv R R e (Equiv.refl ι') : (a : Matrix ι ι' R) → Matrix (ChooseBasisIndex R M) ι' R) (P * A) :
          Matrix (ChooseBasisIndex R M) ι' R)
        ((φ₃ : (a : Matrix ι' ι R) → Matrix ι' (ChooseBasisIndex R M) R) Q :
          Matrix ι' (ChooseBasisIndex R M) R)).charpoly
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := R[X])
    (Matrix.charpoly.{u_1, u_2} (n := ChooseBasisIndex R M)
      ((φ : (a : Matrix ι ι R) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) (P * A * Q)))
    (Matrix.charpoly.{u_1, u_2} (n := ChooseBasisIndex R M)
      ((reindexLinearEquiv R R e e : (a : Matrix ι ι R) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        (P * A * Q)))
⊢ Eq (α := R[X])
    (Matrix.charpoly.{u_1, u_2} (n := ChooseBasisIndex R M)
      ((φ : (a : Matrix ι ι R) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) (P * A * Q)))
    (HMul.hMul (β := Matrix ι' (ChooseBasisIndex R M) R)
        (HMul.hMul (α := Matrix (ChooseBasisIndex R M) ι' R) (β := Matrix ι' ι' R)
          ((φ₁ : (a : Matrix ι ι' R) → Matrix (ChooseBasisIndex R M) ι' R) P : Matrix (ChooseBasisIndex R M) ι' R)
          ((φ₂ : (a : Matrix ι' ι' R) → Matrix ι' ι' R) A : Matrix ι' ι' R))
        ((φ₃ : (a : Matrix ι' ι R) → Matrix ι' (ChooseBasisIndex R M) R) Q :
          Matrix ι' (ChooseBasisIndex R M) R)).charpoly

Tactic:
rw [reindexLinearEquiv_mul, reindexLinearEquiv_mul]

Premises used: Matrix.reindexLinearEquiv_mul
-- Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
h : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix.{w, u_2, u_1} ι (ChooseBasisIndex R M) R := b.toMatrix (⇑b' : (a : ChooseBasisIndex R M) → M)
A : Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R :=
  (toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f
Q : Matrix.{u_2, w, u_1} (ChooseBasisIndex R M) ι R := b'.toMatrix (⇑b : (a : ι) → M)
e : Equiv.{w + 1, u_2 + 1} ι (ChooseBasisIndex R M) := b.indexEquiv b'
ι' : Type u_2 := ChooseBasisIndex R M
φ : Matrix ι ι R ≃ₗ[R] Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R :=
  reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
rw :
  Eq (α := R[X])
    (HMul.hMul (β := Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        (HMul.hMul (α := Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) (β :=
          Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
          ((φ₃ : (a : Matrix ι' ι R) → Matrix ι' (ChooseBasisIndex R M) R) Q : Matrix ι' (ChooseBasisIndex R M) R)
          ((φ₁ : (a : Matrix ι ι' R) → Matrix (ChooseBasisIndex R M) ι' R) P : Matrix (ChooseBasisIndex R M) ι' R))
        ((φ₂ : (a : Matrix ι' ι' R) → Matrix ι' ι' R) A : Matrix ι' ι' R)).charpoly
    A.charpoly
⊢ Eq (α := R[X])
    (HMul.hMul (β := Matrix ι' (ChooseBasisIndex R M) R)
        (HMul.hMul (α := Matrix (ChooseBasisIndex R M) ι' R) (β := Matrix ι' ι' R)
          ((φ₁ : (a : Matrix ι ι' R) → Matrix (ChooseBasisIndex R M) ι' R) P : Matrix (ChooseBasisIndex R M) ι' R)
          ((φ₂ : (a : Matrix ι' ι' R) → Matrix ι' ι' R) A : Matrix ι' ι' R))
        ((φ₃ : (a : Matrix ι' ι R) → Matrix ι' (ChooseBasisIndex R M) R) Q :
          Matrix ι' (ChooseBasisIndex R M) R)).charpoly
    A.charpoly

Tactic:
rw [charpoly_mul_comm, ← mul_assoc]

Premises used: mul_assoc, Matrix.charpoly_mul_comm
-- Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
h : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix.{w, u_2, u_1} ι (ChooseBasisIndex R M) R := b.toMatrix (⇑b' : (a : ChooseBasisIndex R M) → M)
A : Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R :=
  (toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f
Q : Matrix.{u_2, w, u_1} (ChooseBasisIndex R M) ι R := b'.toMatrix (⇑b : (a : ι) → M)
e : Equiv.{w + 1, u_2 + 1} ι (ChooseBasisIndex R M) := b.indexEquiv b'
ι' : Type u_2 := ChooseBasisIndex R M
φ : Matrix ι ι R ≃ₗ[R] Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R :=
  reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
⊢ Eq (α := R[X])
    (HMul.hMul (β := Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        (HMul.hMul (α := Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) (β :=
          Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
          ((φ₃ : (a : Matrix ι' ι R) → Matrix ι' (ChooseBasisIndex R M) R) Q : Matrix ι' (ChooseBasisIndex R M) R)
          ((φ₁ : (a : Matrix ι ι' R) → Matrix (ChooseBasisIndex R M) ι' R) P : Matrix (ChooseBasisIndex R M) ι' R))
        ((φ₂ : (a : Matrix ι' ι' R) → Matrix ι' ι' R) A : Matrix ι' ι' R)).charpoly
    A.charpoly

Tactic:
simp [P, Q, φ₁, φ₂, φ₃]
-- Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
ι : Type w
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
h : Nontrivial R
b' : Basis (ChooseBasisIndex R M) R M := chooseBasis R M
P : Matrix.{w, u_2, u_1} ι (ChooseBasisIndex R M) R := b.toMatrix (⇑b' : (a : ChooseBasisIndex R M) → M)
A : Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R :=
  (toMatrix b' b' : (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) f
Q : Matrix.{u_2, w, u_1} (ChooseBasisIndex R M) ι R := b'.toMatrix (⇑b : (a : ι) → M)
e : Equiv.{w + 1, u_2 + 1} ι (ChooseBasisIndex R M) := b.indexEquiv b'
ι' : Type u_2 := ChooseBasisIndex R M
φ : Matrix ι ι R ≃ₗ[R] Matrix.{u_2, u_2, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R :=
  reindexLinearEquiv R R e e
φ₁ : Matrix ι ι' R ≃ₗ[R] Matrix (ChooseBasisIndex R M) ι' R := reindexLinearEquiv R R e (Equiv.refl ι')
φ₂ : Matrix ι' ι' R ≃ₗ[R] Matrix ι' ι' R := reindexLinearEquiv R R (Equiv.refl ι') (Equiv.refl ι')
φ₃ : Matrix ι' ι R ≃ₗ[R] Matrix ι' (ChooseBasisIndex R M) R := reindexLinearEquiv R R (Equiv.refl ι') e
A₁ :
  Eq (α := R[X])
    (Matrix.charpoly.{u_1, u_2} (n := ChooseBasisIndex R M)
      ((φ : (a : Matrix ι ι R) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) (P * A * Q)))
    (HMul.hMul (β := Matrix ι' (ChooseBasisIndex R M) R)
        (HMul.hMul (α := Matrix (ChooseBasisIndex R M) ι' R) (β := Matrix ι' ι' R)
          ((φ₁ : (a : Matrix ι ι' R) → Matrix (ChooseBasisIndex R M) ι' R) P : Matrix (ChooseBasisIndex R M) ι' R)
          ((φ₂ : (a : Matrix ι' ι' R) → Matrix ι' ι' R) A : Matrix ι' ι' R))
        ((φ₃ : (a : Matrix ι' ι R) → Matrix ι' (ChooseBasisIndex R M) R) Q :
          Matrix ι' (ChooseBasisIndex R M) R)).charpoly
A₂ :
  Eq (α := R[X])
    (HMul.hMul (β := Matrix ι' (ChooseBasisIndex R M) R)
        (HMul.hMul (α := Matrix (ChooseBasisIndex R M) ι' R) (β := Matrix ι' ι' R)
          ((φ₁ : (a : Matrix ι ι' R) → Matrix (ChooseBasisIndex R M) ι' R) P : Matrix (ChooseBasisIndex R M) ι' R)
          ((φ₂ : (a : Matrix ι' ι' R) → Matrix ι' ι' R) A : Matrix ι' ι' R))
        ((φ₃ : (a : Matrix ι' ι R) → Matrix ι' (ChooseBasisIndex R M) R) Q :
          Matrix ι' (ChooseBasisIndex R M) R)).charpoly
    A.charpoly
⊢ Eq (α := R[X]) (P * A * Q).charpoly A.charpoly

Tactic:
calc
    (P * A * Q).charpoly = (φ (P * A * Q)).charpoly := (charpoly_reindex ..).symm
    _ = (φ₁ P * φ₂ A * φ₃ Q).charpoly := by rw [reindexLinearEquiv_mul, reindexLinearEquiv_mul]
    _ = A.charpoly := by rw [charpoly_mul_comm, ← mul_assoc]; simp [P, Q, φ₁, φ₂, φ₃]

Premises used: HMul.hMul, Matrix.charpoly_reindex, Eq.symm, DFunLike.coe, Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Module.Finite R M₁
inst_4 : Free R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : Module.Finite R M₂
inst_8 : Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
rw :
  Eq.{u_1 + 1} (α := R[X])
    (charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
      ((LinearMap.toMatrix (b.map e) (b.map e) :
          (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
        ((e.conj : (a : End R M₁) → End R M₂) φ)))
    (charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
      ((LinearMap.toMatrix b b : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) φ))
⊢ LinearMap.charpoly.{u_1, u_4} (M := M₂) ((e.conj : (a : End R M₁) → End R M₂) φ) = LinearMap.charpoly φ

Tactic:
rw [← LinearMap.charpoly_toMatrix φ b, ← LinearMap.charpoly_toMatrix (e.conj φ) (b.map e)]

Premises used: Module.Basis.map, DFunLike.coe, LinearMap.charpoly_toMatrix, LinearEquiv.conj
-- Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Module.Finite R M₁
inst_4 : Free R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : Module.Finite R M₂
inst_8 : Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
e_M :
  Eq (α := Matrix.{u_3, u_3, u_1} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
    ((LinearMap.toMatrix (b.map e) (b.map e) :
          (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
        ((e.conj : (a : End R M₁) → End R M₂) φ) :
      Matrix.{u_3, u_3, u_1} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
    ((LinearMap.toMatrix b b : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) φ :
      Matrix.{u_3, u_3, u_1} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
⊢ Eq.{u_1 + 1} (α := R[X])
    (charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
      ((LinearMap.toMatrix (b.map e) (b.map e) :
          (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
        ((e.conj : (a : End R M₁) → End R M₂) φ)))
    (charpoly.{u_1, u_3} (n := ChooseBasisIndex R M₁)
      ((LinearMap.toMatrix b b : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) φ))

Tactic:
congr 1
-- Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Module.Finite R M₁
inst_4 : Free R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : Module.Finite R M₂
inst_8 : Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
e_M :
  ∀ (i j : ChooseBasisIndex R M₁),
    Eq.{u_1 + 1} (α := R)
      ((LinearMap.toMatrix (b.map e) (b.map e) :
            (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
          ((e.conj : (a : End R M₁) → End R M₂) φ) i j :
        R)
      ((LinearMap.toMatrix b b : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) φ i j :
        R)
⊢ Eq (α := Matrix.{u_3, u_3, u_1} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
    ((LinearMap.toMatrix (b.map e) (b.map e) :
          (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
        ((e.conj : (a : End R M₁) → End R M₂) φ) :
      Matrix.{u_3, u_3, u_1} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
    ((LinearMap.toMatrix b b : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) φ :
      Matrix.{u_3, u_3, u_1} (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)

Tactic:
ext i j : 1
-- Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Goal:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Module.Finite R M₁
inst_4 : Free R M₁
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
inst_7 : Module.Finite R M₂
inst_8 : Free R M₂
e : M₁ ≃ₗ[R] M₂
φ : End R M₁
b : Basis (ChooseBasisIndex R M₁) R M₁ := chooseBasis R M₁
i j : ChooseBasisIndex R M₁
⊢ Eq.{u_1 + 1} (α := R)
    ((LinearMap.toMatrix (b.map e) (b.map e) :
          (a : M₂ →ₗ[R] M₂) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R)
        ((e.conj : (a : End R M₁) → End R M₂) φ) i j :
      R)
    ((LinearMap.toMatrix b b : (a : M₁ →ₗ[R] M₁) → Matrix (ChooseBasisIndex R M₁) (ChooseBasisIndex R M₁) R) φ i j : R)

Tactic:
simp [LinearMap.toMatrix]

Premises used: LinearMap.toMatrix
-- Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
n : Type u_5
inst_5 : Fintype n
inst_6 : DecidableEq n
A : Matrix n n R
b : Basis n R M
⊢ Eq (α := R[X]) (LinearMap.charpoly.{u_1, u_2} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) A)) A.charpoly

Tactic:
simp [← LinearMap.charpoly_toMatrix (A.toLin b b) b]

Premises used: Matrix.toLin, DFunLike.coe, LinearMap.charpoly_toMatrix
-- Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Goal:
R : Type u_1
inst : CommRing R
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n R
rw :
  Eq (α := R[X])
    (LinearMap.charpoly (M := n → R)
      ((toLin (Pi.basisFun R n) (Pi.basisFun R n) : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) A))
    A.charpoly
rw₁ rw₂ : Eq (α := R[X]) A.charpoly A.charpoly
⊢ Eq (α := R[X]) (LinearMap.charpoly (M := n → R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) A)) A.charpoly

Tactic:
rw [← Matrix.toLin_eq_toLin', charpoly_toLin]

Premises used: Matrix.charpoly_toLin, Matrix.toLin_eq_toLin'
-- Module: Mathlib.LinearAlgebra.Charpoly.ToMatrix
Goal:
R : Type u_1
inst : CommRing R
n : Type u_5
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n R
⊢ Eq (α := R[X]) (LinearMap.charpoly (M := n → R) A.mulVecLin) A.charpoly

Tactic:
charpoly_toLin' A

Premises used: Matrix.charpoly_toLin'