awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (hypothesis)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : Free R V
f : V →ₗ[R] V
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
hV1 : finrank R V = 1
⊢ ∃ (a : R), f = HSMul.hSMul (β := V →ₗ[R] V) a 1
have hV1₁ : Nonempty (Basis Unit R V)
Tactic: rw [finrank_eq_one_iff Unit] at hV1
Cleared hypotheses: hV1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : Free R V
f : V →ₗ[R] V
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
hV1 : Nonempty (Basis Unit R V)
b : Basis Unit R V := Classical.ofNonempty
⊢ ∃ (a : R), f = HSMul.hSMul (β := V →ₗ[R] V) a 1
have h₁ : f =
  HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V →ₗ[R] V)
    ((b.coord () : (a : V) → R) ((f : (a : V) → V) ((b : (a : Unit) → V) () : V) : V) : R) 1
Tactic: use b.coord () (f (b ()))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : Free R V
f : V →ₗ[R] V
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
hV1 : Nonempty (Basis Unit R V)
b : Basis Unit R V := Classical.ofNonempty
⊢ f =
    HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V →ₗ[R] V)
      ((b.coord () : (a : V) → R) ((f : (a : V) → V) ((b : (a : Unit) → V) () : V) : V) : R) 1
have h₁ : ∀ (i : Unit),
  Eq (α := V) ((f : (a : V) → V) ((b : (a : Unit) → V) i : V) : V)
    ((HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V →ₗ[R] V)
            ((b.coord () : (a : V) → R) ((f : (a : V) → V) ((b : (a : Unit) → V) () : V) : V) : R) 1 :
          (a : V) → V)
        ((b : (a : Unit) → V) i : V) :
      V)
Tactic: apply b.ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : Free R V
f : V →ₗ[R] V
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
hV1 : Nonempty (Basis Unit R V)
b : Basis Unit R V := Classical.ofNonempty
i : Unit
⊢ Eq (α := V) ((f : (a : V) → V) ((b : (a : Unit) → V) i : V) : V)
    ((HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V →ₗ[R] V)
            ((b.coord () : (a : V) → R) ((f : (a : V) → V) ((b : (a : Unit) → V) () : V) : V) : R) 1 :
          (a : V) → V)
        ((b : (a : Unit) → V) i : V) :
      V)
have h₁ : Eq.{u_2 + 1} (α := V)
  ((linearCombination R (⇑b : (a : Unit) → V) : (a : Unit →₀ R) → V)
      ((b.repr : (a : V) → Unit →₀ R) ((f : (a : V) → V) ((b : (a : Unit) → V) i : V)) : Unit →₀ R) :
    V)
  ((HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := V →ₗ[R] V)
          ((b.coord () : (a : V) → R) ((f : (a : V) → V) ((b : (a : Unit) → V) () : V) : V) : R) 1 :
        (a : V) → V)
      ((b : (a : Unit) → V) i : V) :
    V)
Tactic: nth_rewrite 1 [← b.linearCombination_repr (f (b i))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Center (goal)
Goal:
R : Type u_1
V : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : Free R V
f : V →ₗ[R] V
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
hV1 : ¬finrank R V = 1
⊢ ∃ (a : R), f = HSMul.hSMul (β := V →ₗ[R] V) a 1
have neg : ∀ (a : ↥(Subring.center R))
  (h :
    ∀ (v : V),
      ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (HSMul.hSMul (β := V →ₗ[R] V) a 1 : (a : V) → V) v]),
  ∃ (a_1 : R), HSMul.hSMul (β := V →ₗ[R] V) a 1 = HSMul.hSMul (β := V →ₗ[R] V) a_1 1
Tactic: obtain ⟨a, rfl⟩ := exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent hV1 h
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.BaseChange (hypothesis)
Goal:
R : Type u_3
M : Type u_2
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
A : Type u_1
inst_5 : CommRing A
inst_6 : Algebra R A
⊢ Eq (α := Polynomial A) (charpoly (M := TensorProduct R A M) (baseChange A f))
    (Polynomial.map (algebraMap R A) f.charpoly)
