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

Tactic:
simp only [Function.comp_apply, Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp]

Premises used: Module.Basis.tensorProduct_apply, Module.Basis.coe_dualBasis, LinearMap.coe_comp, Function.comp_apply
-- 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 ι
i j : ι
intro :
  Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single j i 1) : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        ((dualTensorHom R M M : (a : Dual R M ⊗[R] M) → M →ₗ[R] M) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j) : M →ₗ[R] M) :
      R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)

Tactic:
rw [trace_eq_matrix_trace R b, toMatrix_dualTensorHom]

Premises used: toMatrix_dualTensorHom, 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
ι : Type u_5
inst_3 : Finite ι
b : Basis ι R M
val : Fintype ι
i j : ι
intro :
  Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single i i 1) : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) i : Dual R M ⊗[R] M) : R)
intro₁ :
  ∀ (hij : i ≠ j),
    Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single j i 1) : R)
      ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
⊢ Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single j i 1) : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)

Tactic:
obtain rfl | hij := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- 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 ι
i : ι
⊢ Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single i i 1) : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) i : Dual R M ⊗[R] M) : R)

Tactic:
simp
-- 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 ι
i j : ι
hij : i ≠ j
intro :
  Eq.{u_1 + 1} (α := R) (0 : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)
⊢ Eq.{u_1 + 1} (α := R) (Matrix.trace (Matrix.single j i 1) : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)

Tactic:
rw [Matrix.trace_single_eq_of_ne j i (1 : R) hij.symm]

Premises used: Ne.symm, Matrix.trace_single_eq_of_ne, OfNat.ofNat
-- 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 ι
i j : ι
hij : i ≠ j
⊢ Eq.{u_1 + 1} (α := R) (0 : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) (b.coord i ⊗ₜ[R] (b : (a : ι) → M) j : Dual R M ⊗[R] M) : R)

Tactic:
simp [hij]
-- 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 : Fintype ι
inst_4 : DecidableEq ι
b : Basis ι R M
⊢ trace R M =
    contractLeft R M ∘ₗ (↑(LinearEquiv.symm (dualTensorHomEquivOfBasis b)) : (M →ₗ[R] M) →ₗ[R] Dual R M ⊗[R] M)

Tactic:
simp [LinearEquiv.eq_comp_toLinearMap_symm, trace_eq_contract_of_basis b]

Premises used: LinearEquiv.eq_comp_toLinearMap_symm, LinearMap.trace_eq_contract_of_basis
-- 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
⊢ Eq (α := Dual R M ⊗[R] M →ₗ[R] R) (trace R M ∘ₗ dualTensorHom R M M) (contractLeft R M)

Tactic:
trace_eq_contract_of_basis (Module.Free.chooseBasis R M)

Premises used: LinearMap.trace_eq_contract_of_basis, Module.Free.chooseBasis
-- 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
x : Dual R M ⊗[R] M
rw :
  Eq.{u_1 + 1} (α := R) ((trace R M ∘ₗ dualTensorHom R M M : (a : Dual R M ⊗[R] M) → R) x : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) x : R)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := R) ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) x : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) x : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R) ((dualTensorHom R M M : (a : Dual R M ⊗[R] M) → M →ₗ[R] M) x : M →ₗ[R] M) : R)
    ((contractLeft R M : (a : Dual R M ⊗[R] M) → R) x : R)

Tactic:
rw [← comp_apply, trace_eq_contract]

Premises used: LinearMap.trace_eq_contract, LinearMap.comp_apply
-- 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
⊢ Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M →ₗ[R] M) R) (trace R M)
    (contractLeft R M ∘ₗ (↑(LinearEquiv.symm (dualTensorHomEquiv R M M)) : (M →ₗ[R] M) →ₗ[R] Dual R M ⊗[R] M))

Tactic:
trace_eq_contract_of_basis' (Module.Free.chooseBasis R M)

Premises used: dualTensorHomEquiv, LinearMap.trace_eq_contract_of_basis', Module.Free.chooseBasis
-- 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
inl : Subsingleton R → Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) 1 : R) ((↑(finrank R M) : R) : R)
inr : Nontrivial R → Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) 1 : R) ((↑(finrank R M) : R) : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) 1 : R) ((↑(finrank R M) : R) : R)

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- 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
h : Subsingleton R
⊢ Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) 1 : R) ((↑(finrank R M) : R) : R)

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- 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
h : Nontrivial R
inr :
  ∀ (b : Basis (Free.ChooseBasisIndex R M) R M),
    Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) 1 : R) ((↑(finrank R M) : R) : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) 1 : R) ((↑(finrank R M) : R) : R)

