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)
⊢ (f ⊗ 𝟙 R) ≫ (𝟙 Q ⊗ ∑ j in s, g j) = ∑ j in s, f ⊗ g j
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)
⊢ f ⊗ ∑ j in s, g j = ∑ j in s, f ⊗ g j
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) →+ (((tensoringLeft C).obj Q).obj R ⟶ ((tensoringLeft C).obj Q).obj S) :=
  Functor.mapAddHom ((tensoringLeft C).obj Q)
⊢ (f ⊗ 𝟙 R) ≫ (𝟙 Q ⊗ ∑ j in s, g j) = ∑ j in s, f ⊗ g j
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)
⊢ (f ⊗ 𝟙 R) ≫ (𝟙 Q ⊗ ∑ j in s, g j) = ∑ j in s, f ⊗ g j
let tQ := (((tensoringLeft C).obj Q).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) →+ (((tensoringLeft C).obj Q).obj R ⟶ ((tensoringLeft C).obj Q).obj S) :=
  Functor.mapAddHom ((tensoringLeft C).obj Q)
⊢ (f ⊗ 𝟙 R) ≫ ↑tQ (∑ j in s, g j) = ∑ j in s, f ⊗ g j
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) →+ (((tensoringLeft C).obj Q).obj R ⟶ ((tensoringLeft C).obj Q).obj S) :=
  Functor.mapAddHom ((tensoringLeft C).obj Q)
⊢ (f ⊗ 𝟙 R) ≫ (𝟙 Q ⊗ ∑ j in s, g j) = ∑ j in s, f ⊗ g j
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) →+ (((tensoringLeft C).obj Q).obj R ⟶ ((tensoringLeft C).obj Q).obj S) :=
  Functor.mapAddHom ((tensoringLeft C).obj Q)
⊢ ∑ j in s, (f ⊗ 𝟙 R) ≫ ↑tQ (g j) = ∑ j in s, f ⊗ g j
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) →+ (((tensoringLeft C).obj Q).obj R ⟶ ((tensoringLeft C).obj Q).obj S) :=
  Functor.mapAddHom ((tensoringLeft C).obj Q)
⊢ (f ⊗ 𝟙 R) ≫ ↑tQ (∑ j in s, g j) = ∑ j in s, f ⊗ g j
rw [tQ.map_sum, Preadditive.comp_sum]
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) →+ (((tensoringLeft C).obj Q).obj R ⟶ ((tensoringLeft C).obj Q).obj S) :=
  Functor.mapAddHom ((tensoringLeft C).obj Q)
⊢ ∑ j in s, (f ⊗ 𝟙 R) ≫ (𝟙 Q ⊗ g j) = ∑ j in s, f ⊗ g j
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) →+ (((tensoringLeft C).obj Q).obj R ⟶ ((tensoringLeft C).obj Q).obj S) :=
  Functor.mapAddHom ((tensoringLeft C).obj Q)
⊢ ∑ j in s, (f ⊗ 𝟙 R) ≫ ↑tQ (g j) = ∑ j in s, f ⊗ g j
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) →+ (((tensoringLeft C).obj Q).obj R ⟶ ((tensoringLeft C).obj Q).obj S) :=
  Functor.mapAddHom ((tensoringLeft C).obj Q)
⊢ ∑ j in s, (f ⊗ 𝟙 R) ≫ (𝟙 Q ⊗ g j) = ∑ j in s, f ⊗ g j
simp only [tensor_id_comp_id_tensor]