have a : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.BaseChange (hypothesis)
Goal:
R : Type u_3
M : Type u_2
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
A : Type u_1
inst_5 : CommRing A
inst_6 : Algebra R A
h : Nontrivial A
⊢ Eq (α := Polynomial A) (charpoly (M := TensorProduct R A M) (baseChange A f))
    (Polynomial.map (algebraMap R A) f.charpoly)
have this : Nontrivial R
Tactic: have := (algebraMap R A).domain_nontrivial
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.BaseChange (goal)
Goal:
R : Type u_3
M : Type u_2
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
A : Type u_1
inst_5 : CommRing A
inst_6 : Algebra R A
h : Nontrivial A
this : Nontrivial R
I : Type u_2 := Module.Free.ChooseBasisIndex R M
b : Module.Basis I R M := Module.Free.chooseBasis R M
⊢ Eq (α := Polynomial A) (charpoly (M := TensorProduct R A M) (baseChange A f))
    (Polynomial.map (algebraMap R A) f.charpoly)
have rw : Eq.{u_1 + 1} (α := Polynomial A)
  (Matrix.charpoly.{u_1, u_2} (n := I)
    ((toMatrix (Module.Basis.baseChange A b) (Module.Basis.baseChange A b) :
        (a : TensorProduct R A M →ₗ[A] TensorProduct R A M) → Matrix I I A)
      (baseChange A f)))
  (Matrix.charpoly.{u_1, u_2} (n := I)
    (Matrix.map.{u_3, u_1, u_2, u_2} (α := R) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix I I R) f)
      (⇑(algebraMap R A) : (a : R) → A)))
Tactic: rw [← f.charpoly_toMatrix b, ← (f.baseChange A).charpoly_toMatrix (b.baseChange A),
    ← Matrix.charpoly_map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.BaseChange (goal)
Goal:
R : Type u_3
M : Type u_2
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
A : Type u_1
inst_5 : CommRing A
inst_6 : Algebra R A
h : Nontrivial A
this : Nontrivial R
I : Type u_2 := Module.Free.ChooseBasisIndex R M
b : Module.Basis I R M := Module.Free.chooseBasis R M
⊢ Eq.{u_1 + 1} (α := Polynomial A)
    (Matrix.charpoly.{u_1, u_2} (n := I)
      ((toMatrix (Module.Basis.baseChange A b) (Module.Basis.baseChange A b) :
          (a : TensorProduct R A M →ₗ[A] TensorProduct R A M) → Matrix I I A)
        (baseChange A f)))
    (Matrix.charpoly.{u_1, u_2} (n := I)
      (Matrix.map.{u_3, u_1, u_2, u_2} (α := R) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix I I R) f)
        (⇑(algebraMap R A) : (a : R) → A)))
have e_M : Eq (α := Matrix I I A)
  ((toMatrix (Module.Basis.baseChange A b) (Module.Basis.baseChange A b) :
        (a : TensorProduct R A M →ₗ[A] TensorProduct R A M) → Matrix I I A)
      (baseChange A f) :
    Matrix I I A)
  (Matrix.map.{u_3, u_1, u_2, u_2} (α := R) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix I I R) f)
      (⇑(algebraMap R A) : (a : R) → A) :
    Matrix I I A)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.BaseChange (goal)
Goal:
R : Type u_3
M : Type u_2
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
A : Type u_1
inst_5 : CommRing A
inst_6 : Algebra R A
h : Nontrivial A
this : Nontrivial R
I : Type u_2 := Module.Free.ChooseBasisIndex R M
b : Module.Basis I R M := Module.Free.chooseBasis R M
⊢ Eq (α := Matrix I I A)
    ((toMatrix (Module.Basis.baseChange A b) (Module.Basis.baseChange A b) :
          (a : TensorProduct R A M →ₗ[A] TensorProduct R A M) → Matrix I I A)
        (baseChange A f) :
      Matrix I I A)
    (Matrix.map.{u_3, u_1, u_2, u_2} (α := R) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix I I R) f)
        (⇑(algebraMap R A) : (a : R) → A) :
      Matrix I I A)
