case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom) =
    LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) ((rightUnitor M).hom ≫ f)
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom = (rightUnitor M).hom ≫ f
apply TensorProduct.ext
case H.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ ∀ (x : ↑M),
    ↑(LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) x =
      ↑(LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) ((rightUnitor M).hom ≫ f)) x
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom) =
    LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) ((rightUnitor M).hom ≫ f)
apply LinearMap.ext
case H.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) x =
    ↑(LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) ((rightUnitor M).hom ≫ f)) x
case H.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ ∀ (x : ↑M),
    ↑(LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) x =
      ↑(LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) ((rightUnitor M).hom ≫ f)) x
intro x
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) x) 1 =
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) ((rightUnitor M).hom ≫ f)) x) 1
case H.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) x =
    ↑(LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) ((rightUnitor M).hom ≫ f)) x
apply LinearMap.ext_ring
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(rightUnitor N).hom (↑(tensorHom f (𝟙 (of R R))) (x ⊗ₜ[R] 1)) = ↑f (↑(rightUnitor M).hom (x ⊗ₜ[R] 1))
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) (tensorHom f (𝟙 (of R R)) ≫ (rightUnitor N).hom)) x) 1 =
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑M ↑(of R R)) ((rightUnitor M).hom ≫ f)) x) 1
change ((rightUnitor N).hom) ((tensorHom f (𝟙 (of R R))) (x ⊗ₜ[R] (1 : R))) =
  f (((rightUnitor M).hom) (x ⊗ₜ[R] 1))
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(𝟙 (of R R)) (x, 1).snd • ↑f (x, 1).fst = ↑f (1 • x)
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(rightUnitor N).hom (↑(tensorHom f (𝟙 (of R R))) (x ⊗ₜ[R] 1)) = ↑f (↑(rightUnitor M).hom (x ⊗ₜ[R] 1))
erw [TensorProduct.rid_tmul, TensorProduct.rid_tmul]
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(𝟙 (of R R)) (x, 1).snd • ↑f (x, 1).fst = 1 • ↑f x
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(𝟙 (of R R)) (x, 1).snd • ↑f (x, 1).fst = ↑f (1 • x)
rw [LinearMap.map_smul]
no goals
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(𝟙 (of R R)) (x, 1).snd • ↑f (x, 1).fst = 1 • ↑f x
rfl