-- Mathlib/LinearAlgebra/Contraction.lean
theorem rTensorHomEquivHomRTensor_toLinearMap :
    (rTensorHomEquivHomRTensor R M P Q).toLinearMap = rTensorHomToHomRTensor R M P Q

Proof state:
R : Type u
M : Type v₁
P : Type v₃
Q : Type v₄
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ ↑(rTensorHomEquivHomRTensor R M P Q) = rTensorHomToHomRTensor R M P Q

Tactic:
let e := congr (dualTensorHomEquiv R M P) (LinearEquiv.refl R Q)

Result:
R : Type u
M : Type v₁
P : Type v₃
Q : Type v₄
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Free R M
inst✝ : 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)
⊢ ↑(rTensorHomEquivHomRTensor R M P Q) = rTensorHomToHomRTensor R M P Q

Proof state:
R : Type u
M : Type v₁
P : Type v₃
Q : Type v₄
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Free R M
inst✝ : 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 ⇑↑e
⊢ ↑(rTensorHomEquivHomRTensor R M P Q) = rTensorHomToHomRTensor R M P Q

Tactic:
refine (cancel_right h).1 ?_

Result:
R : Type u
M : Type v₁
P : Type v₃
Q : Type v₄
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Free R M
inst✝ : 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 ⇑↑e
⊢ ↑(rTensorHomEquivHomRTensor R M P Q) ∘ₗ ↑e = rTensorHomToHomRTensor R M P Q ∘ₗ ↑e

Proof state:
R : Type u
M : Type v₁
P : Type v₃
Q : Type v₄
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Free R M
inst✝ : 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 ⇑↑e
⊢ ↑(rTensorHomEquivHomRTensor R M P Q) ∘ₗ ↑e = rTensorHomToHomRTensor R M P Q ∘ₗ ↑e

Tactic:
ext f p q m

Result:
case H.H.h.h.h.h
R : Type u
M : Type v₁
P : Type v₃
Q : Type v₄
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Free R M
inst✝ : 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 ⇑↑e
f : Dual R M
p : P
q : Q
m : M
⊢ (((((TensorProduct.mk R (Dual R M) P).compr₂
              ((TensorProduct.mk R (Dual R M ⊗[R] P) Q).compr₂ (↑(rTensorHomEquivHomRTensor R M P Q) ∘ₗ ↑e)))
            f)
          p)
        q)
      m =
    (((((TensorProduct.mk R (Dual R M) P).compr₂
              ((TensorProduct.mk R (Dual R M ⊗[R] P) Q).compr₂ (rTensorHomToHomRTensor R M P Q ∘ₗ ↑e)))
            f)
          p)
        q)
      m

Proof state:
R : Type u
M : Type v₁
P : Type v₃
Q : Type v₄
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Free R M
inst✝ : 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)
⊢ ↑(rTensorHomEquivHomRTensor R M P Q) = rTensorHomToHomRTensor R M P Q

Tactic:
have h : Function.Surjective e.toLinearMap := e.surjective

Result:
R : Type u
M : Type v₁
P : Type v₃
Q : Type v₄
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Free R M
inst✝ : 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 ⇑↑e
⊢ ↑(rTensorHomEquivHomRTensor R M P Q) = rTensorHomToHomRTensor R M P Q

Proof state:
case H.H.h.h.h.h
R : Type u
M : Type v₁
P : Type v₃
Q : Type v₄
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R Q
inst✝¹ : Free R M
inst✝ : 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 ⇑↑e
f : Dual R M
p : P
q : Q
m : M
⊢ (((((TensorProduct.mk R (Dual R M) P).compr₂
              ((TensorProduct.mk R (Dual R M ⊗[R] P) Q).compr₂ (↑(rTensorHomEquivHomRTensor R M P Q) ∘ₗ ↑e)))
            f)
          p)
        q)
      m =
    (((((TensorProduct.mk R (Dual R M) P).compr₂
              ((TensorProduct.mk R (Dual R M ⊗[R] P) Q).compr₂ (rTensorHomToHomRTensor R M P Q ∘ₗ ↑e)))
            f)
          p)
        q)
      m

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

Result:
no goals