awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] R
x : M
⊢ Eq.{u_1 + 1} (α := R)
    (Matrix.trace.{u_2, u_1} (n := Free.ChooseBasisIndex R M)
        ((toMatrix (Free.chooseBasis R M) (Free.chooseBasis R M) :
            (a : M →ₗ[R] M) → Matrix (Free.ChooseBasisIndex R M) (Free.ChooseBasisIndex R M) R)
          (f.smulRight
            (∑ i : Free.ChooseBasisIndex R M,
              HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
                ((((Basis.repr (Free.chooseBasis R M) : (a : M) → Free.ChooseBasisIndex R M →₀ R) x :
                        Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
                      (a : Free.ChooseBasisIndex R M) → R)
                    i :
                  R)
                ((Free.chooseBasis R M : (a : Free.ChooseBasisIndex R M) → M) i : M)))) :
      R)
    ((f : (a : M) → R)
        (∑ i : Free.ChooseBasisIndex R M,
          HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := M)
            ((((Basis.repr (Free.chooseBasis R M) : (a : M) → Free.ChooseBasisIndex R M →₀ R) x :
                    Finsupp.{u_2, u_1} (Free.ChooseBasisIndex R M) R) :
                  (a : Free.ChooseBasisIndex R M) → R)
                i :
              R)
            ((Free.chooseBasis R M : (a : Free.ChooseBasisIndex R M) → M) i : M)) :
      R)

Tactic:
simp [-Basis.sum_repr, dotProduct]

Premises used: dotProduct, Module.Basis.sum_repr
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : Free R N
inst_8 : Module.Finite R N
inst_9 : Free R P
inst_10 : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
rw :
  Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((f ∘ₗ h) ∘ₗ g) : R)
    ((trace R N : (a : N →ₗ[R] N) → R) (f ∘ₗ h ∘ₗ g) : R)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) (f ∘ₗ h ∘ₗ g) : R)
    ((trace R N : (a : N →ₗ[R] N) → R) (f ∘ₗ h ∘ₗ g) : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R P : (a : P →ₗ[R] P) → R) (g ∘ₗ f ∘ₗ h) : R)
    ((trace R N : (a : N →ₗ[R] N) → R) (f ∘ₗ h ∘ₗ g) : R)

Tactic:
rw [trace_comp_comm', comp_assoc]

Premises used: LinearMap.comp_assoc, LinearMap.trace_comp_comm'
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
P : Type u_4
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : Free R M
inst_8 : Module.Finite R M
inst_9 : Free R P
inst_10 : Module.Finite R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : P →ₗ[R] M
rw :
  Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (h ∘ₗ g ∘ₗ f) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) ((h ∘ₗ g) ∘ₗ f) : R)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) ((h ∘ₗ g) ∘ₗ f) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) ((h ∘ₗ g) ∘ₗ f) : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R P : (a : P →ₗ[R] P) → R) ((g ∘ₗ f) ∘ₗ h) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) ((h ∘ₗ g) ∘ₗ f) : R)

Tactic:
rw [trace_comp_comm', ← comp_assoc]

Premises used: LinearMap.comp_assoc, LinearMap.trace_comp_comm'
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
pos :
  ∀ (hM : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)),
    Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) f : R)
neg :
  ∀ (hM : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)),
    Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) f : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)

Tactic:
by_cases hM : ∃ s : Finset M, Nonempty (Basis s R M)

Premises used: Finset
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)
pos :
  ∀ (s : Finset M) (b : Basis (↥s) R M),
    Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) f : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)

Tactic:
obtain ⟨s, ⟨b⟩⟩ := hM
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
⊢ Module.Finite R M

Tactic:
haveI := Module.Finite.of_basis b
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this : Module.Finite R M
⊢ Free R M

Tactic:
haveI := (Module.free_def R M).mpr ⟨_, ⟨b⟩⟩
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this_1 : Module.Finite R M
this : Free R M
⊢ Module.Finite R N

