R : Type u_3
inst✝¹⁴ : Semiring R
C : Type u_5
inst✝¹³ : Category C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_1
inst✝⁷ : Category 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)
R : Type u_3
inst✝¹⁴ : Semiring R
C : Type u_5
inst✝¹³ : Category C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_1
inst✝⁷ : Category 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)
intros W X Y Z f r g
case a
R : Type u_3
inst✝¹⁴ : Semiring R
C : Type u_5
inst✝¹³ : Category C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_1
inst✝⁷ : Category 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))
R : Type u_3
inst✝¹⁴ : Semiring R
C : Type u_5
inst✝¹³ : Category C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_1
inst✝⁷ : Category 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)
apply F.toFunctor.map_injective
no goals
case a
R : Type u_3
inst✝¹⁴ : Semiring R
C : Type u_5
inst✝¹³ : Category C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_1
inst✝⁷ : Category 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))
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]
R : Type u_3
inst✝¹⁴ : Semiring R
C : Type u_5
inst✝¹³ : Category C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_1
inst✝⁷ : Category 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)
R : Type u_3
inst✝¹⁴ : Semiring R
C : Type u_5
inst✝¹³ : Category C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_1
inst✝⁷ : Category 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)
intros W X Y Z r f g
case a
R : Type u_3
inst✝¹⁴ : Semiring R
C : Type u_5
inst✝¹³ : Category C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_1
inst✝⁷ : Category 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))
R : Type u_3
inst✝¹⁴ : Semiring R
C : Type u_5
inst✝¹³ : Category C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_1
inst✝⁷ : Category 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)
apply F.toFunctor.map_injective
no goals
case a
R : Type u_3
inst✝¹⁴ : Semiring R
C : Type u_5
inst✝¹³ : Category C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_1
inst✝⁷ : Category 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))
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]