awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : DecidableEq ι
inst_4 : Fintype ι
κ : Type u_1
inst_5 : DecidableEq κ
inst_6 : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
rw :
  (HMul.hMul (α := Matrix ι κ R) ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) id : Matrix ι κ R)
        (HMul.hMul (α := Matrix κ κ R) (β := Matrix κ ι R)
          ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) f : Matrix κ κ R)
          ((toMatrix b c : (a : M →ₗ[R] M) → Matrix κ ι R) id : Matrix κ ι R))).trace =
    (HMul.hMul (β := Matrix ι κ R)
        (HMul.hMul (α := Matrix κ κ R) (β := Matrix κ ι R)
          ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) f : Matrix κ κ R)
          ((toMatrix b c : (a : M →ₗ[R] M) → Matrix κ ι R) id : Matrix κ ι R))
        ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) id : Matrix ι κ R)).trace
rw₁ rw₂ :
  (HMul.hMul (β := Matrix ι κ R)
        (HMul.hMul (α := Matrix κ κ R) (β := Matrix κ ι R)
          ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) f : Matrix κ κ R)
          ((toMatrix b c : (a : M →ₗ[R] M) → Matrix κ ι R) id : Matrix κ ι R))
        ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) id : Matrix ι κ R)).trace =
    (HMul.hMul (β := Matrix ι κ R)
        (HMul.hMul (α := Matrix κ κ R) (β := Matrix κ ι R)
          ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) f : Matrix κ κ R)
          ((toMatrix b c : (a : M →ₗ[R] M) → Matrix κ ι R) id : Matrix κ ι R))
        ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) id : Matrix ι κ R)).trace
⊢ (HMul.hMul (β := Matrix κ ι R)
        (HMul.hMul (α := Matrix ι κ R) (β := Matrix κ κ R)
          ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) id : Matrix ι κ R)
          ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) f : Matrix κ κ R))
        ((toMatrix b c : (a : M →ₗ[R] M) → Matrix κ ι R) id : Matrix κ ι R)).trace =
    (HMul.hMul (β := Matrix ι κ R)
        (HMul.hMul (α := Matrix κ κ R) (β := Matrix κ ι R)
          ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) f : Matrix κ κ R)
          ((toMatrix b c : (a : M →ₗ[R] M) → Matrix κ ι R) id : Matrix κ ι R))
        ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) id : Matrix ι κ R)).trace

Tactic:
rw [Matrix.mul_assoc, Matrix.trace_mul_comm]

Premises used: Matrix.trace_mul_comm, Matrix.mul_assoc
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : DecidableEq ι
inst_4 : Fintype ι
κ : Type u_1
inst_5 : DecidableEq κ
inst_6 : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
rw :
  (HMul.hMul (β := Matrix ι κ R)
        (HMul.hMul (α := Matrix κ κ R) (β := Matrix κ ι R)
          ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) f : Matrix κ κ R)
          ((toMatrix b c : (a : M →ₗ[R] M) → Matrix κ ι R) id : Matrix κ ι R))
        ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) id : Matrix ι κ R)).trace =
    (HMul.hMul (α := Matrix κ ι R) (β := Matrix ι κ R)
        ((toMatrix b c : (a : M →ₗ[R] M) → Matrix κ ι R) (f ∘ₗ id) : Matrix κ ι R)
        ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) id : Matrix ι κ R)).trace
rw₁ rw₂ :
  (HMul.hMul (β := Matrix ι κ R)
        (HMul.hMul (α := Matrix κ κ R) (β := Matrix κ ι R)
          ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) f : Matrix κ κ R)
          ((toMatrix b c : (a : M →ₗ[R] M) → Matrix κ ι R) id : Matrix κ ι R))
        ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) id : Matrix ι κ R)).trace =
    (HMul.hMul (β := Matrix ι κ R)
        (HMul.hMul (α := Matrix κ κ R) (β := Matrix κ ι R)
          ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) f : Matrix κ κ R)
          ((toMatrix b c : (a : M →ₗ[R] M) → Matrix κ ι R) id : Matrix κ ι R))
        ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) id : Matrix ι κ R)).trace