Tactic:
have b := Module.Free.chooseBasis R M
-- 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
h : Nontrivial R
b : Basis (Free.ChooseBasisIndex R M) R M
inr :
  Eq.{u_1 + 1} (α := R) (Matrix.trace.{u_2, u_1} (n := Free.ChooseBasisIndex R M) 1)
    (↑(Fintype.card.{u_2} (Free.ChooseBasisIndex R M)) : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) 1 : R) ((↑(finrank R M) : R) : R)

Tactic:
rw [trace_eq_matrix_trace R b, toMatrix_one, finrank_eq_card_chooseBasisIndex]

Premises used: LinearMap.toMatrix_one, Module.finrank_eq_card_chooseBasisIndex, 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
inst_3 : Free R M
inst_4 : Module.Finite R M
h : Nontrivial R
b : Basis (Free.ChooseBasisIndex R M) R M
⊢ Eq.{u_1 + 1} (α := R) (Matrix.trace.{u_2, u_1} (n := Free.ChooseBasisIndex R M) 1)
    (↑(Fintype.card.{u_2} (Free.ChooseBasisIndex R M)) : R)

Tactic:
simp
-- 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
rw : Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) 1 : R) ((↑(finrank R M) : R) : R)
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) (↑(finrank R M) : R) (↑(finrank R M) : R)
⊢ Eq.{u_1 + 1} (α := R) ((trace R M : (a : M →ₗ[R] M) → R) id : R) ((↑(finrank R M) : R) : R)

Tactic:
rw [← Module.End.one_eq_id, trace_one]

Premises used: Module.End.one_eq_id, LinearMap.trace_one
-- 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
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
⊢ Function.Surjective (α := Dual R M ⊗[R] M) (β := M →ₗ[R] M)
    (⇑(↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M) : (a : Dual R M ⊗[R] M) → M →ₗ[R] M)

Tactic:
have h : Function.Surjective e.toLinearMap := e.surjective
-- 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
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h :
  Function.Surjective (α := Dual R M ⊗[R] M) (β := M →ₗ[R] M)
    (⇑(↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M) : (a : Dual R M ⊗[R] M) → M →ₗ[R] M)
⊢ Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M →ₗ[R] M) R) (trace R (Dual R M) ∘ₗ Dual.transpose)
    (trace R M)

Tactic:
(cancel_right h).1 ?_

Premises used: LinearMap.cancel_right, 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
inst_3 : Free R M
inst_4 : Module.Finite R M
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h :
  Function.Surjective (α := Dual R M ⊗[R] M) (β := M →ₗ[R] M)
    (⇑(↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M) : (a : Dual R M ⊗[R] M) → M →ₗ[R] M)
refine :
  (trace R (Dual R M) ∘ₗ Dual.transpose) ∘ₗ (↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M) =
    trace R M ∘ₗ (↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M)
⊢ Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (M →ₗ[R] M) R) (trace R (Dual R M) ∘ₗ Dual.transpose)
    (trace R M)

Tactic:
refine (cancel_right h).1 ?_

Premises used: LinearMap.cancel_right, 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
inst_3 : Free R M
inst_4 : Module.Finite R M
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h :
  Function.Surjective (α := Dual R M ⊗[R] M) (β := M →ₗ[R] M)
    (⇑(↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M) : (a : Dual R M ⊗[R] M) → M →ₗ[R] M)
a :
  ∀ (f : Dual R M) (m : M),
    Eq.{u_1 + 1} (α := R)
      (((((AlgebraTensorModule.curry
                      ((trace R (Dual R M) ∘ₗ Dual.transpose) ∘ₗ (↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M)) :
                    Dual R M →ₗ[R] M →ₗ[R] R) :
                  (a : Dual R M) → M →ₗ[R] R)
                f :
              M →ₗ[R] R) :
            (a : M) → R)
          m :
        R)
      (((((AlgebraTensorModule.curry (trace R M ∘ₗ (↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M)) : Dual R M →ₗ[R] M →ₗ[R] R) :
                  (a : Dual R M) → M →ₗ[R] R)
                f :
              M →ₗ[R] R) :
            (a : M) → R)
          m :
        R)
⊢ (trace R (Dual R M) ∘ₗ Dual.transpose) ∘ₗ (↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M) =
    trace R M ∘ₗ (↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M)

Tactic:
ext f m
-- 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
e : Dual R M ⊗[R] M ≃ₗ[R] M →ₗ[R] M := dualTensorHomEquiv R M M
h :
  Function.Surjective (α := Dual R M ⊗[R] M) (β := M →ₗ[R] M)
    (⇑(↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M) : (a : Dual R M ⊗[R] M) → M →ₗ[R] M)