have e_M : ∀ (i j : I),
  Eq.{u_1 + 1} (α := A)
    ((toMatrix (Module.Basis.baseChange A b) (Module.Basis.baseChange A b) :
          (a : TensorProduct R A M →ₗ[A] TensorProduct R A M) → Matrix I I A)
        (baseChange A f) i j :
      A)
    (Matrix.map.{u_3, u_1, u_2, u_2} (α := R) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix I I R) f)
        (⇑(algebraMap R A) : (a : R) → A) i j :
      A)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.BaseChange (hypothesis)
Goal:
R : Type u_1
M : Type u_2
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
⊢ (LinearMap.det : (a : M →ₗ[R] M) → R) f = HPow.hPow (α := R) (-1) (Module.finrank R M) * f.charpoly.coeff 0
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.BaseChange (goal)
Goal:
R : Type u_1
M : Type u_2
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
h : Nontrivial R
⊢ (LinearMap.det : (a : M →ₗ[R] M) → R) f = HPow.hPow (α := R) (-1) (Module.finrank R M) * f.charpoly.coeff 0
have rw : Matrix.det.{u_1, u_2} (n := Module.Free.ChooseBasisIndex R M)
    ((toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M) :
        (a : M →ₗ[R] M) → Matrix (Module.Free.ChooseBasisIndex R M) (Module.Free.ChooseBasisIndex R M) R)
      f) =
  HPow.hPow (α := R) (-1) (Module.finrank R M) * f.charpoly.coeff 0
Tactic: rw [← LinearMap.det_toMatrix (Module.Free.chooseBasis R M), Matrix.det_eq_sign_charpoly_coeff,
    ← Module.finrank_eq_card_chooseBasisIndex, charpoly_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.BaseChange (goal)
Goal:
R : Type u_1
M : Type u_2
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
h : Nontrivial R
rw :
  Matrix.det.{u_1, u_2} (n := Module.Free.ChooseBasisIndex R M)
      ((toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M) :
          (a : M →ₗ[R] M) → Matrix (Module.Free.ChooseBasisIndex R M) (Module.Free.ChooseBasisIndex R M) R)
        f) =
    HPow.hPow (α := R) (-1) (Module.finrank R M) * f.charpoly.coeff 0
⊢ (LinearMap.det : (a : M →ₗ[R] M) → R) f = HPow.hPow (α := R) (-1) (Module.finrank R M) * f.charpoly.coeff 0
have rw₁ : HPow.hPow (α := R) (-1) (Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R M)) *
    Polynomial.coeff
      (Matrix.charpoly.{u_1, u_2} (n := Module.Free.ChooseBasisIndex R M)
        ((toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M) :
            (a : M →ₗ[R] M) → Matrix (Module.Free.ChooseBasisIndex R M) (Module.Free.ChooseBasisIndex R M) R)
          f))
      0 =
  HPow.hPow (α := R) (-1) (Module.finrank R M) * f.charpoly.coeff 0
Tactic: rw [← LinearMap.det_toMatrix (Module.Free.chooseBasis R M), Matrix.det_eq_sign_charpoly_coeff,
    ← Module.finrank_eq_card_chooseBasisIndex, charpoly_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.BaseChange (goal)
Goal:
R : Type u_1
M : Type u_2
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
h : Nontrivial R
rw :
  Matrix.det.{u_1, u_2} (n := Module.Free.ChooseBasisIndex R M)
      ((toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M) :
          (a : M →ₗ[R] M) → Matrix (Module.Free.ChooseBasisIndex R M) (Module.Free.ChooseBasisIndex R M) R)
        f) =
    HPow.hPow (α := R) (-1) (Module.finrank R M) * f.charpoly.coeff 0