Tactic:
haveI := Module.Finite.of_basis (b.map e)
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this_1 : Module.Finite R M
this_2 : Free R M
this : Module.Finite R N
⊢ Free R N

Tactic:
haveI := (Module.free_def R N).mpr ⟨_, ⟨(b.map e).reindex (e.toEquiv.image _)⟩⟩
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
s : Finset M
b : Basis (↥s) R M
this_1 : Module.Finite R M
this_2 : Free R M
this_3 : Module.Finite R N
this : Free R N
pos :
  Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) (((↑e : M →ₗ[R] N) ∘ₗ f) ∘ₗ (↑e.symm : N →ₗ[R] M)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
pos₁ :
  Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) ((↑e.symm : N →ₗ[R] M) ∘ₗ (↑e : M →ₗ[R] N) ∘ₗ f) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
pos₂ :
  Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (((↑e.symm : N →ₗ[R] M) ∘ₗ (↑e : M →ₗ[R] N)) ∘ₗ f) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
pos₃ :
  Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) ((↑(e ≪≫ₗ e.symm) : M →ₗ[R] M) ∘ₗ f) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
pos₄ :
  Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) ((↑(LinearEquiv.refl R M) : M →ₗ[R] M) ∘ₗ f) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
pos₅ : Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (id ∘ₗ f) : R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
pos₆ pos₇ : Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)

Tactic:
rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe,
      LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, id_comp]

Premises used: LinearMap.comp_assoc, LinearEquiv.refl_toLinearMap, LinearEquiv.conj_apply, LinearEquiv.comp_coe, LinearMap.id_comp, LinearMap.trace_comp_comm', LinearEquiv.self_trans_symm
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)
rw : ¬∃ (s : Finset N), Nonempty (Basis (↥s) R N)
⊢ Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)

Tactic:
rw [trace, trace, dif_neg hM, dif_neg ?_, zero_apply, zero_apply]

Premises used: LinearMap.trace, LinearMap.zero_apply, dif_neg
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)
s : Finset N
b : Basis (↥s) R N
⊢ False

Tactic:
hM ⟨s.image e.symm, ⟨(b.map e.symm).reindex
      ((e.symm.toEquiv.image s).trans (Equiv.setCongr Finset.coe_image.symm))⟩⟩

Premises used: LinearEquiv.symm, Equiv.trans, Module.Basis.map, Equiv.setCongr, Finset.coe_image, Nonempty.intro, SetLike.coe, Equiv.image, LinearEquiv.toEquiv, Exists.intro, Module.Basis.reindex, Eq.symm, DFunLike.coe, Finset.image
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
hM : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)
s : Finset N
b : Basis (↥s) R N
⊢ False

Tactic:
exact hM ⟨s.image e.symm, ⟨(b.map e.symm).reindex
      ((e.symm.toEquiv.image s).trans (Equiv.setCongr Finset.coe_image.symm))⟩⟩

Premises used: LinearEquiv.symm, Equiv.trans, Module.Basis.map, Equiv.setCongr, Finset.coe_image, Nonempty.intro, SetLike.coe, Equiv.image, LinearEquiv.toEquiv, Exists.intro, Module.Basis.reindex, Eq.symm, DFunLike.coe, Finset.image
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
pos :
  ∀ (hM : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)),
    Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) f : R)
neg neg₁ :
  ∀ (hM : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)),
    Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) f : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R N : (a : N →ₗ[R] N) → R) ((e.conj : (a : End R M) → End R N) f : End R N) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)

