awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : DecidableEq ι
inst_6 : Fintype ι
b : Basis ι R M
x : M →ₗ[R] N
rw :
  (dualTensorHomEquivOfBasis b : (a : Dual R M ⊗[R] N) → M →ₗ[R] N)
      ((LinearEquiv.symm (dualTensorHomEquivOfBasis b) : (a : M →ₗ[R] N) → Dual R M ⊗[R] N) x) =
    x
rw₁ rw₂ : x = x
⊢ (dualTensorHom R M N : (a : Dual R M ⊗[R] N) → M →ₗ[R] N)
      ((LinearEquiv.symm (dualTensorHomEquivOfBasis b) : (a : M →ₗ[R] N) → Dual R M ⊗[R] N) x) =
    x

Tactic:
rw [← dualTensorHomEquivOfBasis_apply b, LinearEquiv.apply_symm_apply]

Premises used: LinearEquiv.apply_symm_apply, dualTensorHomEquivOfBasis_apply
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
e : P ⊗[R] (Dual R M ⊗[R] Q) ≃ₗ[R] P ⊗[R] (M →ₗ[R] Q) :=
  TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
⊢ Function.Surjective (α := P ⊗[R] (Dual R M ⊗[R] Q)) (β := P ⊗[R] (M →ₗ[R] Q))
    (⇑(↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q)) : (a : P ⊗[R] (Dual R M ⊗[R] Q)) → P ⊗[R] (M →ₗ[R] Q))

Tactic:
have h : Function.Surjective e.toLinearMap := e.surjective
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
e : P ⊗[R] (Dual R M ⊗[R] Q) ≃ₗ[R] P ⊗[R] (M →ₗ[R] Q) :=
  TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
h :
  Function.Surjective (α := P ⊗[R] (Dual R M ⊗[R] Q)) (β := P ⊗[R] (M →ₗ[R] Q))
    (⇑(↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q)) : (a : P ⊗[R] (Dual R M ⊗[R] Q)) → P ⊗[R] (M →ₗ[R] Q))
⊢ Eq (α := P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q)
    (↑(lTensorHomEquivHomLTensor R M P Q) : P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q)
    (lTensorHomToHomLTensor (RingHom.id R) M P Q)

Tactic:
(cancel_right h).1 ?_

Premises used: LinearMap.cancel_right, Iff.mp
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
e : P ⊗[R] (Dual R M ⊗[R] Q) ≃ₗ[R] P ⊗[R] (M →ₗ[R] Q) :=
  TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
h :
  Function.Surjective (α := P ⊗[R] (Dual R M ⊗[R] Q)) (β := P ⊗[R] (M →ₗ[R] Q))
    (⇑(↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q)) : (a : P ⊗[R] (Dual R M ⊗[R] Q)) → P ⊗[R] (M →ₗ[R] Q))
refine :
  (↑(lTensorHomEquivHomLTensor R M P Q) : P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q) ∘ₗ
      (↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q)) =
    lTensorHomToHomLTensor (RingHom.id R) M P Q ∘ₗ (↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q))
⊢ Eq (α := P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q)
    (↑(lTensorHomEquivHomLTensor R M P Q) : P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q)
    (lTensorHomToHomLTensor (RingHom.id R) M P Q)

Tactic:
refine (cancel_right h).1 ?_

Premises used: LinearMap.cancel_right, Iff.mp
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
e : P ⊗[R] (Dual R M ⊗[R] Q) ≃ₗ[R] P ⊗[R] (M →ₗ[R] Q) :=
  TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
h :
  Function.Surjective (α := P ⊗[R] (Dual R M ⊗[R] Q)) (β := P ⊗[R] (M →ₗ[R] Q))
    (⇑(↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q)) : (a : P ⊗[R] (Dual R M ⊗[R] Q)) → P ⊗[R] (M →ₗ[R] Q))
H :
  ∀ (f : P) (q : Dual R M) (m : Q) (x : M),
    Eq (α := P ⊗[R] Q)
      ((((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (TensorProduct.mk R (Dual R M) Q)
                          ((compr₂ₛₗ (TensorProduct.mk R P (Dual R M ⊗[R] Q))
                                ((↑(lTensorHomEquivHomLTensor R M P Q) : P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q) ∘ₗ
                                  (↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q))) :
                              (a : P) → Dual R M ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                            f) :
                        (a : Dual R M) → Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                      q :
                    Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
                  (a : Q) → M →ₗ[R] P ⊗[R] Q)
                m :
              M →ₗ[R] P ⊗[R] Q) :
            (a : M) → P ⊗[R] Q)
          x :
        P ⊗[R] Q)
      ((((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (TensorProduct.mk R (Dual R M) Q)
                          ((compr₂ₛₗ (TensorProduct.mk R P (Dual R M ⊗[R] Q))
                                (lTensorHomToHomLTensor (RingHom.id R) M P Q ∘ₗ
                                  (↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q))) :
                              (a : P) → Dual R M ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                            f) :
                        (a : Dual R M) → Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                      q :
                    Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
                  (a : Q) → M →ₗ[R] P ⊗[R] Q)
                m :
              M →ₗ[R] P ⊗[R] Q) :
            (a : M) → P ⊗[R] Q)
          x :
        P ⊗[R] Q)
