C : Type u_3
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_1
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
⊢ ((∑ j in s, g j) ⊗ 𝟙 P) ≫ (𝟙 S ⊗ f) = ∑ j in s, g j ⊗ f
C : Type u_3
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_1
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
⊢ (∑ j in s, g j) ⊗ f = ∑ j in s, g j ⊗ f
rw [← tensor_id_comp_id_tensor]
C : Type u_3
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_1
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
tQ : (R ⟶ S) →+ (((tensoringRight C).obj P).obj R ⟶ ((tensoringRight C).obj P).obj S) :=
  Functor.mapAddHom ((tensoringRight C).obj P)
⊢ ((∑ j in s, g j) ⊗ 𝟙 P) ≫ (𝟙 S ⊗ f) = ∑ j in s, g j ⊗ f
C : Type u_3
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_1
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
⊢ ((∑ j in s, g j) ⊗ 𝟙 P) ≫ (𝟙 S ⊗ f) = ∑ j in s, g j ⊗ f
let tQ := (((tensoringRight C).obj P).mapAddHom : (R ⟶ S) →+ _)
C : Type u_3
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_1
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
tQ : (R ⟶ S) →+ (((tensoringRight C).obj P).obj R ⟶ ((tensoringRight C).obj P).obj S) :=
  Functor.mapAddHom ((tensoringRight C).obj P)
⊢ ↑tQ (∑ j in s, g j) ≫ (𝟙 S ⊗ f) = ∑ j in s, g j ⊗ f
C : Type u_3
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_1
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
tQ : (R ⟶ S) →+ (((tensoringRight C).obj P).obj R ⟶ ((tensoringRight C).obj P).obj S) :=
  Functor.mapAddHom ((tensoringRight C).obj P)
⊢ ((∑ j in s, g j) ⊗ 𝟙 P) ≫ (𝟙 S ⊗ f) = ∑ j in s, g j ⊗ f
change tQ _ ≫ _ = _
C : Type u_3
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_1
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
tQ : (R ⟶ S) →+ (((tensoringRight C).obj P).obj R ⟶ ((tensoringRight C).obj P).obj S) :=
  Functor.mapAddHom ((tensoringRight C).obj P)
⊢ ∑ j in s, ↑tQ (g j) ≫ (𝟙 S ⊗ f) = ∑ j in s, g j ⊗ f
C : Type u_3
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_1
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
tQ : (R ⟶ S) →+ (((tensoringRight C).obj P).obj R ⟶ ((tensoringRight C).obj P).obj S) :=
  Functor.mapAddHom ((tensoringRight C).obj P)
⊢ ↑tQ (∑ j in s, g j) ≫ (𝟙 S ⊗ f) = ∑ j in s, g j ⊗ f
rw [tQ.map_sum, Preadditive.sum_comp]
C : Type u_3
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_1
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
tQ : (R ⟶ S) →+ (((tensoringRight C).obj P).obj R ⟶ ((tensoringRight C).obj P).obj S) :=
  Functor.mapAddHom ((tensoringRight C).obj P)
⊢ ∑ j in s, (g j ⊗ 𝟙 P) ≫ (𝟙 S ⊗ f) = ∑ j in s, g j ⊗ f
C : Type u_3
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_1
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
tQ : (R ⟶ S) →+ (((tensoringRight C).obj P).obj R ⟶ ((tensoringRight C).obj P).obj S) :=
  Functor.mapAddHom ((tensoringRight C).obj P)
⊢ ∑ j in s, ↑tQ (g j) ≫ (𝟙 S ⊗ f) = ∑ j in s, g j ⊗ f
dsimp [Functor.mapAddHom]
no goals
C : Type u_3
inst✝³ : Category C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_1
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
tQ : (R ⟶ S) →+ (((tensoringRight C).obj P).obj R ⟶ ((tensoringRight C).obj P).obj S) :=
  Functor.mapAddHom ((tensoringRight C).obj P)
⊢ ∑ j in s, (g j ⊗ 𝟙 P) ≫ (𝟙 S ⊗ f) = ∑ j in s, g j ⊗ f
simp only [tensor_id_comp_id_tensor]