Tactic:
classical
  by_cases hM : ∃ s : Finset M, Nonempty (Basis s R M)
  · obtain ⟨s, ⟨b⟩⟩ := hM
    haveI := Module.Finite.of_basis b
    haveI := (Module.free_def R M).mpr ⟨_, ⟨b⟩⟩
    haveI := Module.Finite.of_basis (b.map e)
    haveI := (Module.free_def R N).mpr ⟨_, ⟨(b.map e).reindex (e.toEquiv.image _)⟩⟩
    rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe,
      LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, id_comp]
  · rw [trace, trace, dif_neg hM, dif_neg ?_, zero_apply, zero_apply]
    rintro ⟨s, ⟨b⟩⟩
    exact hM ⟨s.image e.symm, ⟨(b.map e.symm).reindex
      ((e.symm.toEquiv.image s).trans (Equiv.setCongr Finset.coe_image.symm))⟩⟩

Premises used: LinearMap.trace, LinearMap.zero_apply, Finset, LinearMap.comp_assoc, LinearEquiv.refl_toLinearMap, LinearEquiv.conj_apply, dif_neg, LinearEquiv.comp_coe, LinearMap.id_comp, LinearMap.trace_comp_comm', LinearEquiv.self_trans_symm
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
K : Type u_6
V : Type u_7
W : Type u_8
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup W
inst_4 : Module K W
F : Type u_9
inst_5 : EquivLike.{u_9 + 1, u_7 + 1, u_8 + 1} F (End K V) (End K W)
inst_6 : AlgEquivClass F K (End K V) (End K W)
f : F
x : End K V
w : V ≃ₗ[K] W
h : Eq (α := AlgEquiv.{u_6, u_7, u_8} K (End K V) (End K W)) (↑f : End K V ≃ₐ[K] End K W) (LinearEquiv.conjAlgEquiv K w)
⊢ Eq.{u_8 + 1} (α := End K W) ((f : (a : End K V) → End K W) x : End K W)
    (((LinearEquiv.conjAlgEquiv K w : AlgEquiv.{u_6, u_7, u_8} K (End K V) (End K W)) : (a : End K V) → End K W) x :
      End K W)

Tactic:
simpa using congr($h x)
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
K : Type u_6
m : Type u_7
n : Type u_8
inst : Field K
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
inst_4 : DecidableEq n
F : Type u_9
inst_5 : EquivLike F (Matrix m m K) (Matrix n n K)
inst_6 : AlgEquivClass F K (Matrix m m K) (Matrix n n K)
f : F
x : Matrix m m K
⊢ Matrix.trace.{u_8, u_6} (n := n) ((f : (a : Matrix m m K) → Matrix n n K) x) = x.trace

