awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (hypothesis)
Goal:
R : Type u
M : Type v
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
inst_5 : StrongRankCondition R
⊢ f.charpoly.natDegree = finrank R M
have this : ∀ (R : Type u) [inst : Semiring R] [InvariantBasisNumber R], Nontrivial R
Tactic: haveI := nontrivial_of_invariantBasisNumber
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (goal)
Goal:
R : Type u
M : Type v
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
inst_5 : StrongRankCondition R
this : ∀ (R : Type u) [inst : Semiring R] [InvariantBasisNumber R], Nontrivial R
⊢ f.charpoly.natDegree = finrank R M
have rw : natDegree.{u} (R := R)
    (Matrix.charpoly.{u, v} (n := ChooseBasisIndex R M)
      ((toMatrix (chooseBasis R M) (chooseBasis R M) :
          (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        f)) =
  finrank R M
Tactic: rw [charpoly, Matrix.charpoly_natDegree_eq_dim, finrank_eq_card_chooseBasisIndex]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (goal)
Goal:
R : Type u
M : Type v
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
inst_5 : StrongRankCondition R
this : ∀ (R : Type u) [inst : Semiring R] [InvariantBasisNumber R], Nontrivial R
rw :
  natDegree.{u} (R := R)
      (Matrix.charpoly.{u, v} (n := ChooseBasisIndex R M)
        ((toMatrix (chooseBasis R M) (chooseBasis R M) :
            (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
          f)) =
    finrank R M
⊢ f.charpoly.natDegree = finrank R M
have rw₁ : Fintype.card.{v} (ChooseBasisIndex R M) = finrank R M
Tactic: rw [charpoly, Matrix.charpoly_natDegree_eq_dim, finrank_eq_card_chooseBasisIndex]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (goal)
Goal:
R : Type u
M : Type v
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
inst_5 : StrongRankCondition R
this : ∀ (R : Type u) [inst : Semiring R] [InvariantBasisNumber R], Nontrivial R
rw :
  natDegree.{u} (R := R)
      (Matrix.charpoly.{u, v} (n := ChooseBasisIndex R M)
        ((toMatrix (chooseBasis R M) (chooseBasis R M) :
            (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
          f)) =
    finrank R M
rw₁ : Fintype.card.{v} (ChooseBasisIndex R M) = finrank R M
⊢ f.charpoly.natDegree = finrank R M
have rw₂ : Fintype.card.{v} (ChooseBasisIndex R M) = Fintype.card.{v} (ChooseBasisIndex R M)
Tactic: rw [charpoly, Matrix.charpoly_natDegree_eq_dim, finrank_eq_card_chooseBasisIndex]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
⊢ Eq.{v + 1} (α := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) f.charpoly : M →ₗ[R] M) (0 : M →ₗ[R] M)
have apply : Eq (α := Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
  (((↑(algEquivMatrix (chooseBasis R M)) :
          Module.End R M ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) :
        (a : Module.End R M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
      ((aeval f : (a : R[X]) → M →ₗ[R] M) f.charpoly) :
    Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
  (0 : Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
Tactic: apply (LinearEquiv.map_eq_zero_iff (algEquivMatrix (chooseBasis R M)).toLinearEquiv).1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
⊢ Eq (α := Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
    (((↑(algEquivMatrix (chooseBasis R M)) :
            Module.End R M ≃ₗ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) :
          (a : Module.End R M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        ((aeval f : (a : R[X]) → M →ₗ[R] M) f.charpoly) :
      Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
    (0 : Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
have rw : Eq (α := Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
  (((aeval
            (((↑(algEquivMatrix (chooseBasis R M)) :
                  Module.End R M →ₐ[R] Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) :
                (a : Module.End R M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
              f) :
          R[X] →ₐ[R] Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) :
        (a : R[X]) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
      (Matrix.charpoly.{u, v} (n := ChooseBasisIndex R M)
        ((toMatrix (chooseBasis R M) (chooseBasis R M) :
            (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
          f)) :
    Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
  (0 : Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
Tactic: rw [AlgEquiv.toLinearEquiv_apply, ← AlgEquiv.coe_algHom, ← Polynomial.aeval_algHom_apply _ _ _,
    charpoly_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
k : ℕ
⊢ f ^ k = (aeval f : (a : R[X]) → M →ₗ[R] M) (HPow.hPow (α := R[X]) X k %ₘ f.charpoly)
have rw : f ^ k = (aeval f : (a : R[X]) → M →ₗ[R] M) (HPow.hPow (α := R[X]) X k)
Tactic: rw [← aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
k : ℕ
rw : f ^ k = (aeval f : (a : R[X]) → M →ₗ[R] M) (HPow.hPow (α := R[X]) X k)
⊢ f ^ k = (aeval f : (a : R[X]) → M →ₗ[R] M) (HPow.hPow (α := R[X]) X k %ₘ f.charpoly)
have rw₁ : f ^ k = HPow.hPow (α := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) X : M →ₗ[R] M) k
Tactic: rw [← aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
k : ℕ
rw : f ^ k = (aeval f : (a : R[X]) → M →ₗ[R] M) (HPow.hPow (α := R[X]) X k)
rw₁ : f ^ k = HPow.hPow (α := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) X : M →ₗ[R] M) k
⊢ f ^ k = (aeval f : (a : R[X]) → M →ₗ[R] M) (HPow.hPow (α := R[X]) X k %ₘ f.charpoly)
have rw₂ : f ^ k = f ^ k
Tactic: rw [← aeval_eq_aeval_mod_charpoly, map_pow, aeval_X]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
⊢ False
have obtain : ∀ (P : R[X]) (hP : minpoly R f = X * P), False
Tactic: obtain ⟨P, hP⟩ := X_dvd_iff.2 h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
⊢ P.degree < degree (minpoly R f)
have rw : P.degree < (P * X).degree
Tactic: rw [hP, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
⊢ P.degree < (P * X).degree
have refine : ∀ (h : P = 0), False
Tactic: refine degree_lt_degree_mul_X fun h => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (hypothesis)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h_1 : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
h : P = 0
⊢ False
have hP₁ : Eq (α := R[X]) (minpoly R f) 0
Tactic: rw [h, mul_zero] at hP
Cleared hypotheses: hP, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (hypothesis)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
⊢ False
have hdegP : P.degree < degree (minpoly R f)
Tactic: have hdegP : P.degree < (minpoly R f).degree := by
    rw [hP, mul_comm]
    refine degree_lt_degree_mul_X fun h => ?_
    rw [h, mul_zero] at hP
    exact minpoly.ne_zero (isIntegral f) hP
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < degree (minpoly R f)
this : Monic (minpoly R f)
⊢ P.Monic
have rwa : ∀ (this : leadingCoeff (minpoly R f) = 1), P.Monic
Tactic: rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < degree (minpoly R f)
this : Monic (minpoly R f)
rwa : ∀ (this : leadingCoeff (minpoly R f) = 1), P.Monic
⊢ P.Monic
have rwa₁ : ∀ (this : (X * P).leadingCoeff = 1), P.Monic
Tactic: rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < degree (minpoly R f)
this : Monic (minpoly R f)
rwa : ∀ (this : leadingCoeff (minpoly R f) = 1), P.Monic
rwa₁ : ∀ (this : (X * P).leadingCoeff = 1), P.Monic
⊢ P.Monic
have rwa₂ : ∀ (this : (P * X).leadingCoeff = 1), P.Monic
Tactic: rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < degree (minpoly R f)
this : Monic (minpoly R f)
rwa : ∀ (this : leadingCoeff (minpoly R f) = 1), P.Monic
rwa₁ : ∀ (this : (X * P).leadingCoeff = 1), P.Monic
rwa₂ : ∀ (this : (P * X).leadingCoeff = 1), P.Monic
⊢ P.Monic
have rwa₃ : ∀ (this : P.leadingCoeff = 1), P.Monic
Tactic: rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < degree (minpoly R f)
this : Monic (minpoly R f)
rwa : ∀ (this : leadingCoeff (minpoly R f) = 1), P.Monic
rwa₁ : ∀ (this : (X * P).leadingCoeff = 1), P.Monic
rwa₂ : ∀ (this : (P * X).leadingCoeff = 1), P.Monic
rwa₃ : ∀ (this : P.leadingCoeff = 1), P.Monic
⊢ P.Monic
have rwa₄ : ∀ (this : P.Monic), P.Monic
Tactic: rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (goal)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < degree (minpoly R f)
⊢ P.Monic
have suffices : Monic (minpoly R f)
Tactic: suffices (minpoly R f).Monic by
      rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (hypothesis)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < degree (minpoly R f)
⊢ False
have hPmonic : P.Monic
Tactic: have hPmonic : P.Monic := by
    suffices (minpoly R f).Monic by
      rwa [Monic.def, hP, mul_comm, leadingCoeff_mul_X, ← Monic.def] at this
    exact minpoly.monic (isIntegral f)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (hypothesis)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < degree (minpoly R f)
hPmonic : P.Monic
⊢ False
have hzero : Eq.{v + 1} (α := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) (minpoly R f) : M →ₗ[R] M) (0 : M →ₗ[R] M)
Tactic: have hzero : aeval f (minpoly R f) = 0 := minpoly.aeval _ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.Basic (hypothesis)
Goal:
R : Type u
M : Type v
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] M
inst_5 : Nontrivial R
hf : Function.Injective (α := M) (β := M) (⇑f : (a : M) → M)
h : coeff (minpoly R f) 0 = 0
P : R[X]
hP : minpoly R f = X * P
hdegP : P.degree < degree (minpoly R f)
hPmonic : P.Monic
hzero : Eq.{v + 1} (α := M →ₗ[R] M) ((aeval f : (a : R[X]) → M →ₗ[R] M) (minpoly R f) : M →ₗ[R] M) (0 : M →ₗ[R] M)
⊢ False
have hzero₁ : ∀ (x : M), Eq (α := M) ((((aeval f : (a : R[X]) → M →ₗ[R] M) P : M →ₗ[R] M) : (a : M) → M) x : M) (0 : M)
Tactic: simp only [hP, Module.End.mul_eq_comp, LinearMap.ext_iff, hf, aeval_X, map_eq_zero_iff, coe_comp,
    map_mul, zero_apply, Function.comp_apply] at hzero
Cleared hypotheses: hzero
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.ToMatrix (hypothesis)
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
⊢ Matrix.charpoly.{u_1, w} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f) = f.charpoly
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.ToMatrix (goal)
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
⊢ 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))
have 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))
Tactic: rw [← basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix b b' b b']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.ToMatrix (goal)
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])
    (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
have 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
Tactic: rw [reindexLinearEquiv_mul, reindexLinearEquiv_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.ToMatrix (goal)
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
⊢ 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
have 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)))
Tactic: rw [reindexLinearEquiv_mul, reindexLinearEquiv_mul]