rw₁ :
  HPow.hPow (α := R) (-1) (Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R M)) *
      Polynomial.coeff
        (Matrix.charpoly.{u_1, u_2} (n := Module.Free.ChooseBasisIndex R M)
          ((toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M) :
              (a : M →ₗ[R] M) → Matrix (Module.Free.ChooseBasisIndex R M) (Module.Free.ChooseBasisIndex R M) R)
            f))
        0 =
    HPow.hPow (α := R) (-1) (Module.finrank R M) * f.charpoly.coeff 0
⊢ (LinearMap.det : (a : M →ₗ[R] M) → R) f = HPow.hPow (α := R) (-1) (Module.finrank R M) * f.charpoly.coeff 0
have rw₂ : HPow.hPow (α := R) (-1) (Module.finrank R M) *
    Polynomial.coeff
      (Matrix.charpoly.{u_1, u_2} (n := Module.Free.ChooseBasisIndex R M)
        ((toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M) :
            (a : M →ₗ[R] M) → Matrix (Module.Free.ChooseBasisIndex R M) (Module.Free.ChooseBasisIndex R M) R)
          f))
      0 =
  HPow.hPow (α := R) (-1) (Module.finrank R M) * f.charpoly.coeff 0
Tactic: rw [← LinearMap.det_toMatrix (Module.Free.chooseBasis R M), Matrix.det_eq_sign_charpoly_coeff,
    ← Module.finrank_eq_card_chooseBasisIndex, charpoly_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.BaseChange (goal)
Goal:
R : Type u_1
M : Type u_2
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
h : Nontrivial R
rw :
  Matrix.det.{u_1, u_2} (n := Module.Free.ChooseBasisIndex R M)
      ((toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M) :
          (a : M →ₗ[R] M) → Matrix (Module.Free.ChooseBasisIndex R M) (Module.Free.ChooseBasisIndex R M) R)
        f) =
    HPow.hPow (α := R) (-1) (Module.finrank R M) * f.charpoly.coeff 0
rw₁ :
  HPow.hPow (α := R) (-1) (Fintype.card.{u_2} (Module.Free.ChooseBasisIndex R M)) *
      Polynomial.coeff
        (Matrix.charpoly.{u_1, u_2} (n := Module.Free.ChooseBasisIndex R M)
          ((toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M) :
              (a : M →ₗ[R] M) → Matrix (Module.Free.ChooseBasisIndex R M) (Module.Free.ChooseBasisIndex R M) R)
            f))
        0 =
    HPow.hPow (α := R) (-1) (Module.finrank R M) * f.charpoly.coeff 0
rw₂ :
  HPow.hPow (α := R) (-1) (Module.finrank R M) *
      Polynomial.coeff
        (Matrix.charpoly.{u_1, u_2} (n := Module.Free.ChooseBasisIndex R M)
          ((toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M) :
              (a : M →ₗ[R] M) → Matrix (Module.Free.ChooseBasisIndex R M) (Module.Free.ChooseBasisIndex R M) R)
            f))
        0 =
    HPow.hPow (α := R) (-1) (Module.finrank R M) * f.charpoly.coeff 0
⊢ (LinearMap.det : (a : M →ₗ[R] M) → R) f = HPow.hPow (α := R) (-1) (Module.finrank R M) * f.charpoly.coeff 0
have rw₃ : HPow.hPow (α := R) (-1) (Module.finrank R M) *
    Polynomial.coeff
      (Matrix.charpoly.{u_1, u_2} (n := Module.Free.ChooseBasisIndex R M)
        ((toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M) :
            (a : M →ₗ[R] M) → Matrix (Module.Free.ChooseBasisIndex R M) (Module.Free.ChooseBasisIndex R M) R)
          f))
      0 =
  HPow.hPow (α := R) (-1) (Module.finrank R M) *
    Polynomial.coeff
      (Matrix.charpoly.{u_1, u_2} (n := Module.Free.ChooseBasisIndex R M)
        ((toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M) :
            (a : M →ₗ[R] M) → Matrix (Module.Free.ChooseBasisIndex R M) (Module.Free.ChooseBasisIndex R M) R)
          f))
      0