Tactic:
simpa [toMatrixAlgEquiv', Matrix.toLinAlgEquiv'] using
    LinearMap.trace_map ((Matrix.toLinAlgEquiv'.symm.trans
      (AlgEquivClass.toAlgEquiv f)).trans Matrix.toLinAlgEquiv') x.toLin'

Premises used: AlgEquiv.symm, Matrix.toLin', LinearMap.toMatrixAlgEquiv', AlgEquivClass.toAlgEquiv, AlgEquiv.trans, Matrix.toLinAlgEquiv', DFunLike.coe, LinearMap.trace_map
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
f : M →ₗ[R] M
h : IsProj p f
inst_3 : Free.{u_1, u_2} R ↥p
inst_4 : Module.Finite.{u_1, u_2} R ↥p
inst_5 : Free.{u_1, u_2} R ↥f.ker
inst_6 : Module.Finite.{u_1, u_2} R ↥f.ker
rw :
  Eq.{u_1 + 1} (α := R)
    ((LinearMap.trace R M : (a : M →ₗ[R] M) → R)
        (((LinearEquiv.conj.{u_1, u_1, u_2, u_2} (R₁' := R) (R₂' := R) (M₁' := ↥p × ↥f.ker) (M₂' := M) (σ₁'₂' :=
                  RingHom.id R) (σ₂'₁' := RingHom.id R) (p.prodEquivOfIsCompl f.ker ⋯) :
                End R (↥p × ↥f.ker) ≃ₗ[R] End R M) :
              (a : End R (↥p × ↥f.ker)) → End R M)
            (prodMap id 0) :
          End R M) :
      R)
    ((↑(finrank.{u_1, u_2} R ↥p) : R) : R)
rw₁ :
  Eq.{u_1 + 1} (α := R) ((LinearMap.trace R (↥p × ↥f.ker) : (a : ↥p × ↥f.ker →ₗ[R] ↥p × ↥f.ker) → R) (prodMap id 0) : R)
    ((↑(finrank.{u_1, u_2} R ↥p) : R) : R)
rw₂ :
  HAdd.hAdd (α := R) (β := R) ((LinearMap.trace R ↥p : (a : ↥p →ₗ[R] ↥p) → R) id : R)
      ((LinearMap.trace R ↥f.ker : (a : ↥f.ker →ₗ[R] ↥f.ker) → R) 0 : R) =
    (↑(finrank.{u_1, u_2} R ↥p) : R)
rw₃ :
  HAdd.hAdd (α := R) (β := R) ((↑(finrank.{u_1, u_2} R ↥p) : R) : R)
      ((LinearMap.trace R ↥f.ker : (a : ↥f.ker →ₗ[R] ↥f.ker) → R) 0 : R) =
    (↑(finrank.{u_1, u_2} R ↥p) : R)
rw₄ : HAdd.hAdd (α := R) (↑(finrank.{u_1, u_2} R ↥p) : R) 0 = (↑(finrank.{u_1, u_2} R ↥p) : R)
rw₅ rw₆ : Eq.{u_1 + 1} (α := R) (↑(finrank.{u_1, u_2} R ↥p) : R) (↑(finrank.{u_1, u_2} R ↥p) : R)
⊢ Eq.{u_1 + 1} (α := R) ((LinearMap.trace R M : (a : M →ₗ[R] M) → R) f : R) ((↑(finrank.{u_1, u_2} R ↥p) : R) : R)

Tactic:
rw [h.eq_conj_prodMap, trace_conj', trace_prodMap', trace_id, map_zero, add_zero]

Premises used: LinearMap.IsProj.eq_conj_prodMap, map_zero, LinearMap.trace_id, LinearMap.trace_conj', LinearMap.trace_prodMap', add_zero
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
pos :
  ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)),
    IsNilpotent.{u_1} (R := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
neg :
  ∀ (H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)),
    IsNilpotent.{u_1} (R := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
⊢ IsNilpotent.{u_1} (R := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)

Tactic:
by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)

Premises used: Finset
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)
neg : IsNilpotent.{u_1} (R := R) ((0 : (a : M →ₗ[R] M) → R) f : R)
⊢ IsNilpotent.{u_1} (R := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)

Tactic:
rw [LinearMap.trace, dif_neg H]

Premises used: LinearMap.trace, dif_neg
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)
⊢ IsNilpotent.{u_1} (R := R) ((0 : (a : M →ₗ[R] M) → R) f : R)

Tactic:
IsNilpotent.zero

Premises used: IsNilpotent.zero
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)
⊢ IsNilpotent.{u_1} (R := R) ((0 : (a : M →ₗ[R] M) → R) f : R)

Tactic:
exact IsNilpotent.zero

Premises used: IsNilpotent.zero
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)
pos : ∀ (s : Finset M) (b : Basis (↥s) R M), IsNilpotent.{u_1} (R := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
⊢ IsNilpotent.{u_1} (R := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)

Tactic:
obtain ⟨s, ⟨b⟩⟩ := H
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
s : Finset M
b : Basis (↥s) R M
pos :
  IsNilpotent.{u_1} (R := R)
    (Matrix.trace.{u_2, u_1} (n := ↥s) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (↥s) (↥s) R) f))
⊢ IsNilpotent.{u_1} (R := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)

Tactic:
rw [trace_eq_matrix_trace R b]

Premises used: LinearMap.trace_eq_matrix_trace
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
s : Finset M
b : Basis (↥s) R M
pos :
  IsNilpotent (R := Matrix.{u_2, u_2, u_1} (↥s) (↥s) R)
    ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (↥s) (↥s) R) f : Matrix.{u_2, u_2, u_1} (↥s) (↥s) R)
