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
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
e : (Dual R M ⊗[R] M × Dual R N ⊗[R] N) ≃ₗ[R] Prod.{u_2, u_3} (M →ₗ[R] M) (N →ₗ[R] N) :=
  LinearEquiv.prodCongr (dualTensorHomEquiv R M M) (dualTensorHomEquiv R N N)
h :
  Function.Surjective (α := Dual R M ⊗[R] M × Dual R N ⊗[R] N) (β := Prod.{u_2, u_3} (M →ₗ[R] M) (N →ₗ[R] N))
    (⇑(↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N)) :
      (a : Dual R M ⊗[R] M × Dual R N ⊗[R] N) → (M →ₗ[R] M) × (N →ₗ[R] N))
x : Dual R N
x_1 : N
⊢ Eq.{u_1 + 1} (α := R)
    (((((AlgebraTensorModule.curry
                    (((trace R (M × N) ∘ₗ prodMapLinear R M N M N R) ∘ₗ
                        (↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N))) ∘ₗ
                      inr R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)) :
                  Dual R N →ₗ[R] N →ₗ[R] R) :
                (a : Dual R N) → N →ₗ[R] R)
              x :
            N →ₗ[R] R) :
          (a : N) → R)
        x_1 :
      R)
    (((((AlgebraTensorModule.curry
                    (((coprod id id ∘ₗ prodMap (trace R M) (trace R N)) ∘ₗ
                        (↑e : Dual R M ⊗[R] M × Dual R N ⊗[R] N →ₗ[R] (M →ₗ[R] M) × (N →ₗ[R] N))) ∘ₗ
                      inr R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)) :
                  Dual R N →ₗ[R] N →ₗ[R] R) :
                (a : Dual R N) → N →ₗ[R] R)
              x :
            N →ₗ[R] R) :
          (a : N) → R)
        x_1 :
      R)

Tactic:
simp only [dualTensorHomEquiv, LinearEquiv.coe_prodCongr,
      dualTensorHomEquivOfBasis_toLinearMap, AlgebraTensorModule.curry_apply,
      curry_apply, coe_comp, coe_restrictScalars, coe_inr, Function.comp_apply, prodMap_apply,
      map_zero, prodMapLinear_apply, zero_prodMap_dualTensorHom, trace_eq_contract_apply,
      contractLeft_apply, coe_snd, coprod_apply, id_coe, id_eq, zero_add, e]

Premises used: dualTensorHomEquiv, LinearMap.prodMap_apply, zero_prodMap_dualTensorHom, LinearMap.coe_inr, LinearMap.id_coe, LinearMap.coe_restrictScalars, LinearMap.trace_eq_contract_apply, LinearMap.coprod_apply, map_zero, LinearMap.prodMapLinear_apply, zero_add, TensorProduct.AlgebraTensorModule.curry_apply, LinearMap.coe_snd, LinearMap.coe_comp, contractLeft_apply, dualTensorHomEquivOfBasis_toLinearMap, TensorProduct.curry_apply, Function.comp_apply, LinearEquiv.coe_prodCongr, id_eq
-- 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
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R (M × N) ∘ₗ prodMapLinear R M N M N R : (a : (M →ₗ[R] M) × (N →ₗ[R] N)) → R) (f, g) : R)
    ((coprod id id ∘ₗ prodMap (trace R M) (trace R N) : (a : (M →ₗ[R] M) × (N →ₗ[R] N)) → R) (f, g) : R)

Tactic:
have h := LinearMap.ext_iff.1 (trace_prodMap R M N) (f, g)
-- 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
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
h :
  (trace R (M × N) : (a : M × N →ₗ[R] M × N) → R) (f.prodMap g) =
    HAdd.hAdd (α := R) (β := R)
      (({ toFun := fun (x : R) ↦ x, map_add' := ⋯, map_smul' := ⋯ : R →ₗ[R] R } : (a : R) → R)
          ((trace R M : (a : M →ₗ[R] M) → R) f : R) :
        R)
      (({ toFun := fun (x : R) ↦ x, map_add' := ⋯, map_smul' := ⋯ : R →ₗ[R] R } : (a : R) → R)
          ((trace R N : (a : N →ₗ[R] N) → R) g : R) :
        R)