⊢ (↑(lTensorHomEquivHomLTensor R M P Q) : P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q) ∘ₗ
      (↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q)) =
    lTensorHomToHomLTensor (RingHom.id R) M P Q ∘ₗ (↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q))

Tactic:
ext f q m
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
e : P ⊗[R] (Dual R M ⊗[R] Q) ≃ₗ[R] P ⊗[R] (M →ₗ[R] Q) :=
  TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
h :
  Function.Surjective (α := P ⊗[R] (Dual R M ⊗[R] Q)) (β := P ⊗[R] (M →ₗ[R] Q))
    (⇑(↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q)) : (a : P ⊗[R] (Dual R M ⊗[R] Q)) → P ⊗[R] (M →ₗ[R] Q))
f : P
q : Dual R M
m : Q
x : M
⊢ Eq (α := P ⊗[R] Q)
    ((((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (TensorProduct.mk R (Dual R M) Q)
                        ((compr₂ₛₗ (TensorProduct.mk R P (Dual R M ⊗[R] Q))
                              ((↑(lTensorHomEquivHomLTensor R M P Q) : P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q) ∘ₗ
                                (↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q))) :
                            (a : P) → Dual R M ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                          f) :
                      (a : Dual R M) → Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                    q :
                  Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
                (a : Q) → M →ₗ[R] P ⊗[R] Q)
              m :
            M →ₗ[R] P ⊗[R] Q) :
          (a : M) → P ⊗[R] Q)
        x :
      P ⊗[R] Q)
    ((((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (TensorProduct.mk R (Dual R M) Q)
                        ((compr₂ₛₗ (TensorProduct.mk R P (Dual R M ⊗[R] Q))
                              (lTensorHomToHomLTensor (RingHom.id R) M P Q ∘ₗ
                                (↑e : P ⊗[R] (Dual R M ⊗[R] Q) →ₗ[R] P ⊗[R] (M →ₗ[R] Q))) :
                            (a : P) → Dual R M ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                          f) :
                      (a : Dual R M) → Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                    q :
                  Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
                (a : Q) → M →ₗ[R] P ⊗[R] Q)
              m :
            M →ₗ[R] P ⊗[R] Q) :
          (a : M) → P ⊗[R] Q)
        x :
      P ⊗[R] Q)

Tactic:
simp only [e, lTensorHomEquivHomLTensor, dualTensorHomEquiv, LinearEquiv.comp_coe, compr₂ₛₗ_apply,
    mk_apply, LinearEquiv.coe_coe, LinearEquiv.trans_apply, congr_tmul, LinearEquiv.refl_apply,
    dualTensorHomEquivOfBasis_apply, dualTensorHomEquivOfBasis_symm_cancel_left, leftComm_tmul,
    dualTensorHom_apply, coe_comp, Function.comp_apply, lTensorHomToHomLTensor_apply, tmul_smul]

Premises used: dualTensorHomEquiv, TensorProduct.leftComm_tmul, TensorProduct.mk_apply, dualTensorHom_apply, TensorProduct.tmul_smul, TensorProduct.congr_tmul, LinearEquiv.trans_apply, TensorProduct.lTensorHomToHomLTensor_apply, lTensorHomEquivHomLTensor, LinearEquiv.comp_coe, LinearMap.coe_comp, LinearEquiv.refl_apply, dualTensorHomEquivOfBasis_symm_cancel_left, Function.comp_apply, LinearMap.compr₂ₛₗ_apply, dualTensorHomEquivOfBasis_apply, LinearEquiv.coe_coe
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
e : Dual R M ⊗[R] P ⊗[R] Q ≃ₗ[R] (M →ₗ[R] P) ⊗[R] Q :=
  TensorProduct.congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)
⊢ Function.Surjective (α := Dual R M ⊗[R] P ⊗[R] Q) (β := (M →ₗ[R] P) ⊗[R] Q)
    (⇑(↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q) : (a : Dual R M ⊗[R] P ⊗[R] Q) → (M →ₗ[R] P) ⊗[R] Q)

