awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : StrongRankCondition R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Free R V
f : V →ₗ[R] V
hV1 : finrank R V ≠ 1
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
inl : ∀ (hV : Subsingleton V), ∃ (a : ↥(Subring.center R)), f = HSMul.hSMul (β := V →ₗ[R] V) a 1
inr : ∀ (hV : Nontrivial V), ∃ (a : ↥(Subring.center R)), f = HSMul.hSMul (β := V →ₗ[R] V) a 1
⊢ ∃ (a : ↥(Subring.center R)), f = HSMul.hSMul (β := V →ₗ[R] V) a 1

Tactic:
rcases subsingleton_or_nontrivial V with hV | hV

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : StrongRankCondition R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Free R V
f : V →ₗ[R] V
hV1 : finrank R V ≠ 1
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
hV : Subsingleton V
h₁ : f = HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Subring.center R)) (β := V →ₗ[R] V) 1 1
⊢ ∃ (a : ↥(Subring.center R)), f = HSMul.hSMul (β := V →ₗ[R] V) a 1

Tactic:
use 1
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : StrongRankCondition R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Free R V
f : V →ₗ[R] V
hV1 : finrank R V ≠ 1
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
hV : Subsingleton V
h₁ :
  ∀ (x : V),
    Eq (α := V) ((f : (a : V) → V) x : V)
      ((HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Subring.center R)) (β := V →ₗ[R] V) 1 1 : (a : V) → V) x : V)
⊢ f = HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Subring.center R)) (β := V →ₗ[R] V) 1 1

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : StrongRankCondition R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Free R V
f : V →ₗ[R] V
hV1 : finrank R V ≠ 1
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
hV : Subsingleton V
x : V
⊢ Eq (α := V) ((f : (a : V) → V) x : V)
    ((HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(Subring.center R)) (β := V →ₗ[R] V) 1 1 : (a : V) → V) x : V)

Tactic:
apply hV.allEq

Premises used: Subsingleton.allEq
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : StrongRankCondition R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Free R V
f : V →ₗ[R] V
hV1 : finrank R V ≠ 1
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
hV : Nontrivial V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V := Free.chooseBasis R V
inr : ∀ (hι : Subsingleton ι), ∃ (a : ↥(Subring.center R)), f = HSMul.hSMul (β := V →ₗ[R] V) a 1
inr₁ : ∀ (hι : Nontrivial ι), ∃ (a : ↥(Subring.center R)), f = HSMul.hSMul (β := V →ₗ[R] V) a 1
⊢ ∃ (a : ↥(Subring.center R)), f = HSMul.hSMul (β := V →ₗ[R] V) a 1

Tactic:
rcases subsingleton_or_nontrivial ι with hι | hι

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : StrongRankCondition R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Free R V
f : V →ₗ[R] V
hV1 : finrank R V ≠ 1
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
hV : Nontrivial V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V := Free.chooseBasis R V
hι : Subsingleton ι
⊢ Nonempty ι

Tactic:
have : Nonempty ι := Free.instNonemptyChooseBasisIndexOfNontrivial R V
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : StrongRankCondition R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Free R V
f : V →ₗ[R] V
hV1 : finrank R V ≠ 1
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
hV : Nontrivial V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V := Free.chooseBasis R V
hι : Subsingleton ι
this : Nonempty ι
inr : ∀ (this : Fintype ι), ∃ (a : ↥(Subring.center R)), f = HSMul.hSMul (β := V →ₗ[R] V) a 1
⊢ ∃ (a : ↥(Subring.center R)), f = HSMul.hSMul (β := V →ₗ[R] V) a 1

Tactic:
have : Fintype ι := Fintype.ofFinite ι
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : StrongRankCondition R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Free R V
f : V →ₗ[R] V
hV1 : finrank R V ≠ 1
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
hV : Nontrivial V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V := Free.chooseBasis R V
hι : Subsingleton ι
this_1 : Nonempty ι
this : Fintype ι
⊢ ∃ (a : ↥(Subring.center R)), f = HSMul.hSMul (β := V →ₗ[R] V) a 1

Tactic:
simp_all [finrank_eq_card_basis b, ← Nat.card_eq_fintype_card]

Premises used: Module.finrank_eq_card_basis, Nat.card_eq_fintype_card
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : StrongRankCondition R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Free R V
f : V →ₗ[R] V
hV1 : finrank R V ≠ 1
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
hV : Nontrivial V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V := Free.chooseBasis R V
hι : Nontrivial ι
⊢ ∃ (a : ↥(Subring.center R)), f = HSMul.hSMul (β := V →ₗ[R] V) a 1

Tactic:
exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis b h