⊢ (trace R (M × N) : (a : M × N →ₗ[R] M × N) → R) (f.prodMap g) =
    HAdd.hAdd (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R) ((trace R N : (a : N →ₗ[R] N) → R) g : R)

Tactic:
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
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
h :
  (trace R (M × N) : (a : M × N →ₗ[R] M × N) → R) (f.prodMap g) =
    HAdd.hAdd (α := R) (β := R)
      (({ toFun := fun (x : R) ↦ x, map_add' := ⋯, map_smul' := ⋯ : R →ₗ[R] R } : (a : R) → R)
          ((trace R M : (a : M →ₗ[R] M) → R) f : R) :
        R)
      (({ toFun := fun (x : R) ↦ x, map_add' := ⋯, map_smul' := ⋯ : R →ₗ[R] R } : (a : R) → R)
          ((trace R N : (a : N →ₗ[R] N) → R) g : R) :
        R)
⊢ (trace R (M × N) : (a : M × N →ₗ[R] M × N) → R) (f.prodMap g) =
    HAdd.hAdd (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R) ((trace R N : (a : N →ₗ[R] N) → R) g : R)

Tactic:
exact 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
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
Surjective :
  Eq (α := Dual R M ⊗[R] M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R)
    (compl₁₂ (compr₂ (mapBilinear (RingHom.id R) M N M N) (trace R (M ⊗[R] N))) (dualTensorHom R M M)
      (dualTensorHom R N N))
    (compl₁₂ (compl₁₂ (lsmul R R) (trace R M) (trace R N)) (dualTensorHom R M M) (dualTensorHom R N N))
⊢ Eq (α := (M →ₗ[R] M) →ₗ[R] LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (N →ₗ[R] N) R)
    (compr₂ (mapBilinear (RingHom.id R) M N M N) (trace R (M ⊗[R] N))) (compl₁₂ (lsmul R R) (trace R M) (trace R N))

Tactic:
apply
    (compl₁₂_inj (show Surjective (dualTensorHom R M M) from (dualTensorHomEquiv R M M).surjective)
        (show Surjective (dualTensorHom R N N) from (dualTensorHomEquiv R N N).surjective)).1

Premises used: dualTensorHomEquiv, LinearEquiv.surjective, LinearMap.compl₁₂_inj, Iff.mp
-- 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
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
a :
  ∀ (f : Dual R M) (m : M) (g : Dual R N) (n : N),
    Eq.{u_1 + 1} (α := R)
      (((((AlgebraTensorModule.curry
                      (((((AlgebraTensorModule.curry
                                    (compl₁₂ (compr₂ (mapBilinear (RingHom.id R) M N M N) (trace R (M ⊗[R] N)))
                                      (dualTensorHom R M M) (dualTensorHom R N N)) :
                                  Dual R M →ₗ[R] M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R) :
                                (a : Dual R M) → M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R)
                              f :
                            M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R) :
                          (a : M) → Dual R N ⊗[R] N →ₗ[R] R)
                        m) :
                    Dual R N →ₗ[R] N →ₗ[R] R) :
                  (a : Dual R N) → N →ₗ[R] R)
                g :
              N →ₗ[R] R) :
            (a : N) → R)
          n :
        R)
      (((((AlgebraTensorModule.curry
                      (((((AlgebraTensorModule.curry
                                    (compl₁₂ (compl₁₂ (lsmul R R) (trace R M) (trace R N)) (dualTensorHom R M M)
                                      (dualTensorHom R N N)) :
                                  Dual R M →ₗ[R] M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R) :
                                (a : Dual R M) → M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R)
                              f :
                            M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R) :
                          (a : M) → Dual R N ⊗[R] N →ₗ[R] R)
                        m) :
                    Dual R N →ₗ[R] N →ₗ[R] R) :
                  (a : Dual R N) → N →ₗ[R] R)
                g :
              N →ₗ[R] R) :
            (a : N) → R)
          n :
        R)
⊢ Eq (α := Dual R M ⊗[R] M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R)
    (compl₁₂ (compr₂ (mapBilinear (RingHom.id R) M N M N) (trace R (M ⊗[R] N))) (dualTensorHom R M M)
      (dualTensorHom R N N))
    (compl₁₂ (compl₁₂ (lsmul R R) (trace R M) (trace R N)) (dualTensorHom R M M) (dualTensorHom R N N))