⊢ (HMul.hMul (β := Matrix ι κ R)
        (HMul.hMul (α := Matrix κ κ R) (β := Matrix κ ι R)
          ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) f : Matrix κ κ R)
          ((toMatrix b c : (a : M →ₗ[R] M) → Matrix κ ι R) id : Matrix κ ι R))
        ((toMatrix c b : (a : M →ₗ[R] M) → Matrix ι κ R) id : Matrix ι κ R)).trace =
    Matrix.trace.{u_1, u} (n := κ) ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) ((f ∘ₗ id) ∘ₗ id))

Tactic:
rw [LinearMap.toMatrix_comp _ b, LinearMap.toMatrix_comp _ c]

Premises used: LinearMap.toMatrix_comp
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : DecidableEq ι
inst_4 : Fintype ι
κ : Type u_1
inst_5 : DecidableEq κ
inst_6 : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
rw :
  Eq.{u + 1} (α := R) (Matrix.trace.{u_1, u} (n := κ) ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) (f ∘ₗ id)))
    (Matrix.trace.{u_1, u} (n := κ) ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) f))
rw₁ rw₂ :
  Eq.{u + 1} (α := R) (Matrix.trace.{u_1, u} (n := κ) ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) f))
    (Matrix.trace.{u_1, u} (n := κ) ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) f))
⊢ Eq.{u + 1} (α := R)
    (Matrix.trace.{u_1, u} (n := κ) ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) ((f ∘ₗ id) ∘ₗ id)))
    (Matrix.trace.{u_1, u} (n := κ) ((toMatrix c c : (a : M →ₗ[R] M) → Matrix κ κ R) f))

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

Premises used: LinearMap.comp_id
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset M
b : Basis (↥s) R M
f : M →ₗ[R] M
⊢ ∃ (s : Finset M), Nonempty (Basis (↥s) R M)

Tactic:
have : ∃ s : Finset M, Nonempty (Basis s R M) := ⟨s, ⟨b⟩⟩
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset M
b : Basis (↥s) R M
f : M →ₗ[R] M
this : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)
rw : Eq.{u + 1} (α := R) ((traceAux R ⋯.some : (a : M →ₗ[R] M) → R) f : R) ((traceAux R b : (a : M →ₗ[R] M) → R) f : R)
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
    (Matrix.trace.{v, u} (n := ↥s) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (↥s) (↥s) R) f) : R)

Tactic:
rw [trace, dif_pos this, ← traceAux_def]

Premises used: LinearMap.trace, dif_pos, LinearMap.traceAux_def
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset M
b : Basis (↥s) R M
f : M →ₗ[R] M
this : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)
e_a : traceAux R ⋯.some = traceAux R b
⊢ Eq.{u + 1} (α := R) ((traceAux R ⋯.some : (a : M →ₗ[R] M) → R) f : R) ((traceAux R b : (a : M →ₗ[R] M) → R) f : R)

Tactic:
congr 1
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : DecidableEq ι
inst_4 : Fintype ι
b : Basis ι R M
f : M →ₗ[R] M
rw :
  Eq.{u + 1} (α := R)
    (Matrix.trace.{v, u} (n := ↥(Finset.image.{w, v} (α := ι) (⇑b : (a : ι) → M) Finset.univ))
      ((toMatrix b.reindexFinsetRange b.reindexFinsetRange :
          (a : M →ₗ[R] M) →
            Matrix (↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) (↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) R)
        f))
    (Matrix.trace.{w, u} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f))
rw₁ :
  Eq.{u + 1} (α := R)
    ((traceAux R (ι := ↥(Finset.image.{w, v} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) b.reindexFinsetRange :
          (a : M →ₗ[R] M) → R)
        f :
      R)
    (Matrix.trace.{w, u} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f) : R)
