[GOAL]
R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
⊢ tensorHom (𝟙 M) (𝟙 N) = 𝟙 (of R (↑M ⊗[R] ↑N))
[PROOFSTEP]
apply TensorProduct.ext
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M : ModuleCat R
N : ModuleCat R
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑M ↑N) (tensorHom (𝟙 M) (𝟙 N)) =
    LinearMap.compr₂ (TensorProduct.mk R ↑M ↑N) (𝟙 (of R (↑M ⊗[R] ↑N)))
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ Y₁ Z₁ : ModuleCat R
X₂ Y₂ Z₂ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂
[PROOFSTEP]
apply TensorProduct.ext
[GOAL]
case H
R : Type u
inst✝ : CommRing R
X₁ Y₁ Z₁ : ModuleCat R
X₂ Y₂ Z₂ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ LinearMap.compr₂ (TensorProduct.mk R ↑X₁ ↑X₂) (tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂)) =
    LinearMap.compr₂ (TensorProduct.mk R ↑X₁ ↑X₂) (tensorHom f₁ f₂ ≫ tensorHom g₁ g₂)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹² : CommRing R
X₁ : Type u_1
X₂ : Type u_2
X₃ : Type u_3
inst✝¹¹ : AddCommMonoid X₁
inst✝¹⁰ : AddCommMonoid X₂
inst✝⁹ : AddCommMonoid X₃
inst✝⁸ : Module R X₁
inst✝⁷ : Module R X₂
inst✝⁶ : Module R X₃
Y₁ : Type u_4
Y₂ : Type u_5
Y₃ : Type u_6
inst✝⁵ : AddCommMonoid Y₁
inst✝⁴ : AddCommMonoid Y₂
inst✝³ : AddCommMonoid Y₃
inst✝² : Module R Y₁
inst✝¹ : Module R Y₂
inst✝ : Module R Y₃
f₁ : X₁ →ₗ[R] Y₁
f₂ : X₂ →ₗ[R] Y₂
f₃ : X₃ →ₗ[R] Y₃
⊢ LinearMap.comp (↑(assoc R Y₁ Y₂ Y₃)) (map (map f₁ f₂) f₃) = LinearMap.comp (map f₁ (map f₂ f₃)) ↑(assoc R X₁ X₂ X₃)
[PROOFSTEP]
apply TensorProduct.ext_threefold
[GOAL]
case H
R : Type u
inst✝¹² : CommRing R
X₁ : Type u_1
X₂ : Type u_2
X₃ : Type u_3
inst✝¹¹ : AddCommMonoid X₁
inst✝¹⁰ : AddCommMonoid X₂
inst✝⁹ : AddCommMonoid X₃
inst✝⁸ : Module R X₁
inst✝⁷ : Module R X₂
inst✝⁶ : Module R X₃
Y₁ : Type u_4
Y₂ : Type u_5
Y₃ : Type u_6
inst✝⁵ : AddCommMonoid Y₁
inst✝⁴ : AddCommMonoid Y₂
inst✝³ : AddCommMonoid Y₃
inst✝² : Module R Y₁
inst✝¹ : Module R Y₂
inst✝ : Module R Y₃
f₁ : X₁ →ₗ[R] Y₁
f₂ : X₂ →ₗ[R] Y₂
f₃ : X₃ →ₗ[R] Y₃
⊢ ∀ (x : X₁) (y : X₂) (z : X₃),
    ↑(LinearMap.comp (↑(assoc R Y₁ Y₂ Y₃)) (map (map f₁ f₂) f₃)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      ↑(LinearMap.comp (map f₁ (map f₂ f₃)) ↑(assoc R X₁ X₂ X₃)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
[PROOFSTEP]
intro x y z
[GOAL]
case H
R : Type u
inst✝¹² : CommRing R
X₁ : Type u_1
X₂ : Type u_2
X₃ : Type u_3
inst✝¹¹ : AddCommMonoid X₁
inst✝¹⁰ : AddCommMonoid X₂
inst✝⁹ : AddCommMonoid X₃
inst✝⁸ : Module R X₁
inst✝⁷ : Module R X₂
inst✝⁶ : Module R X₃
Y₁ : Type u_4
Y₂ : Type u_5
Y₃ : Type u_6
inst✝⁵ : AddCommMonoid Y₁
inst✝⁴ : AddCommMonoid Y₂
inst✝³ : AddCommMonoid Y₃
inst✝² : Module R Y₁
inst✝¹ : Module R Y₂
inst✝ : Module R Y₃
f₁ : X₁ →ₗ[R] Y₁
f₂ : X₂ →ₗ[R] Y₂
f₃ : X₃ →ₗ[R] Y₃
x : X₁
y : X₂
z : X₃
⊢ ↑(LinearMap.comp (↑(assoc R Y₁ Y₂ Y₃)) (map (map f₁ f₂) f₃)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(LinearMap.comp (map f₁ (map f₂ f₃)) ↑(assoc R X₁ X₂ X₃)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
[PROOFSTEP]
rfl
  -- Porting note: private so hopeful never used outside this file
  -- #align Module.monoidal_category.associator_naturality_aux ModuleCat.MonoidalCategory.associator_naturality_aux
[GOAL]
R : Type u
inst✝⁸ : CommRing R
W : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁷ : AddCommMonoid W
inst✝⁶ : AddCommMonoid X
inst✝⁵ : AddCommMonoid Y
inst✝⁴ : AddCommMonoid Z
inst✝³ : Module R W
inst✝² : Module R X
inst✝¹ : Module R Y
inst✝ : Module R Z
⊢ LinearMap.comp (LinearMap.comp (map 1 ↑(assoc R X Y Z)) ↑(assoc R W (X ⊗[R] Y) Z)) (map (↑(assoc R W X Y)) 1) =
    LinearMap.comp ↑(assoc R W X (Y ⊗[R] Z)) ↑(assoc R (W ⊗[R] X) Y Z)
[PROOFSTEP]
apply TensorProduct.ext_fourfold
[GOAL]
case H
R : Type u
inst✝⁸ : CommRing R
W : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁷ : AddCommMonoid W
inst✝⁶ : AddCommMonoid X
inst✝⁵ : AddCommMonoid Y
inst✝⁴ : AddCommMonoid Z
inst✝³ : Module R W
inst✝² : Module R X
inst✝¹ : Module R Y
inst✝ : Module R Z
⊢ ∀ (w : W) (x : X) (y : Y) (z : Z),
    ↑(LinearMap.comp (LinearMap.comp (map 1 ↑(assoc R X Y Z)) ↑(assoc R W (X ⊗[R] Y) Z)) (map (↑(assoc R W X Y)) 1))
        (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) =
      ↑(LinearMap.comp ↑(assoc R W X (Y ⊗[R] Z)) ↑(assoc R (W ⊗[R] X) Y Z)) (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)
[PROOFSTEP]
intro w x y z
[GOAL]
case H
R : Type u
inst✝⁸ : CommRing R
W : Type u_1
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝⁷ : AddCommMonoid W
inst✝⁶ : AddCommMonoid X
inst✝⁵ : AddCommMonoid Y
inst✝⁴ : AddCommMonoid Z
inst✝³ : Module R W
inst✝² : Module R X
inst✝¹ : Module R Y
inst✝ : Module R Z
w : W
x : X
y : Y
z : Z
⊢ ↑(LinearMap.comp (LinearMap.comp (map 1 ↑(assoc R X Y Z)) ↑(assoc R W (X ⊗[R] Y) Z)) (map (↑(assoc R W X Y)) 1))
      (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(LinearMap.comp ↑(assoc R W X (Y ⊗[R] Z)) ↑(assoc R (W ⊗[R] X) Y Z)) (((w ⊗ₜ[R] x) ⊗ₜ[R] y) ⊗ₜ[R] z)
[PROOFSTEP]
rfl
  -- Porting note: private so hopeful never used outside this file
  -- #align Module.monoidal_category.pentagon_aux Module.monoidal_category.pentagon_aux
[GOAL]
R : Type u
inst✝ : CommRing R
X₁ : ModuleCat R
X₂ : ModuleCat R
X₃ : ModuleCat R
Y₁ : ModuleCat R
Y₂ : ModuleCat R
Y₃ : ModuleCat R
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
    (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃)
[PROOFSTEP]
convert associator_naturality_aux f₁ f₂ f₃ using 1
[GOAL]
R : Type u
inst✝ : CommRing R
W : ModuleCat R
X : ModuleCat R
Y : ModuleCat R
Z : ModuleCat R
⊢ tensorHom (associator W X Y).hom (𝟙 Z) ≫
      (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom =
    (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom
[PROOFSTEP]
convert pentagon_aux R W X Y Z using 1
[GOAL]
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
[PROOFSTEP]
apply TensorProduct.ext
[GOAL]
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)
[PROOFSTEP]
apply LinearMap.ext_ring
[GOAL]
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
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
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
[PROOFSTEP]
intro x
[GOAL]
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
[PROOFSTEP]
change ((leftUnitor N).hom) ((tensorHom (𝟙 (of R R)) f) ((1 : R) ⊗ₜ[R] x)) = f (((leftUnitor M).hom) (1 ⊗ₜ[R] x))
[GOAL]
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))
[PROOFSTEP]
erw [TensorProduct.lid_tmul, TensorProduct.lid_tmul]
[GOAL]
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)
[PROOFSTEP]
rw [LinearMap.map_smul]
[GOAL]
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
[PROOFSTEP]
rfl
[GOAL]
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
[PROOFSTEP]
apply TensorProduct.ext
[GOAL]
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)
[PROOFSTEP]
apply LinearMap.ext
[GOAL]
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
[PROOFSTEP]
intro x
[GOAL]
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
[PROOFSTEP]
apply LinearMap.ext_ring
[GOAL]
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
[PROOFSTEP]
change ((rightUnitor N).hom) ((tensorHom f (𝟙 (of R R))) (x ⊗ₜ[R] (1 : R))) = f (((rightUnitor M).hom) (x ⊗ₜ[R] 1))
[GOAL]
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))
[PROOFSTEP]
erw [TensorProduct.rid_tmul, TensorProduct.rid_tmul]
[GOAL]
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)
[PROOFSTEP]
rw [LinearMap.map_smul]
[GOAL]
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
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ (associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom = tensorHom (rightUnitor M).hom (𝟙 N)
[PROOFSTEP]
apply TensorProduct.ext_threefold
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
⊢ ∀ (x : ↑M) (y : ↑(of R R)) (z : ↑N),
    ↑((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
      ↑(tensorHom (rightUnitor M).hom (𝟙 N)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
[PROOFSTEP]
intro x y z
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
y : ↑(of R R)
z : ↑N
⊢ ↑((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(tensorHom (rightUnitor M).hom (𝟙 N)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
[PROOFSTEP]
change R at y 
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
z : ↑N
y : R
⊢ ↑((associator M (of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom) ((x ⊗ₜ[R] y) ⊗ₜ[R] z) =
    ↑(tensorHom (rightUnitor M).hom (𝟙 N)) ((x ⊗ₜ[R] y) ⊗ₜ[R] z)
[PROOFSTEP]
change x ⊗ₜ[R] ((leftUnitor N).hom) (y ⊗ₜ[R] z) = ((rightUnitor M).hom) (x ⊗ₜ[R] y) ⊗ₜ[R] z
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
z : ↑N
y : R
⊢ x ⊗ₜ[R] ↑(leftUnitor N).hom (y ⊗ₜ[R] z) = ↑(rightUnitor M).hom (x ⊗ₜ[R] y) ⊗ₜ[R] z
[PROOFSTEP]
erw [TensorProduct.lid_tmul, TensorProduct.rid_tmul]
[GOAL]
case H
R : Type u
inst✝ : CommRing R
M N : ModuleCat R
x : ↑M
z : ↑N
y : R
⊢ x ⊗ₜ[R] (y • z) = (y • x) ⊗ₜ[R] z
[PROOFSTEP]
exact (TensorProduct.smul_tmul _ _ _).symm
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ MonoidalPreadditive (ModuleCat R)
[PROOFSTEP]
refine' ⟨_, _, _, _⟩
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f : W ⟶ X), f ⊗ 0 = 0
[PROOFSTEP]
dsimp only [autoParam]
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f : W ⟶ X), f ⊗ 0 = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
⊢ f✝ ⊗ 0 = 0
[PROOFSTEP]
refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) (f✝ ⊗ 0)) x) y =
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) 0) x) y
[PROOFSTEP]
simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(f✝ ⊗ 0) (x ⊗ₜ[R] y) = ↑0 (x ⊗ₜ[R] y)
[PROOFSTEP]
rw [LinearMap.zero_apply, MonoidalCategory.hom_apply, LinearMap.zero_apply, TensorProduct.tmul_zero]
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f : Y ⟶ Z), 0 ⊗ f = 0
[PROOFSTEP]
dsimp only [autoParam]
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f : Y ⟶ Z), 0 ⊗ f = 0
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : Y✝ ⟶ Z✝
⊢ 0 ⊗ f✝ = 0
[PROOFSTEP]
refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) (0 ⊗ f✝)) x) y =
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) 0) x) y
[PROOFSTEP]
simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(0 ⊗ f✝) (x ⊗ₜ[R] y) = ↑0 (x ⊗ₜ[R] y)
[PROOFSTEP]
rw [LinearMap.zero_apply, MonoidalCategory.hom_apply, LinearMap.zero_apply, TensorProduct.zero_tmul]
[GOAL]
case refine'_3
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f : W ⟶ X) (g h : Y ⟶ Z), f ⊗ (g + h) = f ⊗ g + f ⊗ h
[PROOFSTEP]
dsimp only [autoParam]
[GOAL]
case refine'_3
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f : W ⟶ X) (g h : Y ⟶ Z), f ⊗ (g + h) = f ⊗ g + f ⊗ h
[PROOFSTEP]
intros
[GOAL]
case refine'_3
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
g✝ h✝ : Y✝ ⟶ Z✝
⊢ f✝ ⊗ (g✝ + h✝) = f✝ ⊗ g✝ + f✝ ⊗ h✝
[PROOFSTEP]
refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
[GOAL]
case refine'_3
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
g✝ h✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) (f✝ ⊗ (g✝ + h✝))) x) y =
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) (f✝ ⊗ g✝ + f✝ ⊗ h✝)) x) y
[PROOFSTEP]
simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
[GOAL]
case refine'_3
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
g✝ h✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(f✝ ⊗ (g✝ + h✝)) (x ⊗ₜ[R] y) = ↑(f✝ ⊗ g✝ + f✝ ⊗ h✝) (x ⊗ₜ[R] y)
[PROOFSTEP]
rw [LinearMap.add_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
[GOAL]
case refine'_3
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
g✝ h✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑f✝ x ⊗ₜ[R] ↑(g✝ + h✝) y = ↑f✝ x ⊗ₜ[R] ↑g✝ y + ↑(f✝ ⊗ h✝) (x ⊗ₜ[R] y)
[PROOFSTEP]
erw [MonoidalCategory.hom_apply]
[GOAL]
case refine'_3
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
g✝ h✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑f✝ x ⊗ₜ[R] ↑(g✝ + h✝) y = ↑f✝ x ⊗ₜ[R] ↑g✝ y + ↑f✝ x ⊗ₜ[R] ↑h✝ y
[PROOFSTEP]
rw [LinearMap.add_apply, TensorProduct.tmul_add]
[GOAL]
case refine'_4
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f g : W ⟶ X) (h : Y ⟶ Z), (f + g) ⊗ h = f ⊗ h + g ⊗ h
[PROOFSTEP]
dsimp only [autoParam]
[GOAL]
case refine'_4
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f g : W ⟶ X) (h : Y ⟶ Z), (f + g) ⊗ h = f ⊗ h + g ⊗ h
[PROOFSTEP]
intros
[GOAL]
case refine'_4
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : W✝ ⟶ X✝
h✝ : Y✝ ⟶ Z✝
⊢ (f✝ + g✝) ⊗ h✝ = f✝ ⊗ h✝ + g✝ ⊗ h✝
[PROOFSTEP]
refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
[GOAL]
case refine'_4
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : W✝ ⟶ X✝
h✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) ((f✝ + g✝) ⊗ h✝)) x) y =
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) (f✝ ⊗ h✝ + g✝ ⊗ h✝)) x) y
[PROOFSTEP]
simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
[GOAL]
case refine'_4
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : W✝ ⟶ X✝
h✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑((f✝ + g✝) ⊗ h✝) (x ⊗ₜ[R] y) = ↑(f✝ ⊗ h✝ + g✝ ⊗ h✝) (x ⊗ₜ[R] y)
[PROOFSTEP]
rw [LinearMap.add_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
[GOAL]
case refine'_4
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : W✝ ⟶ X✝
h✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(f✝ + g✝) x ⊗ₜ[R] ↑h✝ y = ↑f✝ x ⊗ₜ[R] ↑h✝ y + ↑(g✝ ⊗ h✝) (x ⊗ₜ[R] y)
[PROOFSTEP]
erw [MonoidalCategory.hom_apply]
[GOAL]
case refine'_4
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ g✝ : W✝ ⟶ X✝
h✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(f✝ + g✝) x ⊗ₜ[R] ↑h✝ y = ↑f✝ x ⊗ₜ[R] ↑h✝ y + ↑g✝ x ⊗ₜ[R] ↑h✝ y
[PROOFSTEP]
rw [LinearMap.add_apply, TensorProduct.add_tmul]
  -- Porting note: simp wasn't firing but rw was, annoying
[GOAL]
R : Type u
inst✝ : CommRing R
⊢ MonoidalLinear R (ModuleCat R)
[PROOFSTEP]
refine' ⟨_, _⟩
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f : W ⟶ X) (r : R) (g : Y ⟶ Z), f ⊗ r • g = r • (f ⊗ g)
[PROOFSTEP]
dsimp only [autoParam]
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (f : W ⟶ X) (r : R) (g : Y ⟶ Z), f ⊗ r • g = r • (f ⊗ g)
[PROOFSTEP]
intros
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
r✝ : R
g✝ : Y✝ ⟶ Z✝
⊢ f✝ ⊗ r✝ • g✝ = r✝ • (f✝ ⊗ g✝)
[PROOFSTEP]
refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
r✝ : R
g✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) (f✝ ⊗ r✝ • g✝)) x) y =
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) (r✝ • (f✝ ⊗ g✝))) x) y
[PROOFSTEP]
simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
[GOAL]
case refine'_1
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
f✝ : W✝ ⟶ X✝
r✝ : R
g✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(f✝ ⊗ r✝ • g✝) (x ⊗ₜ[R] y) = ↑(r✝ • (f✝ ⊗ g✝)) (x ⊗ₜ[R] y)
[PROOFSTEP]
rw [LinearMap.smul_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply, LinearMap.smul_apply,
  TensorProduct.tmul_smul]
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (r : R) (f : W ⟶ X) (g : Y ⟶ Z), r • f ⊗ g = r • (f ⊗ g)
[PROOFSTEP]
dsimp only [autoParam]
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
⊢ ∀ {W X Y Z : ModuleCat R} (r : R) (f : W ⟶ X) (g : Y ⟶ Z), r • f ⊗ g = r • (f ⊗ g)
[PROOFSTEP]
intros
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
r✝ : R
f✝ : W✝ ⟶ X✝
g✝ : Y✝ ⟶ Z✝
⊢ r✝ • f✝ ⊗ g✝ = r✝ • (f✝ ⊗ g✝)
[PROOFSTEP]
refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
r✝ : R
f✝ : W✝ ⟶ X✝
g✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) (r✝ • f✝ ⊗ g✝)) x) y =
    ↑(↑(LinearMap.compr₂ (TensorProduct.mk R ↑W✝ ↑Y✝) (r✝ • (f✝ ⊗ g✝))) x) y
[PROOFSTEP]
simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
[GOAL]
case refine'_2
R : Type u
inst✝ : CommRing R
W✝ X✝ Y✝ Z✝ : ModuleCat R
r✝ : R
f✝ : W✝ ⟶ X✝
g✝ : Y✝ ⟶ Z✝
x : ↑W✝
y : ↑Y✝
⊢ ↑(r✝ • f✝ ⊗ g✝) (x ⊗ₜ[R] y) = ↑(r✝ • (f✝ ⊗ g✝)) (x ⊗ₜ[R] y)
[PROOFSTEP]
rw [LinearMap.smul_apply, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply, LinearMap.smul_apply,
  TensorProduct.smul_tmul, TensorProduct.tmul_smul]