Tactic:
ext f m g n
-- 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
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
f : Dual R M
m : M
g : Dual R N
n : N
⊢ Eq.{u_1 + 1} (α := R)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry
                                  (compl₁₂ (compr₂ (mapBilinear (RingHom.id R) M N M N) (trace R (M ⊗[R] N)))
                                    (dualTensorHom R M M) (dualTensorHom R N N)) :
                                Dual R M →ₗ[R] M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R) :
                              (a : Dual R M) → M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R)
                            f :
                          M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R) :
                        (a : M) → Dual R N ⊗[R] N →ₗ[R] R)
                      m) :
                  Dual R N →ₗ[R] N →ₗ[R] R) :
                (a : Dual R N) → N →ₗ[R] R)
              g :
            N →ₗ[R] R) :
          (a : N) → R)
        n :
      R)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry
                                  (compl₁₂ (compl₁₂ (lsmul R R) (trace R M) (trace R N)) (dualTensorHom R M M)
                                    (dualTensorHom R N N)) :
                                Dual R M →ₗ[R] M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R) :
                              (a : Dual R M) → M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R)
                            f :
                          M →ₗ[R] Dual R N ⊗[R] N →ₗ[R] R) :
                        (a : M) → Dual R N ⊗[R] N →ₗ[R] R)
                      m) :
                  Dual R N →ₗ[R] N →ₗ[R] R) :
                (a : Dual R N) → N →ₗ[R] R)
              g :
            N →ₗ[R] R) :
          (a : N) → R)
        n :
      R)

Tactic:
simp only [AlgebraTensorModule.curry_apply, TensorProduct.curry_apply,
    coe_restrictScalars, compl₁₂_apply, compr₂_apply, mapBilinear_apply,
    trace_eq_contract_apply, contractLeft_apply, lsmul_apply, smul_eq_mul,
    map_dualTensorHom, dualDistrib_apply]

Premises used: LinearMap.coe_restrictScalars, LinearMap.trace_eq_contract_apply, LinearMap.compr₂_apply, TensorProduct.mapBilinear_apply, TensorProduct.AlgebraTensorModule.curry_apply, LinearMap.lsmul_apply, contractLeft_apply, LinearMap.compl₁₂_apply, TensorProduct.curry_apply, map_dualTensorHom, TensorProduct.dualDistrib_apply, smul_eq_mul
-- 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
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
Surjective :
  Eq (α := Dual R N ⊗[R] M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R)
    (compl₁₂ (compr₂ (llcomp R M N M) (trace R M)) (dualTensorHom R N M) (dualTensorHom R M N))
    (compl₁₂ (compr₂ (flip (llcomp R N M N)) (trace R N)) (dualTensorHom R N M) (dualTensorHom R M N))
⊢ Eq (α := (N →ₗ[R] M) →ₗ[R] (M →ₗ[R] N) →ₗ[R] R) (compr₂ (llcomp R M N M) (trace R M))
    (compr₂ (flip (llcomp R N M N)) (trace R N))

Tactic:
apply
    (compl₁₂_inj (show Surjective (dualTensorHom R N M) from (dualTensorHomEquiv R N M).surjective)
        (show Surjective (dualTensorHom R M N) from (dualTensorHomEquiv R M N).surjective)).1