rw₂ :
  Eq.{u + 1} (α := R)
    ((traceAux R (ι := ↥(Finset.image.{w, v} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) b.reindexFinsetRange :
          (a : M →ₗ[R] M) → R)
        f :
      R)
    ((traceAux R b : (a : M →ₗ[R] M) → R) f : R)
rw₃ rw₄ :
  Eq.{u + 1} (α := R)
    ((traceAux R (ι := ↥(Finset.image.{w, v} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) b.reindexFinsetRange :
          (a : M →ₗ[R] M) → R)
        f :
      R)
    ((traceAux R (ι := ↥(Finset.image.{w, v} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) b.reindexFinsetRange :
          (a : M →ₗ[R] M) → R)
        f :
      R)
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
    (Matrix.trace.{w, u} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f) : R)

Tactic:
rw [trace_eq_matrix_trace_of_finset R b.reindexFinsetRange, ← traceAux_def, ← traceAux_def,
    traceAux_eq R b b.reindexFinsetRange]

Premises used: Module.Basis.reindexFinsetRange, LinearMap.trace_eq_matrix_trace_of_finset, LinearMap.traceAux_def, LinearMap.traceAux_eq
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : DecidableEq ι
inst_4 : Fintype ι
b : Basis ι R M
f : M →ₗ[R] M
rw :
  Eq.{u + 1} (α := R)
    (Matrix.trace.{v, u} (n := ↥(Finset.image.{w, v} (α := ι) (⇑b : (a : ι) → M) Finset.univ))
      ((toMatrix b.reindexFinsetRange b.reindexFinsetRange :
          (a : M →ₗ[R] M) →
            Matrix (↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) (↥(Finset.image (⇑b : (a : ι) → M) Finset.univ)) R)
        f))
    (Matrix.trace.{w, u} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f))
rw₁ :
  Eq.{u + 1} (α := R)
    ((traceAux R (ι := ↥(Finset.image.{w, v} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) b.reindexFinsetRange :
          (a : M →ₗ[R] M) → R)
        f :
      R)
    (Matrix.trace.{w, u} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f) : R)
rw₂ :
  Eq.{u + 1} (α := R)
    ((traceAux R (ι := ↥(Finset.image.{w, v} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) b.reindexFinsetRange :
          (a : M →ₗ[R] M) → R)
        f :
      R)
    ((traceAux R b : (a : M →ₗ[R] M) → R) f : R)
rw₃ rw₄ :
  Eq.{u + 1} (α := R)
    ((traceAux R (ι := ↥(Finset.image.{w, v} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) b.reindexFinsetRange :
          (a : M →ₗ[R] M) → R)
        f :
      R)
    ((traceAux R (ι := ↥(Finset.image.{w, v} (α := ι) (⇑b : (a : ι) → M) Finset.univ)) b.reindexFinsetRange :
          (a : M →ₗ[R] M) → R)
        f :
      R)
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R)
    (Matrix.trace.{w, u} (n := ι) ((toMatrix b b : (a : M →ₗ[R] M) → Matrix ι ι R) f) : R)

Tactic:
classical
  rw [trace_eq_matrix_trace_of_finset R b.reindexFinsetRange, ← traceAux_def, ← traceAux_def,
    traceAux_eq R b b.reindexFinsetRange]

Premises used: LinearMap.traceAux_def
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type w
inst_3 : DecidableEq ι
inst_4 : Fintype ι
A : Matrix ι ι R
b : Basis ι R M
⊢ (trace R M : (a : M →ₗ[R] M) → R) ((Matrix.toLin b b : (a : Matrix ι ι R) → M →ₗ[R] M) A : M →ₗ[R] M) = A.trace

Tactic:
simp [trace_eq_matrix_trace R b]

Premises used: LinearMap.trace_eq_matrix_trace
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
ι : Type w
inst_1 : DecidableEq ι
inst_2 : Fintype ι
A : Matrix ι ι R
⊢ (trace R (ι → R) : (a : (ι → R) →ₗ[R] ι → R) → R)
      ((Matrix.toLin' : (a : Matrix ι ι R) → (ι → R) →ₗ[R] ι → R) A : (ι → R) →ₗ[R] ι → R) =
    A.trace

Tactic:
A.trace_toLin_eq (Pi.basisFun R ι)

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.trace_toLin_eq, Pi.basisFun, Matrix.mulVec, Finset.sum
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
pos :
  ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)),
    Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g) : R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)