Tactic: rw [← LinearMap.det_toMatrix (Module.Free.chooseBasis R M), Matrix.det_eq_sign_charpoly_coeff,
    ← Module.finrank_eq_card_chooseBasisIndex, charpoly_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.BaseChange (hypothesis)
Goal:
R : Type u_3
M : Type u_2
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
A : Type u_1
inst_5 : CommRing A
inst_6 : Algebra R A
⊢ Eq.{u_1 + 1} (α := A)
    (((LinearMap.det (M := TensorProduct R A M) (A := A) : (TensorProduct R A M →ₗ[A] TensorProduct R A M) →* A) :
          (a : TensorProduct R A M →ₗ[A] TensorProduct R A M) → A)
        (baseChange A f) :
      A)
    ((algebraMap R A : (a : R) → A) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) : A)
have a : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.BaseChange (hypothesis)
Goal:
R : Type u_3
M : Type u_2
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
A : Type u_1
inst_5 : CommRing A
inst_6 : Algebra R A
h : Nontrivial A
⊢ Eq.{u_1 + 1} (α := A)
    (((LinearMap.det (M := TensorProduct R A M) (A := A) : (TensorProduct R A M →ₗ[A] TensorProduct R A M) →* A) :
          (a : TensorProduct R A M →ₗ[A] TensorProduct R A M) → A)
        (baseChange A f) :
      A)
    ((algebraMap R A : (a : R) → A) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) : A)
have this : Nontrivial R
Tactic: have := (algebraMap R A).domain_nontrivial
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.BaseChange (goal)
Goal:
R : Type u_3
M : Type u_2
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
A : Type u_1
inst_5 : CommRing A
inst_6 : Algebra R A
h : Nontrivial A
this : Nontrivial R
⊢ Eq.{u_1 + 1} (α := A)
    (((LinearMap.det (M := TensorProduct R A M) (A := A) : (TensorProduct R A M →ₗ[A] TensorProduct R A M) →* A) :
          (a : TensorProduct R A M →ₗ[A] TensorProduct R A M) → A)
        (baseChange A f) :
      A)
    ((algebraMap R A : (a : R) → A) ((LinearMap.det : (a : M →ₗ[R] M) → R) f : R) : A)
have rw : HPow.hPow (α := A) (-1) (Module.finrank A (TensorProduct R A M)) *
    Polynomial.coeff (charpoly (M := TensorProduct R A M) (baseChange A f)) 0 =
  (algebraMap R A : (a : R) → A) (HPow.hPow (α := R) (-1) (Module.finrank R M) * f.charpoly.coeff 0)
