[GOAL]
R : Type u
inst✝ : CommRing R
M N P : ModuleCat R
f : (MonoidalCategory.tensorLeft M).obj N ⟶ P
⊢ (fun f => (β_ M N).hom ≫ TensorProduct.lift f)
      ((fun f => LinearMap.compr₂ (TensorProduct.mk R ↑N ↑M) ((β_ N M).hom ≫ f)) f) =
    f
[PROOFSTEP]
apply TensorProduct.ext'
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M N P : ModuleCat R
f : (MonoidalCategory.tensorLeft M).obj N ⟶ P
⊢ ∀ (x : ↑M) (y : ↑N),
    ↑((fun f => (β_ M N).hom ≫ TensorProduct.lift f)
            ((fun f => LinearMap.compr₂ (TensorProduct.mk R ↑N ↑M) ((β_ N M).hom ≫ f)) f))
        (x ⊗ₜ[R] y) =
      ↑f (x ⊗ₜ[R] y)
[PROOFSTEP]
intro m n
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M N P : ModuleCat R
f : (MonoidalCategory.tensorLeft M).obj N ⟶ P
m : ↑M
n : ↑N
⊢ ↑((fun f => (β_ M N).hom ≫ TensorProduct.lift f)
          ((fun f => LinearMap.compr₂ (TensorProduct.mk R ↑N ↑M) ((β_ N M).hom ≫ f)) f))
      (m ⊗ₜ[R] n) =
    ↑f (m ⊗ₜ[R] n)
[PROOFSTEP]
rw [coe_comp, Function.comp_apply, MonoidalCategory.braiding_hom_apply, TensorProduct.lift.tmul, LinearMap.compr₂_apply,
  TensorProduct.mk_apply, coe_comp, Function.comp_apply, MonoidalCategory.braiding_hom_apply]
[GOAL]
R : Type u
inst✝ : CommRing R
M : ModuleCat R
⊢ ∀ {X' X Y : ModuleCat R} (f : X' ⟶ X) (g : X ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y),
    ↑((fun N P => monoidalClosedHomEquiv M N P) X' Y).symm (f ≫ g) =
      (MonoidalCategory.tensorLeft M).map f ≫ ↑((fun N P => monoidalClosedHomEquiv M N P) X Y).symm g
[PROOFSTEP]
intros
[GOAL]
R : Type u
inst✝ : CommRing R
M X'✝ X✝ Y✝ : ModuleCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y✝
⊢ ↑((fun N P => monoidalClosedHomEquiv M N P) X'✝ Y✝).symm (f✝ ≫ g✝) =
    (MonoidalCategory.tensorLeft M).map f✝ ≫ ↑((fun N P => monoidalClosedHomEquiv M N P) X✝ Y✝).symm g✝
[PROOFSTEP]
apply TensorProduct.ext'
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M X'✝ X✝ Y✝ : ModuleCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y✝
⊢ ∀ (x : ↑M) (y : ↑X'✝),
    ↑(↑((fun N P => monoidalClosedHomEquiv M N P) X'✝ Y✝).symm (f✝ ≫ g✝)) (x ⊗ₜ[R] y) =
      ↑((MonoidalCategory.tensorLeft M).map f✝ ≫ ↑((fun N P => monoidalClosedHomEquiv M N P) X✝ Y✝).symm g✝) (x ⊗ₜ[R] y)
[PROOFSTEP]
intro m n
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M X'✝ X✝ Y✝ : ModuleCat R
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ ((linearCoyoneda R (ModuleCat R)).obj (op M)).obj Y✝
m : ↑M
n : ↑X'✝
⊢ ↑(↑((fun N P => monoidalClosedHomEquiv M N P) X'✝ Y✝).symm (f✝ ≫ g✝)) (m ⊗ₜ[R] n) =
    ↑((MonoidalCategory.tensorLeft M).map f✝ ≫ ↑((fun N P => monoidalClosedHomEquiv M N P) X✝ Y✝).symm g✝) (m ⊗ₜ[R] n)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ NatTrans.app (ihom.ev M) N = ↑(TensorProduct.uncurry R (↑M) (↑M →ₗ[R] ↑N) ↑N) (LinearMap.flip LinearMap.id)
[PROOFSTEP]
apply TensorProduct.ext'
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ ∀ (x : ↑M) (y : ↑((ihom M).obj N)),
    ↑(NatTrans.app (ihom.ev M) N) (x ⊗ₜ[R] y) =
      ↑(↑(TensorProduct.uncurry R (↑M) (↑M →ₗ[R] ↑N) ↑N) (LinearMap.flip LinearMap.id)) (x ⊗ₜ[R] y)
[PROOFSTEP]
apply ModuleCat.monoidalClosed_uncurry