neg :
  ∀ (H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)),
    Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g) : R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g) : R) ((trace R M : (a : M →ₗ[R] M) → R) (g * 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
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)
pos :
  ∀ (s : Finset M) (b : Basis (↥s) R M),
    Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g) : R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g) : R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)

Tactic:
let ⟨s, ⟨b⟩⟩ := H
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)
s : Finset M
b : Basis (↥s) R M
pos :
  (HMul.hMul (α := Matrix.{v, v, u} (↥s) (↥s) R) (β := Matrix.{v, v, u} (↥s) (↥s) R)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (↥s) (↥s) R) f : Matrix.{v, v, u} (↥s) (↥s) R)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (↥s) (↥s) R) g : Matrix.{v, v, u} (↥s) (↥s) R)).trace =
    (HMul.hMul (α := Matrix.{v, v, u} (↥s) (↥s) R) (β := Matrix.{v, v, u} (↥s) (↥s) R)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (↥s) (↥s) R) g : Matrix.{v, v, u} (↥s) (↥s) R)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (↥s) (↥s) R) f : Matrix.{v, v, u} (↥s) (↥s) R)).trace
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g) : R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)

Tactic:
simp_rw [trace_eq_matrix_trace R b, LinearMap.toMatrix_mul]

Premises used: LinearMap.toMatrix_mul, LinearMap.trace_eq_matrix_trace
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)
s : Finset M
b : Basis (↥s) R M
⊢ (HMul.hMul (α := Matrix.{v, v, u} (↥s) (↥s) R) (β := Matrix.{v, v, u} (↥s) (↥s) R)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (↥s) (↥s) R) f : Matrix.{v, v, u} (↥s) (↥s) R)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (↥s) (↥s) R) g : Matrix.{v, v, u} (↥s) (↥s) R)).trace =
    (HMul.hMul (α := Matrix.{v, v, u} (↥s) (↥s) R) (β := Matrix.{v, v, u} (↥s) (↥s) R)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (↥s) (↥s) R) g : Matrix.{v, v, u} (↥s) (↥s) R)
        ((toMatrix b b : (a : M →ₗ[R] M) → Matrix (↥s) (↥s) R) f : Matrix.{v, v, u} (↥s) (↥s) R)).trace

Tactic:
apply Matrix.trace_mul_comm

Premises used: Matrix.trace_mul_comm
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)
neg :
  Eq.{u + 1} (α := R)
    ((if H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M) then traceAux R ⋯.some else 0 : (a : M →ₗ[R] M) → R) (f * g) :
      R)
    ((if H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M) then traceAux R ⋯.some else 0 : (a : M →ₗ[R] M) → R) (g * f) :
      R)
neg₁ : Eq.{u + 1} (α := R) ((0 : (a : M →ₗ[R] M) → R) (f * g) : R) ((0 : (a : M →ₗ[R] M) → R) (g * f) : R)
neg₂ : Eq.{u + 1} (α := R) (0 : R) ((0 : (a : M →ₗ[R] M) → R) (g * f) : R)
neg₃ neg₄ : Eq.{u + 1} (α := R) 0 0
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g) : R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)

Tactic:
rw [trace, dif_neg H, LinearMap.zero_apply, LinearMap.zero_apply]

Premises used: LinearMap.trace, LinearMap.zero_apply, dif_neg
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g : M →ₗ[R] M
pos :
  ∀ (H : ∃ (s : Finset M), Nonempty (Basis (↥s) R M)),
    Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g) : R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)
neg neg₁ :
  ∀ (H : ¬∃ (s : Finset M), Nonempty (Basis (↥s) R M)),
    Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g) : R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g) : R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)

Tactic:
classical
  by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)
  · let ⟨s, ⟨b⟩⟩ := H
    simp_rw [trace_eq_matrix_trace R b, LinearMap.toMatrix_mul]
    apply Matrix.trace_mul_comm
  · rw [trace, dif_neg H, LinearMap.zero_apply, LinearMap.zero_apply]