Premises used: dualTensorHomEquiv, LinearEquiv.surjective, LinearMap.compl₁₂_inj, Iff.mp
-- 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
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
a :
  ∀ (g : Dual R N) (m : M) (f : Dual R M) (n : N),
    Eq.{u_1 + 1} (α := R)
      (((((AlgebraTensorModule.curry
                      (((((AlgebraTensorModule.curry
                                    (compl₁₂ (compr₂ (llcomp R M N M) (trace R M)) (dualTensorHom R N M)
                                      (dualTensorHom R M N)) :
                                  Dual R N →ₗ[R] M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R) :
                                (a : Dual R N) → M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R)
                              g :
                            M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R) :
                          (a : M) → Dual R M ⊗[R] N →ₗ[R] R)
                        m) :
                    Dual R M →ₗ[R] N →ₗ[R] R) :
                  (a : Dual R M) → N →ₗ[R] R)
                f :
              N →ₗ[R] R) :
            (a : N) → R)
          n :
        R)
      (((((AlgebraTensorModule.curry
                      (((((AlgebraTensorModule.curry
                                    (compl₁₂ (compr₂ (flip (llcomp R N M N)) (trace R N)) (dualTensorHom R N M)
                                      (dualTensorHom R M N)) :
                                  Dual R N →ₗ[R] M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R) :
                                (a : Dual R N) → M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R)
                              g :
                            M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R) :
                          (a : M) → Dual R M ⊗[R] N →ₗ[R] R)
                        m) :
                    Dual R M →ₗ[R] N →ₗ[R] R) :
                  (a : Dual R M) → N →ₗ[R] R)
                f :
              N →ₗ[R] R) :
            (a : N) → R)
          n :
        R)
⊢ Eq (α := Dual R N ⊗[R] M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R)
    (compl₁₂ (compr₂ (llcomp R M N M) (trace R M)) (dualTensorHom R N M) (dualTensorHom R M N))
    (compl₁₂ (compr₂ (flip (llcomp R N M N)) (trace R N)) (dualTensorHom R N M) (dualTensorHom R M N))

Tactic:
ext g m f n
-- 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
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
g : Dual R N
m : M
f : Dual R M
n : N
⊢ Eq.{u_1 + 1} (α := R)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry
                                  (compl₁₂ (compr₂ (llcomp R M N M) (trace R M)) (dualTensorHom R N M)
                                    (dualTensorHom R M N)) :
                                Dual R N →ₗ[R] M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R) :
                              (a : Dual R N) → M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R)
                            g :
                          M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R) :
                        (a : M) → Dual R M ⊗[R] N →ₗ[R] R)
                      m) :
                  Dual R M →ₗ[R] N →ₗ[R] R) :
                (a : Dual R M) → N →ₗ[R] R)
              f :
            N →ₗ[R] R) :
          (a : N) → R)
        n :
      R)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry
                                  (compl₁₂ (compr₂ (flip (llcomp R N M N)) (trace R N)) (dualTensorHom R N M)
                                    (dualTensorHom R M N)) :
                                Dual R N →ₗ[R] M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R) :
                              (a : Dual R N) → M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R)
                            g :
                          M →ₗ[R] Dual R M ⊗[R] N →ₗ[R] R) :
                        (a : M) → Dual R M ⊗[R] N →ₗ[R] R)
                      m) :
                  Dual R M →ₗ[R] N →ₗ[R] R) :
                (a : Dual R M) → N →ₗ[R] R)
              f :
            N →ₗ[R] R) :
          (a : N) → R)
        n :
      R)

Tactic:
simp only [AlgebraTensorModule.curry_apply, TensorProduct.curry_apply,
    coe_restrictScalars, compl₁₂_apply, compr₂_apply, flip_apply, llcomp_apply',
    comp_dualTensorHom, LinearMapClass.map_smul, trace_eq_contract_apply,
    contractLeft_apply, smul_eq_mul, mul_comm]

Premises used: LinearMap.coe_restrictScalars, LinearMap.trace_eq_contract_apply, LinearMap.compr₂_apply, LinearMap.flip_apply, LinearMap.llcomp_apply', TensorProduct.AlgebraTensorModule.curry_apply, contractLeft_apply, LinearMap.compl₁₂_apply, LinearMapClass.map_smul, TensorProduct.curry_apply, comp_dualTensorHom, mul_comm, smul_eq_mul
-- 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] M
rw :
  Eq.{u_1 + 1} (α := R) ((trace R (Dual R M) ∘ₗ Dual.transpose : (a : M →ₗ[R] M) → R) f : R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)
rw₁ rw₂ : 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 (Dual R M) : (a : Dual R M →ₗ[R] Dual R M) → R)
        ((Dual.transpose : (a : M →ₗ[R] M) → Dual R M →ₗ[R] Dual R M) f : Dual R M →ₗ[R] Dual R M) :
      R)
    ((trace R M : (a : M →ₗ[R] M) → R) f : R)

Tactic:
rw [← comp_apply, trace_transpose]

