[GOAL]
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : MonoidalFunctor D C
inst✝² : Faithful F.toFunctor
inst✝¹ : Functor.Additive F.toFunctor
inst✝ : Functor.Linear R F.toFunctor
⊢ ∀ {W X Y Z : D} (f : W ⟶ X) (r : R) (g : Y ⟶ Z), f ⊗ r • g = r • (f ⊗ g)
[PROOFSTEP]
intros W X Y Z f r g
[GOAL]
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : MonoidalFunctor D C
inst✝² : Faithful F.toFunctor
inst✝¹ : Functor.Additive F.toFunctor
inst✝ : Functor.Linear R F.toFunctor
W X Y Z : D
f : W ⟶ X
r : R
g : Y ⟶ Z
⊢ f ⊗ r • g = r • (f ⊗ g)
[PROOFSTEP]
apply F.toFunctor.map_injective
[GOAL]
case a
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : MonoidalFunctor D C
inst✝² : Faithful F.toFunctor
inst✝¹ : Functor.Additive F.toFunctor
inst✝ : Functor.Linear R F.toFunctor
W X Y Z : D
f : W ⟶ X
r : R
g : Y ⟶ Z
⊢ F.map (f ⊗ r • g) = F.map (r • (f ⊗ g))
[PROOFSTEP]
simp only [F.toFunctor.map_smul r (f ⊗ g), F.toFunctor.map_smul r g, F.map_tensor, MonoidalLinear.tensor_smul,
  Linear.smul_comp, Linear.comp_smul]
[GOAL]
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : MonoidalFunctor D C
inst✝² : Faithful F.toFunctor
inst✝¹ : Functor.Additive F.toFunctor
inst✝ : Functor.Linear R F.toFunctor
⊢ ∀ {W X Y Z : D} (r : R) (f : W ⟶ X) (g : Y ⟶ Z), r • f ⊗ g = r • (f ⊗ g)
[PROOFSTEP]
intros W X Y Z r f g
[GOAL]
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : MonoidalFunctor D C
inst✝² : Faithful F.toFunctor
inst✝¹ : Functor.Additive F.toFunctor
inst✝ : Functor.Linear R F.toFunctor
W X Y Z : D
r : R
f : W ⟶ X
g : Y ⟶ Z
⊢ r • f ⊗ g = r • (f ⊗ g)
[PROOFSTEP]
apply F.toFunctor.map_injective
[GOAL]
case a
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : MonoidalFunctor D C
inst✝² : Faithful F.toFunctor
inst✝¹ : Functor.Additive F.toFunctor
inst✝ : Functor.Linear R F.toFunctor
W X Y Z : D
r : R
f : W ⟶ X
g : Y ⟶ Z
⊢ F.map (r • f ⊗ g) = F.map (r • (f ⊗ g))
[PROOFSTEP]
simp only [F.toFunctor.map_smul r (f ⊗ g), F.toFunctor.map_smul r f, F.map_tensor, MonoidalLinear.smul_tensor,
  Linear.smul_comp, Linear.comp_smul]