Tactic: rw [LinearMap.det_eq_sign_charpoly_coeff, LinearMap.det_eq_sign_charpoly_coeff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Charpoly.BaseChange (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Free R M
inst_4 : Module.Finite R M
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra R A
f : M ≃ₗ[R] M
⊢ Eq.{u_3 + 1} (α := Aˣ)
    (((LinearEquiv.det (R := A) (M := TensorProduct R A M) : (TensorProduct R A M ≃ₗ[A] TensorProduct R A M) →* Aˣ) :
          (a : TensorProduct R A M ≃ₗ[A] TensorProduct R A M) → Aˣ)
        (baseChange R A M M f) :
      Aˣ)
    (((Units.map (↑(algebraMap R A) : R →* A) : MonoidHom.{u_1, u_3} Rˣ Aˣ) : (a : Rˣ) → Aˣ)
        ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f) :
      Aˣ)
have huv : Eq.{u_3 + 1} (α := A)
  (↑(((LinearEquiv.det (R := A) (M := TensorProduct R A M) : (TensorProduct R A M ≃ₗ[A] TensorProduct R A M) →* Aˣ) :
          (a : TensorProduct R A M ≃ₗ[A] TensorProduct R A M) → Aˣ)
        (baseChange R A M M f)) :
    A)
  (↑(((Units.map (↑(algebraMap R A) : R →* A) : MonoidHom.{u_1, u_3} Rˣ Aˣ) : (a : Rˣ) → Aˣ)
        ((LinearEquiv.det : (a : M ≃ₗ[R] M) → Rˣ) f)) :
    A)
Tactic: ext
-- 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
t : R
⊢ eval t f.charpoly =
    (LinearMap.det : (a : M →ₗ[R] M) → R)
      (HSub.hSub (α := M →ₗ[R] M) ((algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) t : M →ₗ[R] M) f)
have rw : eval t
    (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)) =
  (LinearMap.det : (a : M →ₗ[R] M) → R)
    (HSub.hSub (α := M →ₗ[R] M) ((algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) t : M →ₗ[R] M) f)
Tactic: rw [charpoly, Matrix.eval_charpoly, ← LinearMap.det_toMatrix (chooseBasis R M), map_sub,
    scalar_apply, toMatrix_algebraMap, scalar_apply]
-- 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
t : R
rw :
  eval t
      (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)) =
    (LinearMap.det : (a : M →ₗ[R] M) → R)
      (HSub.hSub (α := M →ₗ[R] M) ((algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) t : M →ₗ[R] M) f)
⊢ eval t f.charpoly =
    (LinearMap.det : (a : M →ₗ[R] M) → R)
      (HSub.hSub (α := M →ₗ[R] M) ((algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) t : M →ₗ[R] M) f)
have rw₁ : (HSub.hSub (α := Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) (β :=
      Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
      ((scalar (ChooseBasisIndex R M) : (a : R) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) t :
        Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
      ((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)).det =
  (LinearMap.det : (a : M →ₗ[R] M) → R)
    (HSub.hSub (α := M →ₗ[R] M) ((algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) t : M →ₗ[R] M) f)
Tactic: rw [charpoly, Matrix.eval_charpoly, ← LinearMap.det_toMatrix (chooseBasis R M), map_sub,
    scalar_apply, toMatrix_algebraMap, scalar_apply]
-- 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
t : R
rw :
  eval t
      (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)) =
    (LinearMap.det : (a : M →ₗ[R] M) → R)
      (HSub.hSub (α := M →ₗ[R] M) ((algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) t : M →ₗ[R] M) f)
rw₁ :
  (HSub.hSub (α := Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) (β :=
        Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        ((scalar (ChooseBasisIndex R M) : (a : R) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) t :
          Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
        ((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)).det =
    (LinearMap.det : (a : M →ₗ[R] M) → R)
      (HSub.hSub (α := M →ₗ[R] M) ((algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) t : M →ₗ[R] M) f)
⊢ eval t f.charpoly =
    (LinearMap.det : (a : M →ₗ[R] M) → R)
      (HSub.hSub (α := M →ₗ[R] M) ((algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) t : M →ₗ[R] M) f)
have rw₂ : (HSub.hSub (α := Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) (β :=
      Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
      ((scalar (ChooseBasisIndex R M) : (a : R) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R) t :
        Matrix.{v, v, u} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
      ((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)).det =
  det.{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)
      (HSub.hSub (α := M →ₗ[R] M) ((algebraMap R (M →ₗ[R] M) : (a : R) → M →ₗ[R] M) t : M →ₗ[R] M) f))
Tactic: rw [charpoly, Matrix.eval_charpoly, ← LinearMap.det_toMatrix (chooseBasis R M), map_sub,
    scalar_apply, toMatrix_algebraMap, scalar_apply]