Premises used: LinearMap.comp_apply, LinearMap.trace_transpose
-- 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
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
⊢ Eq.{u_1 + 1} (α := R)
    ((((compr₂ (mapBilinear (RingHom.id R) M N M N) (trace R (M ⊗[R] N)) : (a : M →ₗ[R] M) → (N →ₗ[R] N) →ₗ[R] R) f :
            LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (N →ₗ[R] N) R) :
          (a : N →ₗ[R] N) → R)
        g :
      R)
    ((((compl₁₂ (lsmul R R) (trace R M) (trace R N) : (a : M →ₗ[R] M) → (N →ₗ[R] N) →ₗ[R] R) f :
            LinearMap.{u_1, u_1, u_3, u_1} (RingHom.id R) (N →ₗ[R] N) R) :
          (a : N →ₗ[R] N) → R)
        g :
      R)

Tactic:
have h := LinearMap.ext_iff.1 (LinearMap.ext_iff.1 (trace_tensorProduct R M N) f) g
-- 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
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
h :
  (trace R (M ⊗[R] N) : (a : M ⊗[R] N →ₗ[R] M ⊗[R] N) → R) (map f g) =
    HMul.hMul (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R) ((trace R N : (a : N →ₗ[R] N) → R) g : R)
⊢ (trace R (M ⊗[R] N) : (a : M ⊗[R] N →ₗ[R] M ⊗[R] N) → R) (map f g) =
    HMul.hMul (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R) ((trace R N : (a : N →ₗ[R] N) → R) g : R)

Tactic:
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
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
f : M →ₗ[R] M
g : N →ₗ[R] N
h :
  (trace R (M ⊗[R] N) : (a : M ⊗[R] N →ₗ[R] M ⊗[R] N) → R) (map f g) =
    HMul.hMul (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R) ((trace R N : (a : N →ₗ[R] N) → R) g : R)
⊢ (trace R (M ⊗[R] N) : (a : M ⊗[R] N →ₗ[R] M ⊗[R] N) → R) (map f g) =
    HMul.hMul (α := R) (β := R) ((trace R M : (a : M →ₗ[R] M) → R) f : R) ((trace R N : (a : N →ₗ[R] N) → R) g : R)

Tactic:
exact 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
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] M
⊢ Eq.{u_1 + 1} (α := R)
    ((((compr₂ (llcomp R M N M) (trace R M) : (a : N →ₗ[R] M) → (M →ₗ[R] N) →ₗ[R] R) g : (M →ₗ[R] N) →ₗ[R] R) :
          (a : M →ₗ[R] N) → R)
        f :
      R)
    ((((compr₂ (flip (llcomp R N M N)) (trace R N) : (a : N →ₗ[R] M) → (M →ₗ[R] N) →ₗ[R] R) g : (M →ₗ[R] N) →ₗ[R] R) :
          (a : M →ₗ[R] N) → R)
        f :
      R)

Tactic:
have h := LinearMap.ext_iff.1 (LinearMap.ext_iff.1 (trace_comp_comm R M N) g) 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
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] M
h :
  Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (g ∘ₗ f) : R)
    ((trace R N : (a : N →ₗ[R] N) → R) (f ∘ₗ g) : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (g ∘ₗ f) : R)
    ((trace R N : (a : N →ₗ[R] N) → R) (f ∘ₗ g) : R)

Tactic:
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
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Free R M
inst_6 : Module.Finite R M
inst_7 : Free R N
inst_8 : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] M
h :
  Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (g ∘ₗ f) : R)
    ((trace R N : (a : N →ₗ[R] N) → R) (f ∘ₗ g) : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (g ∘ₗ f) : R)
    ((trace R N : (a : N →ₗ[R] N) → R) (f ∘ₗ g) : R)

Tactic:
exact 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
inst_3 : Free R M
inst_4 : Module.Finite R M
f : M →ₗ[R] R
x : M
rw :
  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)
⊢ Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) (f.smulRight x) : R) ((f : (a : M) → R) x : R)

Tactic:
rw [trace_eq_matrix_trace _ (Free.chooseBasis R M), ← (Free.chooseBasis R M).sum_repr x]

Premises used: LinearMap.trace_eq_matrix_trace, Module.Basis.sum_repr, Module.Free.chooseBasis