Premises used: LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis
-- Module: Mathlib.LinearAlgebra.Center
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : IsDomain R
inst_2 : StrongRankCondition R
inst_3 : AddCommGroup V
inst_4 : Module R V
inst_5 : Free R V
f : V →ₗ[R] V
hV1 : finrank R V ≠ 1
h : ∀ (v : V), ¬LinearIndependent (ι := Fin (Nat.succ 0).succ) R ![v, (f : (a : V) → V) v]
hV : Nontrivial V
ι : Type u_2 := Free.ChooseBasisIndex R V
b : Basis ι R V := Free.chooseBasis R V
hι : Nontrivial ι
⊢ ∃ (a : ↥(Subring.center R)), f = HSMul.hSMul (β := V →ₗ[R] V) a 1

Tactic:
exact exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis b h

Premises used: LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis
-- Module: Mathlib.LinearAlgebra.Center
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]
pos : ∀ (hV1 : finrank R V = 1), ∃ (a : R), f = HSMul.hSMul (β := V →ₗ[R] V) a 1
neg : ∀ (hV1 : ¬finrank R V = 1), ∃ (a : R), f = HSMul.hSMul (β := V →ₗ[R] V) a 1
⊢ ∃ (a : R), f = HSMul.hSMul (β := V →ₗ[R] V) a 1

Tactic:
by_cases hV1 : finrank R V = 1

Premises used: Module.finrank
-- Module: Mathlib.LinearAlgebra.Center
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
⊢ Nonempty (Basis Unit R V)

Tactic:
rw [finrank_eq_one_iff Unit] at hV1

Premises used: finrank_eq_one_iff, Unit
-- Module: Mathlib.LinearAlgebra.Center
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
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
⊢ ∃ (a : R), f = HSMul.hSMul (β := V →ₗ[R] V) a 1

Tactic:
use b.coord () (f (b ()))

Premises used: Unit.unit, Module.Basis.coord, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Center
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
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)
⊢ 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:
apply b.ext

Premises used: Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Center
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
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)
⊢ 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:
nth_rewrite 1 [← b.linearCombination_repr (f (b i))]

Premises used: Module.Basis.linearCombination_repr, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Center
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.{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:
simp [linearCombination_unique]

Premises used: Finsupp.linearCombination_unique
-- Module: Mathlib.LinearAlgebra.Center
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
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
⊢ ∃ (a : R), f = HSMul.hSMul (β := V →ₗ[R] V) a 1

Tactic:
obtain ⟨a, rfl⟩ := exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent hV1 h

Premises used: LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent, rfl
-- Module: Mathlib.LinearAlgebra.Center
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
hV1 : ¬finrank R V = 1
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]
⊢ HSMul.hSMul (β := V →ₗ[R] V) a 1 = HSMul.hSMul (β := V →ₗ[R] V) (↑a : R) 1

Tactic:
simp [Subring.smul_def]

Premises used: Subring.smul_def
-- Module: Mathlib.LinearAlgebra.Center
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
hV1 : ¬finrank R V = 1
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:
refine ⟨a, by simp [Subring.smul_def]⟩
-- Module: Mathlib.LinearAlgebra.Charpoly.BaseChange
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
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.LinearAlgebra.Charpoly.BaseChange
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
⊢ Nontrivial R

Tactic:
have := (algebraMap R A).domain_nontrivial
-- Module: Mathlib.LinearAlgebra.Charpoly.BaseChange
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
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)))
⊢ Eq (α := Polynomial A) (charpoly (M := TensorProduct R A M) (baseChange A f))
    (Polynomial.map (algebraMap R A) f.charpoly)

Tactic:
rw [← f.charpoly_toMatrix b, ← (f.baseChange A).charpoly_toMatrix (b.baseChange A),
    ← Matrix.charpoly_map]

Premises used: LinearMap.baseChange, Matrix.charpoly_map, Module.Basis.baseChange, LinearMap.charpoly_toMatrix
-- Module: Mathlib.LinearAlgebra.Charpoly.BaseChange
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
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)
⊢ 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:
congr 1
-- Module: Mathlib.LinearAlgebra.Charpoly.BaseChange
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
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)
⊢ 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:
ext i j
-- Module: Mathlib.LinearAlgebra.Charpoly.BaseChange
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
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:
simp [LinearMap.toMatrix_apply, ← Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one, LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Charpoly.BaseChange
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
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.LinearAlgebra.Charpoly.BaseChange
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
rw₃ 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
⊢ (LinearMap.det : (a : M →ₗ[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]

Premises used: LinearMap.charpoly_def, Module.finrank_eq_card_chooseBasisIndex, LinearMap.det_toMatrix, Matrix.det_eq_sign_charpoly_coeff, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.Charpoly.BaseChange
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
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)
⊢ 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)

Tactic:
rw [LinearMap.det_eq_sign_charpoly_coeff, LinearMap.det_eq_sign_charpoly_coeff]

Premises used: LinearMap.det_eq_sign_charpoly_coeff
-- Module: Mathlib.LinearAlgebra.Charpoly.BaseChange
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
⊢ 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:
simp
-- Module: Mathlib.LinearAlgebra.Charpoly.BaseChange
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
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)
⊢ 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