⊢ IsNilpotent.{u_1} (R := R)
    (Matrix.trace.{u_2, u_1} (n := ↥s) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (↥s) (↥s) R) f))

Tactic:
apply Matrix.isNilpotent_trace_of_isNilpotent

Premises used: Matrix.isNilpotent_trace_of_isNilpotent
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
s : Finset M
b : Basis (↥s) R M
⊢ IsNilpotent (R := Matrix.{u_2, u_2, u_1} (↥s) (↥s) R)
    ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (↥s) (↥s) R) f : Matrix.{u_2, u_2, u_1} (↥s) (↥s) R)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
s : Finset M
b : Basis (↥s) R M
pos pos₁ pos₂ :
  IsNilpotent.{u_1} (R := R)
    (Matrix.trace.{u_2, u_1} (n := ↥s) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (↥s) (↥s) R) f))
pos₃ :
  IsNilpotent (R := Matrix.{u_2, u_2, u_1} (↥s) (↥s) R)
    ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (↥s) (↥s) R) f : Matrix.{u_2, u_2, u_1} (↥s) (↥s) R)
⊢ IsNilpotent.{u_1} (R := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)

Tactic:
classical
  rw [trace_eq_matrix_trace R b]
  apply Matrix.isNilpotent_trace_of_isNilpotent
  simpa

Premises used: Matrix.isNilpotent_trace_of_isNilpotent
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
hg : IsNilpotent (HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M))
⊢ let n := HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M);
  IsNilpotent n

Tactic:
set n := g - algebraMap R _ μ

Premises used: Algebra.algebraMap, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)
hg : IsNilpotent n
rw : IsNilpotent.{u_1} (R := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * n) : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ n) : R) (0 : R)

Tactic:
rw [← isNilpotent_iff_eq_zero, ← Module.End.mul_eq_comp]

Premises used: Module.End.mul_eq_comp, isNilpotent_iff_eq_zero
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)
hg : IsNilpotent n
⊢ IsNilpotent.{u_1} (R := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * n) : R)

Tactic:
isNilpotent_trace_of_isNilpotent (Commute.isNilpotent_mul_left ?_ hg)

Premises used: Commute.isNilpotent_mul_left, LinearMap.isNilpotent_trace_of_isNilpotent
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)
hg : IsNilpotent n
refine : Commute f n
⊢ IsNilpotent.{u_1} (R := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * n) : R)

Tactic:
refine isNilpotent_trace_of_isNilpotent (Commute.isNilpotent_mul_left ?_ hg)

Premises used: Commute.isNilpotent_mul_left, LinearMap.isNilpotent_trace_of_isNilpotent
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)
hg : IsNilpotent n
⊢ Commute f n

Tactic:
h_comm.sub_right (Algebra.commute_algebraMap_right μ f)

Premises used: Commute.sub_right, Algebra.commute_algebraMap_right
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)
hg : IsNilpotent n
⊢ Commute f n

Tactic:
exact h_comm.sub_right (Algebra.commute_algebraMap_right μ f)

Premises used: Commute.sub_right, Algebra.commute_algebraMap_right
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)
hg : IsNilpotent n
⊢ Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ n) : R) (0 : R)

Tactic:
replace hg : trace R M (f ∘ₗ n) = 0 := by
    rw [← isNilpotent_iff_eq_zero, ← Module.End.mul_eq_comp]
    refine isNilpotent_trace_of_isNilpotent (Commute.isNilpotent_mul_left ?_ hg)
    exact h_comm.sub_right (Algebra.commute_algebraMap_right μ f)
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)
hg : Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ n) : R) (0 : R)
⊢ g = HAdd.hAdd (α := End R M) ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M) n

Tactic:
have hμ : g = algebraMap R _ μ + n := eq_add_of_sub_eq' rfl