f : Dual R M
m : M
⊢ Eq.{u_1 + 1} (α := R)
    (((((AlgebraTensorModule.curry ((trace R (Dual R M) ∘ₗ Dual.transpose) ∘ₗ (↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M)) :
                  Dual R M →ₗ[R] M →ₗ[R] R) :
                (a : Dual R M) → M →ₗ[R] R)
              f :
            M →ₗ[R] R) :
          (a : M) → R)
        m :
      R)
    (((((AlgebraTensorModule.curry (trace R M ∘ₗ (↑e : Dual R M ⊗[R] M →ₗ[R] M →ₗ[R] M)) : Dual R M →ₗ[R] M →ₗ[R] R) :
                (a : Dual R M) → M →ₗ[R] R)
              f :
            M →ₗ[R] R) :
          (a : M) → R)
        m :
      R)

Tactic:
simp [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
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)
⊢ 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))

Tactic:
have h : Function.Surjective e.toLinearMap := e.surjective
-- 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))
⊢ Eq (α := Prod.{u_2, u_3} (M →ₗ[R] M) (N →ₗ[R] N) →ₗ[R] R) (trace R (M × N) ∘ₗ prodMapLinear R M N M N R)
    (coprod id id ∘ₗ prodMap (trace R M) (trace R N))

Tactic:
(cancel_right h).1 ?_

Premises used: LinearMap.cancel_right, 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
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))
refine :
  (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)) =
    (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))
⊢ Eq (α := Prod.{u_2, u_3} (M →ₗ[R] M) (N →ₗ[R] N) →ₗ[R] R) (trace R (M × N) ∘ₗ prodMapLinear R M N M N R)
    (coprod id id ∘ₗ prodMap (trace R M) (trace R N))

Tactic:
refine (cancel_right h).1 ?_

Premises used: LinearMap.cancel_right, 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
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))
hl :
  ∀ (x : Dual R M) (x_1 : M),
    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))) ∘ₗ
                        inl R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)) :
                    Dual R M →ₗ[R] M →ₗ[R] R) :
                  (a : Dual R M) → M →ₗ[R] R)
                x :
              M →ₗ[R] R) :
            (a : M) → 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))) ∘ₗ
                        inl R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)) :
                    Dual R M →ₗ[R] M →ₗ[R] R) :
                  (a : Dual R M) → M →ₗ[R] R)
                x :
              M →ₗ[R] R) :
            (a : M) → R)
          x_1 :
        R)
hr :
  ∀ (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)
⊢ (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)) =
    (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))

Tactic:
ext
-- 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 M
x_1 : M
⊢ 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))) ∘ₗ
                      inl R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)) :
                  Dual R M →ₗ[R] M →ₗ[R] R) :
                (a : Dual R M) → M →ₗ[R] R)
              x :
            M →ₗ[R] R) :
          (a : M) → 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))) ∘ₗ
                      inl R (Dual R M ⊗[R] M) (Dual R N ⊗[R] N)) :
                  Dual R M →ₗ[R] M →ₗ[R] R) :
                (a : Dual R M) → M →ₗ[R] R)
              x :
            M →ₗ[R] R) :
          (a : M) → R)
        x_1 :
      R)

Tactic:
simp only [dualTensorHomEquiv, LinearEquiv.coe_prodCongr,
      dualTensorHomEquivOfBasis_toLinearMap, AlgebraTensorModule.curry_apply,
      curry_apply, coe_comp, coe_restrictScalars, coe_inl, Function.comp_apply, prodMap_apply,
      map_zero, prodMapLinear_apply, dualTensorHom_prodMap_zero, trace_eq_contract_apply,
      contractLeft_apply, coe_fst, coprod_apply, id_coe, id_eq, add_zero, e]

Premises used: dualTensorHomEquiv, LinearMap.prodMap_apply, LinearMap.id_coe, LinearMap.coe_restrictScalars, LinearMap.trace_eq_contract_apply, LinearMap.coprod_apply, LinearMap.coe_fst, map_zero, LinearMap.prodMapLinear_apply, TensorProduct.AlgebraTensorModule.curry_apply, LinearMap.coe_inl, LinearMap.coe_comp, contractLeft_apply, dualTensorHom_prodMap_zero, dualTensorHomEquivOfBasis_toLinearMap, TensorProduct.curry_apply, Function.comp_apply, LinearEquiv.coe_prodCongr, add_zero, id_eq