Premises used: LinearMap.trace, LinearMap.zero_apply, Matrix.trace_mul_comm, Finset, LinearMap.toMatrix_mul
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g h : M →ₗ[R] M
rw :
  Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (h * (f * g)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (h * f * g) : R)
rw₁ rw₂ :
  Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (h * f * g) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (h * f * g) : R)
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g * h) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (h * f * g) : R)

Tactic:
rw [LinearMap.trace_mul_comm, ← mul_assoc]

Premises used: mul_assoc, LinearMap.trace_mul_comm
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
f g h : M →ₗ[R] M
rw :
  Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * g * h) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (h * (f * g)) : R)
rw₁ rw₂ :
  Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (h * (f * g)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (h * (f * g)) : R)
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (h * (f * g)) : R)

Tactic:
rw [← mul_assoc, LinearMap.trace_mul_comm]

Premises used: mul_assoc, LinearMap.trace_mul_comm
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g h : M →ₗ[R] M
simp :
  HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) (g * (f * h)) : R) =
    HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) (f * (h * g)) : R)
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (⁅f, g⁆ * h) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) (f * ⁅g, h⁆) : R)

Tactic:
simp only [Ring.lie_def, sub_mul, mul_sub, map_sub, mul_assoc]

Premises used: map_sub, mul_sub, mul_assoc, sub_mul, Ring.lie_def
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g h : M →ₗ[R] M
rw :
  HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) (f * h * g) : R) =
    HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) (f * (h * g)) : R)
rw₁ rw₂ :
  HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) (f * (h * g)) : R) =
    HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) (f * (h * g)) : R)
⊢ HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) (g * (f * h)) : R) =
    HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (f * (g * h)) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) (f * (h * g)) : R)

Tactic:
rw [trace_mul_comm R g (f * h), mul_assoc]

Premises used: HMul.hMul, mul_assoc, LinearMap.trace_mul_comm
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
g : M →ₗ[R] M
f : (M →ₗ[R] M)ˣ
rw :
  Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) ((↑f⁻¹ : M →ₗ[R] M) * ((↑f : M →ₗ[R] M) * g)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) g : R)
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) ((↑f : M →ₗ[R] M) * g * (↑f⁻¹ : M →ₗ[R] M)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) g : R)

Tactic:
rw [trace_mul_comm]

Premises used: LinearMap.trace_mul_comm
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
g : M →ₗ[R] M
f : (M →ₗ[R] M)ˣ
⊢ Eq.{u + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) ((↑f⁻¹ : M →ₗ[R] M) * ((↑f : M →ₗ[R] M) * g)) : R)
    ((trace R M : (a : M →ₗ[R] M) → R) g : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
rw :
  HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R) =
    0
⊢ Eq.{u_2 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) ⁅f, g⁆ : R) (0 : R)

Tactic:
rw [Ring.lie_def, map_sub, trace_mul_comm]

Premises used: map_sub, LinearMap.trace_mul_comm, Ring.lie_def
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
⊢ HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R) =
    0

Tactic:
sub_self _

Premises used: sub_self
-- Module: Mathlib.LinearAlgebra.Trace
Goal:
R : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
⊢ HSub.hSub (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R)
      ((trace R M : (a : M →ₗ[R] M) → R) (g * f) : R) =
    0

Tactic:
exact sub_self _

Premises used: sub_self
-- 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
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
intro : ∀ (val : Fintype ι), Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)
⊢ Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- 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
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
val : Fintype ι
intro :
  ∀ (i : ι × ι),
    Eq.{u_1 + 1} (α := R)
      ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
            Dual R M ⊗[R] M) :
        R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R)
          (((b.dualBasis.tensorProduct b : Basis (ι × ι) R (Dual R M ⊗[R] M)) : (a : ι × ι) → Dual R M ⊗[R] M) i :
            Dual R M ⊗[R] M) :
        R)
⊢ Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)

Tactic:
apply Basis.ext (Basis.tensorProduct (Basis.dualBasis b) b)

Premises used: Module.Basis.dualBasis, Module.Basis.tensorProduct, Module.Basis.ext