awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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)
⊢ 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)
have 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)
Tactic: rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe,
      LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, id_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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)
⊢ 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)
have 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)
Tactic: rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe,
      LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, id_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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)
⊢ 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)
have 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)
Tactic: rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe,
      LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, id_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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)
⊢ 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)
have rw : ¬∃ (s : Finset N), Nonempty (Basis (↥s) R N)
Tactic: rw [trace, trace, dif_neg hM, dif_neg ?_, zero_apply, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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
⊢ 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)
have 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)
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))⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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)
⊢ 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)
have 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)
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))⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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
⊢ 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)
have 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 sorry) :
              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)
Tactic: rw [h.eq_conj_prodMap, trace_conj', trace_prodMap', trace_id, map_zero, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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)
⊢ 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)
have 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)
Tactic: rw [h.eq_conj_prodMap, trace_conj', trace_prodMap', trace_id, map_zero, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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)
⊢ 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)
have 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)
Tactic: rw [h.eq_conj_prodMap, trace_conj', trace_prodMap', trace_id, map_zero, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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)
⊢ 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)
have 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)
Tactic: rw [h.eq_conj_prodMap, trace_conj', trace_prodMap', trace_id, map_zero, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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)
⊢ 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)
have rw₄ : HAdd.hAdd (α := R) (↑(finrank.{u_1, u_2} R ↥p) : R) 0 = (↑(finrank.{u_1, u_2} R ↥p) : R)
Tactic: rw [h.eq_conj_prodMap, trace_conj', trace_prodMap', trace_id, map_zero, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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)
⊢ 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)
have rw₅ : Eq.{u_1 + 1} (α := R) (↑(finrank.{u_1, u_2} R ↥p) : R) (↑(finrank.{u_1, u_2} R ↥p) : R)
Tactic: rw [h.eq_conj_prodMap, trace_conj', trace_prodMap', trace_id, map_zero, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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
⊢ IsNilpotent.{u_1} (R := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have 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)
Tactic: by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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)
⊢ IsNilpotent.{u_1} (R := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have 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)
Tactic: by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have neg : IsNilpotent.{u_1} (R := R) ((0 : (a : M →ₗ[R] M) → R) f : R)
Tactic: rw [LinearMap.trace, dif_neg H]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have pos : ∀ (s : Finset M) (b : Basis (↥s) R M), IsNilpotent.{u_1} (R := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
Tactic: obtain ⟨s, ⟨b⟩⟩ := H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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.{u_1} (R := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have 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))
Tactic: rw [trace_eq_matrix_trace R b]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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.{u_1} (R := R)
    (Matrix.trace.{u_2, u_1} (n := ↥s) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (↥s) (↥s) R) f))
have 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)
Tactic: apply Matrix.isNilpotent_trace_of_isNilpotent
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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.{u_1} (R := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have 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))
Tactic: classical
  rw [trace_eq_matrix_trace R b]
  apply Matrix.isNilpotent_trace_of_isNilpotent
  simpa
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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))
⊢ IsNilpotent.{u_1} (R := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have 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)
Tactic: classical
  rw [trace_eq_matrix_trace R b]
  apply Matrix.isNilpotent_trace_of_isNilpotent
  simpa
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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)
have rw : IsNilpotent.{u_1} (R := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * n) : R)
Tactic: rw [← isNilpotent_iff_eq_zero, ← Module.End.mul_eq_comp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (goal)
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)
have refine : Commute f n
Tactic: refine isNilpotent_trace_of_isNilpotent (Commute.isNilpotent_mul_left ?_ hg)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (hypothesis)
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
⊢ (trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ g) = HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have hg₁ : 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)
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Trace (hypothesis)
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)
⊢ (trace R M : (a : M →ₗ[R] M) → R) (f ∘ₗ g) = HMul.hMul (β := R) μ ((trace R M : (a : M →ₗ[R] M) → R) f : R)
have hμ : 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