-- Mathlib/LinearAlgebra/Contraction.lean
theorem lTensorHomEquivHomLTensor_toLinearMap :
    (lTensorHomEquivHomLTensor R M P Q).toLinearMap = lTensorHomToHomLTensor 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 : P ⊗[R] Dual R M ⊗[R] Q ≃ₗ[R] P ⊗[R] (M →ₗ[R] Q) :=
  TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
⊢ ↑(lTensorHomEquivHomLTensor R M P Q) = lTensorHomToHomLTensor 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 : 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 ⇑↑e
⊢ ↑(lTensorHomEquivHomLTensor R M P Q) = lTensorHomToHomLTensor 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 : 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 ⇑↑e
⊢ ↑(lTensorHomEquivHomLTensor R M P Q) = lTensorHomToHomLTensor 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 : 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 ⇑↑e
⊢ ↑(lTensorHomEquivHomLTensor R M P Q) ∘ₗ ↑e = lTensorHomToHomLTensor 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
⊢ ↑(lTensorHomEquivHomLTensor R M P Q) = lTensorHomToHomLTensor R M P Q

Tactic:
let e := congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M 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 : P ⊗[R] Dual R M ⊗[R] Q ≃ₗ[R] P ⊗[R] (M →ₗ[R] Q) :=
  TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q)
⊢ ↑(lTensorHomEquivHomLTensor R M P Q) = lTensorHomToHomLTensor 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 : 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 ⇑↑e
⊢ ↑(lTensorHomEquivHomLTensor R M P Q) ∘ₗ ↑e = lTensorHomToHomLTensor R M P Q ∘ₗ ↑e

Tactic:
ext f 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 : 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 ⇑↑e
f : P
q : Dual R M
m : Q
x✝ : M
⊢ ((((TensorProduct.mk R (Dual R M) Q).compr₂
            (((TensorProduct.mk R P (Dual R M ⊗[R] Q)).compr₂ (↑(lTensorHomEquivHomLTensor R M P Q) ∘ₗ ↑e)) f))
          q)
        m)
      x✝ =
    ((((TensorProduct.mk R (Dual R M) Q).compr₂
            (((TensorProduct.mk R P (Dual R M ⊗[R] Q)).compr₂ (lTensorHomToHomLTensor R M P Q ∘ₗ ↑e)) f))
          q)
        m)
      x✝

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 : 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 ⇑↑e
f : P
q : Dual R M
m : Q
x✝ : M
⊢ ((((TensorProduct.mk R (Dual R M) Q).compr₂
            (((TensorProduct.mk R P (Dual R M ⊗[R] Q)).compr₂ (↑(lTensorHomEquivHomLTensor R M P Q) ∘ₗ ↑e)) f))
          q)
        m)
      x✝ =
    ((((TensorProduct.mk R (Dual R M) Q).compr₂
            (((TensorProduct.mk R P (Dual R M ⊗[R] Q)).compr₂ (lTensorHomToHomLTensor R M P Q ∘ₗ ↑e)) f))
          q)
        m)
      x✝

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]

Result:
no goals