Tactic:
have h : Function.Surjective e.toLinearMap := e.surjective
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
e : Dual R M ⊗[R] P ⊗[R] Q ≃ₗ[R] (M →ₗ[R] P) ⊗[R] Q :=
  TensorProduct.congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)
h :
  Function.Surjective (α := Dual R M ⊗[R] P ⊗[R] Q) (β := (M →ₗ[R] P) ⊗[R] Q)
    (⇑(↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q) : (a : Dual R M ⊗[R] P ⊗[R] Q) → (M →ₗ[R] P) ⊗[R] Q)
⊢ Eq (α := (M →ₗ[R] P) ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
    (↑(rTensorHomEquivHomRTensor R M P Q) : (M →ₗ[R] P) ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
    (rTensorHomToHomRTensor (RingHom.id R) M P Q)

Tactic:
(cancel_right h).1 ?_

Premises used: LinearMap.cancel_right, Iff.mp
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
e : Dual R M ⊗[R] P ⊗[R] Q ≃ₗ[R] (M →ₗ[R] P) ⊗[R] Q :=
  TensorProduct.congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)
h :
  Function.Surjective (α := Dual R M ⊗[R] P ⊗[R] Q) (β := (M →ₗ[R] P) ⊗[R] Q)
    (⇑(↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q) : (a : Dual R M ⊗[R] P ⊗[R] Q) → (M →ₗ[R] P) ⊗[R] Q)
refine :
  (↑(rTensorHomEquivHomRTensor R M P Q) : (M →ₗ[R] P) ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) ∘ₗ
      (↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q) =
    rTensorHomToHomRTensor (RingHom.id R) M P Q ∘ₗ (↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q)
⊢ Eq (α := (M →ₗ[R] P) ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
    (↑(rTensorHomEquivHomRTensor R M P Q) : (M →ₗ[R] P) ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
    (rTensorHomToHomRTensor (RingHom.id R) M P Q)

Tactic:
refine (cancel_right h).1 ?_

Premises used: LinearMap.cancel_right, Iff.mp
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
e : Dual R M ⊗[R] P ⊗[R] Q ≃ₗ[R] (M →ₗ[R] P) ⊗[R] Q :=
  TensorProduct.congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)
h :
  Function.Surjective (α := Dual R M ⊗[R] P ⊗[R] Q) (β := (M →ₗ[R] P) ⊗[R] Q)
    (⇑(↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q) : (a : Dual R M ⊗[R] P ⊗[R] Q) → (M →ₗ[R] P) ⊗[R] Q)
H :
  ∀ (f : Dual R M) (p : P) (q : Q) (m : M),
    Eq (α := P ⊗[R] Q)
      ((((((((compr₂ₛₗ (TensorProduct.mk R (Dual R M) P)
                                (compr₂ₛₗ (TensorProduct.mk R (Dual R M ⊗[R] P) Q)
                                  ((↑(rTensorHomEquivHomRTensor R M P Q) : (M →ₗ[R] P) ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) ∘ₗ
                                    (↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q))) :
                              (a : Dual R M) → P →ₗ[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                            f :
                          P →ₗ[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
                        (a : P) → Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                      p :
                    Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
                  (a : Q) → M →ₗ[R] P ⊗[R] Q)
                q :
              M →ₗ[R] P ⊗[R] Q) :
            (a : M) → P ⊗[R] Q)
          m :
        P ⊗[R] Q)
      ((((((((compr₂ₛₗ (TensorProduct.mk R (Dual R M) P)
                                (compr₂ₛₗ (TensorProduct.mk R (Dual R M ⊗[R] P) Q)
                                  (rTensorHomToHomRTensor (RingHom.id R) M P Q ∘ₗ
                                    (↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q))) :
                              (a : Dual R M) → P →ₗ[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                            f :
                          P →ₗ[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
                        (a : P) → Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                      p :
                    Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
                  (a : Q) → M →ₗ[R] P ⊗[R] Q)
                q :
              M →ₗ[R] P ⊗[R] Q) :
            (a : M) → P ⊗[R] Q)
          m :
        P ⊗[R] Q)
⊢ (↑(rTensorHomEquivHomRTensor R M P Q) : (M →ₗ[R] P) ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) ∘ₗ
      (↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q) =
    rTensorHomToHomRTensor (RingHom.id R) M P Q ∘ₗ (↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q)

Tactic:
ext f p q m
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
e : Dual R M ⊗[R] P ⊗[R] Q ≃ₗ[R] (M →ₗ[R] P) ⊗[R] Q :=
  TensorProduct.congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)
h :
  Function.Surjective (α := Dual R M ⊗[R] P ⊗[R] Q) (β := (M →ₗ[R] P) ⊗[R] Q)
    (⇑(↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q) : (a : Dual R M ⊗[R] P ⊗[R] Q) → (M →ₗ[R] P) ⊗[R] Q)
f : Dual R M
p : P
q : Q
m : M
⊢ Eq (α := P ⊗[R] Q)
    ((((((((compr₂ₛₗ (TensorProduct.mk R (Dual R M) P)
                              (compr₂ₛₗ (TensorProduct.mk R (Dual R M ⊗[R] P) Q)
                                ((↑(rTensorHomEquivHomRTensor R M P Q) : (M →ₗ[R] P) ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) ∘ₗ
                                  (↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q))) :
                            (a : Dual R M) → P →ₗ[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                          f :
                        P →ₗ[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
                      (a : P) → Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                    p :
                  Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
                (a : Q) → M →ₗ[R] P ⊗[R] Q)
              q :
            M →ₗ[R] P ⊗[R] Q) :
          (a : M) → P ⊗[R] Q)
        m :
      P ⊗[R] Q)
    ((((((((compr₂ₛₗ (TensorProduct.mk R (Dual R M) P)
                              (compr₂ₛₗ (TensorProduct.mk R (Dual R M ⊗[R] P) Q)
                                (rTensorHomToHomRTensor (RingHom.id R) M P Q ∘ₗ
                                  (↑e : Dual R M ⊗[R] P ⊗[R] Q →ₗ[R] (M →ₗ[R] P) ⊗[R] Q))) :
                            (a : Dual R M) → P →ₗ[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                          f :
                        P →ₗ[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
                      (a : P) → Q →ₗ[R] M →ₗ[R] P ⊗[R] Q)
                    p :
                  Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
                (a : Q) → M →ₗ[R] P ⊗[R] Q)
              q :
            M →ₗ[R] P ⊗[R] Q) :
          (a : M) → P ⊗[R] Q)
        m :
      P ⊗[R] Q)

Tactic:
simp only [e, rTensorHomEquivHomRTensor, dualTensorHomEquiv, compr₂ₛₗ_apply, mk_apply, coe_comp,
    LinearEquiv.coe_toLinearMap, Function.comp_apply,
    dualTensorHomEquivOfBasis_apply, LinearEquiv.trans_apply, congr_tmul,
    dualTensorHomEquivOfBasis_symm_cancel_left, LinearEquiv.refl_apply, assoc_tmul,
    dualTensorHom_apply, rTensorHomToHomRTensor_apply, smul_tmul']

Premises used: dualTensorHomEquiv, TensorProduct.mk_apply, dualTensorHom_apply, TensorProduct.assoc_tmul, rTensorHomEquivHomRTensor, TensorProduct.congr_tmul, LinearEquiv.trans_apply, TensorProduct.smul_tmul', LinearMap.coe_comp, LinearEquiv.refl_apply, dualTensorHomEquivOfBasis_symm_cancel_left, LinearEquiv.coe_toLinearMap, Function.comp_apply, TensorProduct.rTensorHomToHomRTensor_apply, LinearMap.compr₂ₛₗ_apply, dualTensorHomEquivOfBasis_apply
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
x : P ⊗[R] (M →ₗ[R] Q)
rw :
  Eq (α := M →ₗ[R] P ⊗[R] Q)
    (((↑(lTensorHomEquivHomLTensor R M P Q) : P ⊗[R] (M →ₗ[R] Q) →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
          (a : P ⊗[R] (M →ₗ[R] Q)) → M →ₗ[R] P ⊗[R] Q)
        x :
      M →ₗ[R] P ⊗[R] Q)
    ((lTensorHomToHomLTensor (RingHom.id R) M P Q : (a : P ⊗[R] (M →ₗ[R] Q)) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
rw₁ rw₂ :
  Eq (α := M →ₗ[R] P ⊗[R] Q)
    ((lTensorHomToHomLTensor (RingHom.id R) M P Q : (a : P ⊗[R] (M →ₗ[R] Q)) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
    ((lTensorHomToHomLTensor (RingHom.id R) M P Q : (a : P ⊗[R] (M →ₗ[R] Q)) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
⊢ Eq (α := M →ₗ[R] P ⊗[R] Q)
    ((lTensorHomEquivHomLTensor R M P Q : (a : P ⊗[R] (M →ₗ[R] Q)) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
    ((lTensorHomToHomLTensor (RingHom.id R) M P Q : (a : P ⊗[R] (M →ₗ[R] Q)) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)

Tactic:
rw [← LinearEquiv.coe_toLinearMap, lTensorHomEquivHomLTensor_toLinearMap]

Premises used: lTensorHomEquivHomLTensor_toLinearMap, LinearEquiv.coe_toLinearMap
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : AddCommMonoid Q
inst_4 : Module R M
inst_5 : Module R P
inst_6 : Module R Q
inst_7 : Free R M
inst_8 : Module.Finite R M
x : (M →ₗ[R] P) ⊗[R] Q
rw :
  Eq (α := M →ₗ[R] P ⊗[R] Q)
    (((↑(rTensorHomEquivHomRTensor R M P Q) : (M →ₗ[R] P) ⊗[R] Q →ₗ[R] M →ₗ[R] P ⊗[R] Q) :
          (a : (M →ₗ[R] P) ⊗[R] Q) → M →ₗ[R] P ⊗[R] Q)
        x :
      M →ₗ[R] P ⊗[R] Q)
    ((rTensorHomToHomRTensor (RingHom.id R) M P Q : (a : (M →ₗ[R] P) ⊗[R] Q) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
rw₁ rw₂ :
  Eq (α := M →ₗ[R] P ⊗[R] Q)
    ((rTensorHomToHomRTensor (RingHom.id R) M P Q : (a : (M →ₗ[R] P) ⊗[R] Q) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
    ((rTensorHomToHomRTensor (RingHom.id R) M P Q : (a : (M →ₗ[R] P) ⊗[R] Q) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
⊢ Eq (α := M →ₗ[R] P ⊗[R] Q)
    ((rTensorHomEquivHomRTensor R M P Q : (a : (M →ₗ[R] P) ⊗[R] Q) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)
    ((rTensorHomToHomRTensor (RingHom.id R) M P Q : (a : (M →ₗ[R] P) ⊗[R] Q) → M →ₗ[R] P ⊗[R] Q) x : M →ₗ[R] P ⊗[R] Q)

Tactic:
rw [← LinearEquiv.coe_toLinearMap, rTensorHomEquivHomRTensor_toLinearMap]

Premises used: rTensorHomEquivHomRTensor_toLinearMap, LinearEquiv.coe_toLinearMap
-- Module: Mathlib.LinearAlgebra.Contraction
Goal:
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
Q : Type u_6
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid Q
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R Q
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : Free R N
inst_12 : Module.Finite R N
H :
  ∀ (m : M →ₗ[R] P) (n : N →ₗ[R] Q) (x : M) (x_1 : N),
    Eq (α := P ⊗[R] Q)
      ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (TensorProduct.mk R M N)
                    ((((compr₂ₛₗ (TensorProduct.mk R (M →ₗ[R] P) (N →ₗ[R] Q))
                                (↑(homTensorHomEquiv R M N P Q) :
                                  (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q) :
                              (a : M →ₗ[R] P) → (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q)
                            m :
                          (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q) :
                        (a : N →ₗ[R] Q) → M ⊗[R] N →ₗ[R] P ⊗[R] Q)
                      n) :
                  (a : M) → N →ₗ[R] P ⊗[R] Q)
                x :
              N →ₗ[R] P ⊗[R] Q) :
            (a : N) → P ⊗[R] Q)
          x_1 :
        P ⊗[R] Q)
      ((((compr₂ₛₗ (σ₃₄ := RingHom.id R) (TensorProduct.mk R M N)
                    ((((compr₂ₛₗ (TensorProduct.mk R (M →ₗ[R] P) (N →ₗ[R] Q)) (homTensorHomMap (RingHom.id R) M N P Q) :
                              (a : M →ₗ[R] P) → (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q)
                            m :
                          (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q) :
                        (a : N →ₗ[R] Q) → M ⊗[R] N →ₗ[R] P ⊗[R] Q)
                      n) :
                  (a : M) → N →ₗ[R] P ⊗[R] Q)
                x :
              N →ₗ[R] P ⊗[R] Q) :
            (a : N) → P ⊗[R] Q)
          x_1 :
        P ⊗[R] Q)
⊢ Eq (α := (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q)
    (↑(homTensorHomEquiv R M N P Q) : (M →ₗ[R] P) ⊗[R] (N →ₗ[R] Q) →ₗ[R] M ⊗[R] N →ₗ[R] P ⊗[R] Q)
    (homTensorHomMap (RingHom.id R) M N P Q)

Tactic:
ext m n