case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom) =
    LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) ((leftUnitor M).hom ≫ f)
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom = (leftUnitor M).hom ≫ f
apply TensorProduct.ext
case H.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ ↑(LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) 1 =
    ↑(LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) ((leftUnitor M).hom ≫ f)) 1
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom) =
    LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) ((leftUnitor M).hom ≫ f)
apply LinearMap.ext_ring
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ ∀ (x : ↑M),
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) 1) x =
      ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) ((leftUnitor M).hom ≫ f)) 1) x
case H.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
⊢ ↑(LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) 1 =
    ↑(LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) ((leftUnitor M).hom ≫ f)) 1
apply LinearMap.ext
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) 1) x =
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) ((leftUnitor M).hom ≫ f)) 1) 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 ↑(of R R) ↑M) (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) 1) x =
      ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) ((leftUnitor M).hom ≫ f)) 1) x
intro x
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(leftUnitor N).hom (↑(tensorHom (𝟙 (of R R)) f) (1 ⊗ₜ[R] x)) = ↑f (↑(leftUnitor M).hom (1 ⊗ₜ[R] 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 ↑(of R R) ↑M) (tensorHom (𝟙 (of R R)) f ≫ (leftUnitor N).hom)) 1) x =
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑(of R R) ↑M) ((leftUnitor M).hom ≫ f)) 1) x
change ((leftUnitor N).hom) ((tensorHom (𝟙 (of R R)) f) ((1 : R) ⊗ₜ[R] x)) =
  f (((leftUnitor M).hom) (1 ⊗ₜ[R] x))
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(𝟙 (of R R)) (1, x).fst • ↑f (1, x).snd = ↑f (1 • x)
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(leftUnitor N).hom (↑(tensorHom (𝟙 (of R R)) f) (1 ⊗ₜ[R] x)) = ↑f (↑(leftUnitor M).hom (1 ⊗ₜ[R] x))
erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul]
case H.h.h
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
f : M ⟶ N
x : ↑M
⊢ ↑(𝟙 (of R R)) (1, x).fst • ↑f (1, x).snd = 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)) (1, x).fst • ↑f (1, x).snd = ↑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)) (1, x).fst • ↑f (1, x).snd = 1 • ↑f x
rfl