[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
⊢ ∀ {W X Y Z : D} (f : W ⟶ X), f ⊗ 0 = 0
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
W✝ X✝ Y✝ Z✝ : D
f✝ : W✝ ⟶ X✝
⊢ f✝ ⊗ 0 = 0
[PROOFSTEP]
apply F.toFunctor.map_injective
[GOAL]
case a
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
W✝ X✝ Y✝ Z✝ : D
f✝ : W✝ ⟶ X✝
⊢ F.map (f✝ ⊗ 0) = F.map 0
[PROOFSTEP]
simp [F.map_tensor]
[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
⊢ ∀ {W X Y Z : D} (f : Y ⟶ Z), 0 ⊗ f = 0
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
W✝ X✝ Y✝ Z✝ : D
f✝ : Y✝ ⟶ Z✝
⊢ 0 ⊗ f✝ = 0
[PROOFSTEP]
apply F.toFunctor.map_injective
[GOAL]
case a
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
W✝ X✝ Y✝ Z✝ : D
f✝ : Y✝ ⟶ Z✝
⊢ F.map (0 ⊗ f✝) = F.map 0
[PROOFSTEP]
simp [F.map_tensor]
[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
⊢ ∀ {W X Y Z : D} (f : W ⟶ X) (g h : Y ⟶ Z), f ⊗ (g + h) = f ⊗ g + f ⊗ h
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
W✝ X✝ Y✝ Z✝ : D
f✝ : W✝ ⟶ X✝
g✝ h✝ : Y✝ ⟶ Z✝
⊢ f✝ ⊗ (g✝ + h✝) = f✝ ⊗ g✝ + f✝ ⊗ h✝
[PROOFSTEP]
apply F.toFunctor.map_injective
[GOAL]
case a
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
W✝ X✝ Y✝ Z✝ : D
f✝ : W✝ ⟶ X✝
g✝ h✝ : Y✝ ⟶ Z✝
⊢ F.map (f✝ ⊗ (g✝ + h✝)) = F.map (f✝ ⊗ g✝ + f✝ ⊗ h✝)
[PROOFSTEP]
simp only [F.map_tensor, Functor.map_add, Preadditive.comp_add, Preadditive.add_comp, MonoidalPreadditive.tensor_add]
[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
⊢ ∀ {W X Y Z : D} (f g : W ⟶ X) (h : Y ⟶ Z), (f + g) ⊗ h = f ⊗ h + g ⊗ h
[PROOFSTEP]
intros
[GOAL]
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
W✝ X✝ Y✝ Z✝ : D
f✝ g✝ : W✝ ⟶ X✝
h✝ : Y✝ ⟶ Z✝
⊢ (f✝ + g✝) ⊗ h✝ = f✝ ⊗ h✝ + g✝ ⊗ h✝
[PROOFSTEP]
apply F.toFunctor.map_injective
[GOAL]
case a
C : Type u_1
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : Preadditive C
inst✝⁶ : MonoidalCategory C
inst✝⁵ : MonoidalPreadditive C
D : Type u_2
inst✝⁴ : Category.{u_3, u_2} D
inst✝³ : Preadditive D
inst✝² : MonoidalCategory D
F : MonoidalFunctor D C
inst✝¹ : Faithful F.toFunctor
inst✝ : Functor.Additive F.toFunctor
W✝ X✝ Y✝ Z✝ : D
f✝ g✝ : W✝ ⟶ X✝
h✝ : Y✝ ⟶ Z✝
⊢ F.map ((f✝ + g✝) ⊗ h✝) = F.map (f✝ ⊗ h✝ + g✝ ⊗ h✝)
[PROOFSTEP]
simp only [F.map_tensor, Functor.map_add, Preadditive.comp_add, Preadditive.add_comp, MonoidalPreadditive.add_tensor]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
⊢ f ⊗ ∑ j in s, g j = ∑ j in s, f ⊗ g j
[PROOFSTEP]
rw [← tensor_id_comp_id_tensor]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
⊢ (f ⊗ 𝟙 R) ≫ (𝟙 Q ⊗ ∑ j in s, g j) = ∑ j in s, f ⊗ g j
[PROOFSTEP]
let tQ := (((tensoringLeft C).obj Q).mapAddHom : (R ⟶ S) →+ _)
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
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
[PROOFSTEP]
change _ ≫ tQ _ = _
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
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
[PROOFSTEP]
rw [tQ.map_sum, Preadditive.comp_sum]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
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
[PROOFSTEP]
dsimp [Functor.mapAddHom]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
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
[PROOFSTEP]
simp only [tensor_id_comp_id_tensor]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
⊢ (∑ j in s, g j) ⊗ f = ∑ j in s, g j ⊗ f
[PROOFSTEP]
rw [← tensor_id_comp_id_tensor]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
s : Finset J
f : P ⟶ Q
g : J → (R ⟶ S)
⊢ ((∑ j in s, g j) ⊗ 𝟙 P) ≫ (𝟙 S ⊗ f) = ∑ j in s, g j ⊗ f
[PROOFSTEP]
let tQ := (((tensoringRight C).obj P).mapAddHom : (R ⟶ S) →+ _)
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
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
[PROOFSTEP]
change tQ _ ≫ _ = _
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
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
[PROOFSTEP]
rw [tQ.map_sum, Preadditive.sum_comp]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
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
[PROOFSTEP]
dsimp [Functor.mapAddHom]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
P Q R S : C
J : Type u_2
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
[PROOFSTEP]
simp only [tensor_id_comp_id_tensor]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.453496, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Fintype J
f : J → C
b : Bicone f
i : Bicone.IsBilimit b
⊢ ∑ j : J, Bicone.π (Functor.mapBicone (tensorLeft X) b) j ≫ Bicone.ι (Functor.mapBicone (tensorLeft X) b) j =
    𝟙 (Functor.mapBicone (tensorLeft X) b).pt
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.453496, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Fintype J
f : J → C
b : Bicone f
i : Bicone.IsBilimit b
⊢ ∑ j : J, (𝟙 X ⊗ Bicone.π b j) ≫ (𝟙 X ⊗ Bicone.ι b j) = 𝟙 (X ⊗ b.pt)
[PROOFSTEP]
simp only [← tensor_comp, Category.comp_id, ← tensor_sum, ← tensor_id, IsBilimit.total i]
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.457304, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Fintype J
f : J → C
b : Bicone f
i : Bicone.IsBilimit b
⊢ ∑ j : J, Bicone.π (Functor.mapBicone (tensorRight X) b) j ≫ Bicone.ι (Functor.mapBicone (tensorRight X) b) j =
    𝟙 (Functor.mapBicone (tensorRight X) b).pt
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁴ : Category.{?u.457304, u_1} C
inst✝³ : Preadditive C
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalPreadditive C
X : C
J : Type
inst✝ : Fintype J
f : J → C
b : Bicone f
i : Bicone.IsBilimit b
⊢ ∑ j : J, (Bicone.π b j ⊗ 𝟙 X) ≫ (Bicone.ι b j ⊗ 𝟙 X) = 𝟙 (b.pt ⊗ X)
[PROOFSTEP]
simp only [← tensor_comp, Category.comp_id, ← sum_tensor, ← tensor_id, IsBilimit.total i]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
⊢ (leftDistributor X f).hom = ∑ j : J, (𝟙 X ⊗ biproduct.π f j) ≫ biproduct.ι (fun j => X ⊗ f j) j
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ (leftDistributor X f).hom ≫ biproduct.π (fun j => X ⊗ f j) j✝ =
    (∑ j : J, (𝟙 X ⊗ biproduct.π f j) ≫ biproduct.ι (fun j => X ⊗ f j) j) ≫ biproduct.π (fun j => X ⊗ f j) j✝
[PROOFSTEP]
dsimp [leftDistributor, Functor.mapBiproduct, Functor.mapBicone]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ (biproduct.lift fun j => 𝟙 X ⊗ biproduct.π f j) ≫ biproduct.π (fun j => X ⊗ f j) j✝ =
    (∑ j : J, (𝟙 X ⊗ biproduct.π f j) ≫ biproduct.ι (fun j => X ⊗ f j) j) ≫ biproduct.π (fun j => X ⊗ f j) j✝
[PROOFSTEP]
erw [biproduct.lift_π]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ 𝟙 X ⊗ biproduct.π f j✝ =
    (∑ j : J, (𝟙 X ⊗ biproduct.π f j) ≫ biproduct.ι (fun j => X ⊗ f j) j) ≫ biproduct.π (fun j => X ⊗ f j) j✝
[PROOFSTEP]
simp only [Preadditive.sum_comp, Category.assoc, biproduct.ι_π, comp_dite, comp_zero, Finset.sum_dite_eq',
  Finset.mem_univ, ite_true, eqToHom_refl, Category.comp_id]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
⊢ (leftDistributor X f).inv = ∑ j : J, biproduct.π (fun j => X ⊗ f j) j ≫ (𝟙 X ⊗ biproduct.ι f j)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ biproduct.ι (fun j => X ⊗ f j) j✝ ≫ (leftDistributor X f).inv =
    biproduct.ι (fun j => X ⊗ f j) j✝ ≫ ∑ j : J, biproduct.π (fun j => X ⊗ f j) j ≫ (𝟙 X ⊗ biproduct.ι f j)
[PROOFSTEP]
dsimp [leftDistributor, Functor.mapBiproduct, Functor.mapBicone]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j✝ : J
⊢ (biproduct.ι (fun j => X ⊗ f j) j✝ ≫ biproduct.desc fun j => 𝟙 X ⊗ biproduct.ι f j) =
    biproduct.ι (fun j => X ⊗ f j) j✝ ≫ ∑ j : J, biproduct.π (fun j => X ⊗ f j) j ≫ (𝟙 X ⊗ biproduct.ι f j)
[PROOFSTEP]
simp only [Preadditive.comp_sum, biproduct.ι_π_assoc, dite_comp, zero_comp, Finset.sum_dite_eq, Finset.mem_univ,
  ite_true, eqToHom_refl, Category.id_comp, biproduct.ι_desc]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j : J
⊢ (leftDistributor X f).hom ≫ biproduct.π (fun j => X ⊗ f j) j = 𝟙 X ⊗ biproduct.π f j
[PROOFSTEP]
simp [leftDistributor_hom, Preadditive.sum_comp, biproduct.ι_π, comp_dite]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j : J
⊢ (𝟙 X ⊗ biproduct.ι f j) ≫ (leftDistributor X f).hom = biproduct.ι (fun j => X ⊗ f j) j
[PROOFSTEP]
simp [leftDistributor_hom, Preadditive.comp_sum, ← id_tensor_comp_assoc, biproduct.ι_π, tensor_dite, dite_comp]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j : J
⊢ (leftDistributor X f).inv ≫ (𝟙 X ⊗ biproduct.π f j) = biproduct.π (fun j => X ⊗ f j) j
[PROOFSTEP]
simp [leftDistributor_inv, Preadditive.sum_comp, ← id_tensor_comp, biproduct.ι_π, tensor_dite, comp_dite]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j : J
⊢ biproduct.ι (fun j => X ⊗ f j) j ≫ (leftDistributor X f).inv = 𝟙 X ⊗ biproduct.ι f j
[PROOFSTEP]
simp [leftDistributor_inv, Preadditive.comp_sum, ← id_tensor_comp, biproduct.ι_π_assoc, dite_comp]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
⊢ ((asIso (𝟙 X) ⊗ leftDistributor Y f) ≪≫ leftDistributor X fun j => Y ⊗ f j) =
    (α_ X Y (⨁ f)).symm ≪≫ leftDistributor (X ⊗ Y) f ≪≫ biproduct.mapIso fun j => α_ X Y (f j)
[PROOFSTEP]
ext
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
j✝ : J
⊢ ((asIso (𝟙 X) ⊗ leftDistributor Y f) ≪≫ leftDistributor X fun j => Y ⊗ f j).hom ≫
      biproduct.π (fun j => X ⊗ Y ⊗ f j) j✝ =
    ((α_ X Y (⨁ f)).symm ≪≫ leftDistributor (X ⊗ Y) f ≪≫ biproduct.mapIso fun j => α_ X Y (f j)).hom ≫
      biproduct.π (fun j => X ⊗ Y ⊗ f j) j✝
[PROOFSTEP]
simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.trans_hom, Iso.symm_hom, asIso_hom, comp_zero, comp_dite,
  Preadditive.sum_comp, Preadditive.comp_sum, tensor_sum, id_tensor_comp, tensorIso_hom, leftDistributor_hom,
  biproduct.mapIso_hom, biproduct.ι_map, biproduct.ι_π, Finset.sum_dite_irrel, Finset.sum_dite_eq',
  Finset.sum_const_zero]
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
j✝ : J
⊢ (if j✝ ∈ Finset.univ then
      ∑ x : J,
        (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.π f x) ≫
          (𝟙 X ⊗ biproduct.ι (fun j => Y ⊗ f j) x) ≫ (𝟙 X ⊗ biproduct.π (fun j => Y ⊗ f j) j✝)
    else 0) =
    if j✝ ∈ Finset.univ then (α_ X Y (⨁ f)).inv ≫ (𝟙 (X ⊗ Y) ⊗ biproduct.π f j✝) ≫ (α_ X Y (f j✝)).hom else 0
[PROOFSTEP]
simp only [← id_tensor_comp, biproduct.ι_π]
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
j✝ : J
⊢ (if j✝ ∈ Finset.univ then
      ∑ x : J, 𝟙 X ⊗ (𝟙 Y ⊗ biproduct.π f x) ≫ if h : x = j✝ then eqToHom (_ : Y ⊗ f x = Y ⊗ f j✝) else 0
    else 0) =
    if j✝ ∈ Finset.univ then (α_ X Y (⨁ f)).inv ≫ (𝟙 (X ⊗ Y) ⊗ biproduct.π f j✝) ≫ (α_ X Y (f j✝)).hom else 0
[PROOFSTEP]
simp only [id_tensor_comp, tensor_dite, comp_dite]
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
j✝ : J
⊢ (if j✝ ∈ Finset.univ then
      ∑ x : J,
        if h : x = j✝ then (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.π f x) ≫ (𝟙 X ⊗ eqToHom (_ : Y ⊗ f x = Y ⊗ f j✝))
        else (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.π f x) ≫ (𝟙 X ⊗ 0)
    else 0) =
    if j✝ ∈ Finset.univ then (α_ X Y (⨁ f)).inv ≫ (𝟙 (X ⊗ Y) ⊗ biproduct.π f j✝) ≫ (α_ X Y (f j✝)).hom else 0
[PROOFSTEP]
simp only [Category.comp_id, comp_zero, MonoidalPreadditive.tensor_zero, eqToHom_refl, tensor_id, if_true,
  dif_ctx_congr, Finset.sum_congr, Finset.mem_univ, Finset.sum_dite_eq']
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
j✝ : J
⊢ 𝟙 X ⊗ 𝟙 Y ⊗ biproduct.π f j✝ = (α_ X Y (⨁ f)).inv ≫ (𝟙 (X ⊗ Y) ⊗ biproduct.π f j✝) ≫ (α_ X Y (f j✝)).hom
[PROOFSTEP]
simp only [← tensor_id, associator_naturality, Iso.inv_hom_id_assoc]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
⊢ (rightDistributor f X).hom = ∑ j : J, (biproduct.π f j ⊗ 𝟙 X) ≫ biproduct.ι (fun j => f j ⊗ X) j
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ (rightDistributor f X).hom ≫ biproduct.π (fun j => f j ⊗ X) j✝ =
    (∑ j : J, (biproduct.π f j ⊗ 𝟙 X) ≫ biproduct.ι (fun j => f j ⊗ X) j) ≫ biproduct.π (fun j => f j ⊗ X) j✝
[PROOFSTEP]
dsimp [rightDistributor, Functor.mapBiproduct, Functor.mapBicone]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ (biproduct.lift fun j => biproduct.π f j ⊗ 𝟙 X) ≫ biproduct.π (fun j => f j ⊗ X) j✝ =
    (∑ j : J, (biproduct.π f j ⊗ 𝟙 X) ≫ biproduct.ι (fun j => f j ⊗ X) j) ≫ biproduct.π (fun j => f j ⊗ X) j✝
[PROOFSTEP]
erw [biproduct.lift_π]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ biproduct.π f j✝ ⊗ 𝟙 X =
    (∑ j : J, (biproduct.π f j ⊗ 𝟙 X) ≫ biproduct.ι (fun j => f j ⊗ X) j) ≫ biproduct.π (fun j => f j ⊗ X) j✝
[PROOFSTEP]
simp only [Preadditive.sum_comp, Category.assoc, biproduct.ι_π, comp_dite, comp_zero, Finset.sum_dite_eq',
  Finset.mem_univ, eqToHom_refl, Category.comp_id, ite_true]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
⊢ (rightDistributor f X).inv = ∑ j : J, biproduct.π (fun j => f j ⊗ X) j ≫ (biproduct.ι f j ⊗ 𝟙 X)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv =
    biproduct.ι (fun j => f j ⊗ X) j✝ ≫ ∑ j : J, biproduct.π (fun j => f j ⊗ X) j ≫ (biproduct.ι f j ⊗ 𝟙 X)
[PROOFSTEP]
dsimp [rightDistributor, Functor.mapBiproduct, Functor.mapBicone]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ (biproduct.ι (fun j => f j ⊗ X) j✝ ≫ biproduct.desc fun j => biproduct.ι f j ⊗ 𝟙 X) =
    biproduct.ι (fun j => f j ⊗ X) j✝ ≫ ∑ j : J, biproduct.π (fun j => f j ⊗ X) j ≫ (biproduct.ι f j ⊗ 𝟙 X)
[PROOFSTEP]
simp only [biproduct.ι_desc, Preadditive.comp_sum, ne_eq, biproduct.ι_π_assoc, dite_comp, zero_comp, Finset.sum_dite_eq,
  Finset.mem_univ, eqToHom_refl, Category.id_comp, ite_true]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j : J
⊢ (rightDistributor f X).hom ≫ biproduct.π (fun j => f j ⊗ X) j = biproduct.π f j ⊗ 𝟙 X
[PROOFSTEP]
simp [rightDistributor_hom, Preadditive.sum_comp, biproduct.ι_π, comp_dite]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j : J
⊢ (biproduct.ι f j ⊗ 𝟙 X) ≫ (rightDistributor f X).hom = biproduct.ι (fun j => f j ⊗ X) j
[PROOFSTEP]
simp [rightDistributor_hom, Preadditive.comp_sum, ← comp_tensor_id_assoc, biproduct.ι_π, dite_tensor, dite_comp]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j : J
⊢ (rightDistributor f X).inv ≫ (biproduct.π f j ⊗ 𝟙 X) = biproduct.π (fun j => f j ⊗ X) j
[PROOFSTEP]
simp [rightDistributor_inv, Preadditive.sum_comp, ← comp_tensor_id, biproduct.ι_π, dite_tensor, comp_dite]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j : J
⊢ biproduct.ι (fun j => f j ⊗ X) j ≫ (rightDistributor f X).inv = biproduct.ι f j ⊗ 𝟙 X
[PROOFSTEP]
simp [rightDistributor_inv, Preadditive.comp_sum, ← id_tensor_comp, biproduct.ι_π_assoc, dite_comp]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
⊢ (rightDistributor f X ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j => f j ⊗ X) Y =
    α_ (⨁ f) X Y ≪≫ rightDistributor f (X ⊗ Y) ≪≫ biproduct.mapIso fun j => (α_ (f j) X Y).symm
[PROOFSTEP]
ext
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
j✝ : J
⊢ ((rightDistributor f X ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j => f j ⊗ X) Y).hom ≫
      biproduct.π (fun j => (f j ⊗ X) ⊗ Y) j✝ =
    (α_ (⨁ f) X Y ≪≫ rightDistributor f (X ⊗ Y) ≪≫ biproduct.mapIso fun j => (α_ (f j) X Y).symm).hom ≫
      biproduct.π (fun j => (f j ⊗ X) ⊗ Y) j✝
[PROOFSTEP]
simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.symm_hom, Iso.trans_hom, asIso_hom, comp_zero, comp_dite,
  Preadditive.sum_comp, Preadditive.comp_sum, sum_tensor, comp_tensor_id, tensorIso_hom, rightDistributor_hom,
  biproduct.mapIso_hom, biproduct.ι_map, biproduct.ι_π, Finset.sum_dite_irrel, Finset.sum_dite_eq',
  Finset.sum_const_zero, Finset.mem_univ, if_true]
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
j✝ : J
⊢ ∑ x : J,
      ((biproduct.π f x ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫
        (biproduct.ι (fun j => f j ⊗ X) x ⊗ 𝟙 Y) ≫ (biproduct.π (fun j => f j ⊗ X) j✝ ⊗ 𝟙 Y) =
    (α_ (⨁ f) X Y).hom ≫ (biproduct.π f j✝ ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ (f j✝) X Y).inv
[PROOFSTEP]
simp only [← comp_tensor_id, biproduct.ι_π, dite_tensor, comp_dite]
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
j✝ : J
⊢ (∑ x : J,
      if h : x = j✝ then (biproduct.π f x ⊗ 𝟙 X) ≫ eqToHom (_ : f x ⊗ X = f j✝ ⊗ X) ⊗ 𝟙 Y
      else (biproduct.π f x ⊗ 𝟙 X) ≫ 0 ⊗ 𝟙 Y) =
    (α_ (⨁ f) X Y).hom ≫ (biproduct.π f j✝ ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ (f j✝) X Y).inv
[PROOFSTEP]
simp only [Category.comp_id, comp_tensor_id, eqToHom_refl, tensor_id, comp_zero, MonoidalPreadditive.zero_tensor,
  if_true, dif_ctx_congr, Finset.mem_univ, Finset.sum_congr, Finset.sum_dite_eq']
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
j✝ : J
⊢ (biproduct.π f j✝ ⊗ 𝟙 X) ⊗ 𝟙 Y = (α_ (⨁ f) X Y).hom ≫ (biproduct.π f j✝ ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ (f j✝) X Y).inv
[PROOFSTEP]
simp only [← tensor_id, associator_inv_naturality, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
Y : C
⊢ (leftDistributor X f ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j => X ⊗ f j) Y =
    α_ X (⨁ f) Y ≪≫
      (asIso (𝟙 X) ⊗ rightDistributor f Y) ≪≫
        (leftDistributor X fun j => f j ⊗ Y) ≪≫ biproduct.mapIso fun j => (α_ X (f j) Y).symm
[PROOFSTEP]
ext
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
Y : C
j✝ : J
⊢ ((leftDistributor X f ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j => X ⊗ f j) Y).hom ≫
      biproduct.π (fun j => (X ⊗ f j) ⊗ Y) j✝ =
    (α_ X (⨁ f) Y ≪≫
          (asIso (𝟙 X) ⊗ rightDistributor f Y) ≪≫
            (leftDistributor X fun j => f j ⊗ Y) ≪≫ biproduct.mapIso fun j => (α_ X (f j) Y).symm).hom ≫
      biproduct.π (fun j => (X ⊗ f j) ⊗ Y) j✝
[PROOFSTEP]
simp only [Category.comp_id, Category.assoc, eqToHom_refl, Iso.symm_hom, Iso.trans_hom, asIso_hom, comp_zero, comp_dite,
  Preadditive.sum_comp, Preadditive.comp_sum, sum_tensor, tensor_sum, comp_tensor_id, tensorIso_hom,
  leftDistributor_hom, rightDistributor_hom, biproduct.mapIso_hom, biproduct.ι_map, biproduct.ι_π,
  Finset.sum_dite_irrel, Finset.sum_dite_eq', Finset.sum_const_zero, Finset.mem_univ, if_true]
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
Y : C
j✝ : J
⊢ ∑ x : J,
      ((𝟙 X ⊗ biproduct.π f x) ⊗ 𝟙 Y) ≫
        (biproduct.ι (fun j => X ⊗ f j) x ⊗ 𝟙 Y) ≫ (biproduct.π (fun j => X ⊗ f j) j✝ ⊗ 𝟙 Y) =
    ∑ x : J,
      (α_ X (⨁ f) Y).hom ≫
        (𝟙 X ⊗ (biproduct.π f x ⊗ 𝟙 Y) ≫ biproduct.ι (fun j => f j ⊗ Y) x) ≫
          (𝟙 X ⊗ biproduct.π (fun j => f j ⊗ Y) j✝) ≫ (α_ X (f j✝) Y).inv
[PROOFSTEP]
simp only [← comp_tensor_id, ← id_tensor_comp_assoc, Category.assoc, biproduct.ι_π, comp_dite, dite_comp, tensor_dite,
  dite_tensor]
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
Y : C
j✝ : J
⊢ (∑ x : J,
      if h : x = j✝ then (𝟙 X ⊗ biproduct.π f x) ≫ eqToHom (_ : X ⊗ f x = X ⊗ f j✝) ⊗ 𝟙 Y
      else (𝟙 X ⊗ biproduct.π f x) ≫ 0 ⊗ 𝟙 Y) =
    ∑ x : J,
      if h : x = j✝ then
        (α_ X (⨁ f) Y).hom ≫ (𝟙 X ⊗ (biproduct.π f x ⊗ 𝟙 Y) ≫ eqToHom (_ : f x ⊗ Y = f j✝ ⊗ Y)) ≫ (α_ X (f j✝) Y).inv
      else (α_ X (⨁ f) Y).hom ≫ (𝟙 X ⊗ (biproduct.π f x ⊗ 𝟙 Y) ≫ 0) ≫ (α_ X (f j✝) Y).inv
[PROOFSTEP]
simp only [Category.comp_id, Category.id_comp, Category.assoc, id_tensor_comp, comp_zero, zero_comp,
  MonoidalPreadditive.tensor_zero, MonoidalPreadditive.zero_tensor, comp_tensor_id, eqToHom_refl, tensor_id, if_true,
  dif_ctx_congr, Finset.sum_congr, Finset.mem_univ, Finset.sum_dite_eq']
[GOAL]
case w.w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
Y : C
j✝ : J
⊢ (𝟙 X ⊗ biproduct.π f j✝) ⊗ 𝟙 Y = (α_ X (⨁ f) Y).hom ≫ (𝟙 X ⊗ biproduct.π f j✝ ⊗ 𝟙 Y) ≫ (α_ X (f j✝) Y).inv
[PROOFSTEP]
simp only [associator_inv_naturality, Iso.hom_inv_id_assoc]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⊗ ⨁ f ⟶ Y
w : ∀ (j : J), (𝟙 X ⊗ biproduct.ι f j) ≫ g = (𝟙 X ⊗ biproduct.ι f j) ≫ h
⊢ g = h
[PROOFSTEP]
apply (cancel_epi (leftDistributor X f).inv).mp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⊗ ⨁ f ⟶ Y
w : ∀ (j : J), (𝟙 X ⊗ biproduct.ι f j) ≫ g = (𝟙 X ⊗ biproduct.ι f j) ≫ h
⊢ (leftDistributor X f).inv ≫ g = (leftDistributor X f).inv ≫ h
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⊗ ⨁ f ⟶ Y
w : ∀ (j : J), (𝟙 X ⊗ biproduct.ι f j) ≫ g = (𝟙 X ⊗ biproduct.ι f j) ≫ h
j✝ : J
⊢ biproduct.ι (fun j => X ⊗ f j) j✝ ≫ (leftDistributor X f).inv ≫ g =
    biproduct.ι (fun j => X ⊗ f j) j✝ ≫ (leftDistributor X f).inv ≫ h
[PROOFSTEP]
simp? [leftDistributor_inv, Preadditive.comp_sum_assoc, biproduct.ι_π_assoc,
    dite_comp] says simp only [leftDistributor_inv, Preadditive.comp_sum_assoc, ne_eq, biproduct.ι_π_assoc, dite_comp,
    zero_comp, Finset.sum_dite_eq, Finset.mem_univ, eqToHom_refl, Category.id_comp, ite_true]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⊗ ⨁ f ⟶ Y
w : ∀ (j : J), (𝟙 X ⊗ biproduct.ι f j) ≫ g = (𝟙 X ⊗ biproduct.ι f j) ≫ h
j✝ : J
⊢ biproduct.ι (fun j => X ⊗ f j) j✝ ≫ (leftDistributor X f).inv ≫ g =
    biproduct.ι (fun j => X ⊗ f j) j✝ ≫ (leftDistributor X f).inv ≫ h
[PROOFSTEP]
simp only [leftDistributor_inv, Preadditive.comp_sum_assoc, ne_eq, biproduct.ι_π_assoc, dite_comp, zero_comp,
  Finset.sum_dite_eq, Finset.mem_univ, eqToHom_refl, Category.id_comp, ite_true]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⊗ ⨁ f ⟶ Y
w : ∀ (j : J), (𝟙 X ⊗ biproduct.ι f j) ≫ g = (𝟙 X ⊗ biproduct.ι f j) ≫ h
j✝ : J
⊢ (𝟙 X ⊗ biproduct.ι f j✝) ≫ g = (𝟙 X ⊗ biproduct.ι f j✝) ≫ h
[PROOFSTEP]
apply w
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⟶ Y ⊗ ⨁ f
w : ∀ (j : J), g ≫ (𝟙 Y ⊗ biproduct.π f j) = h ≫ (𝟙 Y ⊗ biproduct.π f j)
⊢ g = h
[PROOFSTEP]
apply (cancel_mono (leftDistributor Y f).hom).mp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⟶ Y ⊗ ⨁ f
w : ∀ (j : J), g ≫ (𝟙 Y ⊗ biproduct.π f j) = h ≫ (𝟙 Y ⊗ biproduct.π f j)
⊢ g ≫ (leftDistributor Y f).hom = h ≫ (leftDistributor Y f).hom
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⟶ Y ⊗ ⨁ f
w : ∀ (j : J), g ≫ (𝟙 Y ⊗ biproduct.π f j) = h ≫ (𝟙 Y ⊗ biproduct.π f j)
j✝ : J
⊢ (g ≫ (leftDistributor Y f).hom) ≫ biproduct.π (fun j => Y ⊗ f j) j✝ =
    (h ≫ (leftDistributor Y f).hom) ≫ biproduct.π (fun j => Y ⊗ f j) j✝
[PROOFSTEP]
simp? [leftDistributor_hom, Preadditive.sum_comp, Preadditive.comp_sum_assoc, biproduct.ι_π,
    comp_dite] says simp only [leftDistributor_hom, Category.assoc, Preadditive.sum_comp, ne_eq, biproduct.ι_π,
    comp_dite, comp_zero, Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, ite_true]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⟶ Y ⊗ ⨁ f
w : ∀ (j : J), g ≫ (𝟙 Y ⊗ biproduct.π f j) = h ≫ (𝟙 Y ⊗ biproduct.π f j)
j✝ : J
⊢ (g ≫ (leftDistributor Y f).hom) ≫ biproduct.π (fun j => Y ⊗ f j) j✝ =
    (h ≫ (leftDistributor Y f).hom) ≫ biproduct.π (fun j => Y ⊗ f j) j✝
[PROOFSTEP]
simp only [leftDistributor_hom, Category.assoc, Preadditive.sum_comp, ne_eq, biproduct.ι_π, comp_dite, comp_zero,
  Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, ite_true]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y : C
f : J → C
g h : X ⟶ Y ⊗ ⨁ f
w : ∀ (j : J), g ≫ (𝟙 Y ⊗ biproduct.π f j) = h ≫ (𝟙 Y ⊗ biproduct.π f j)
j✝ : J
⊢ g ≫ (𝟙 Y ⊗ biproduct.π f j✝) = h ≫ (𝟙 Y ⊗ biproduct.π f j✝)
[PROOFSTEP]
apply w
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⊗ Y ⊗ ⨁ f ⟶ Z
w : ∀ (j : J), (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.ι f j) ≫ g = (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.ι f j) ≫ h
⊢ g = h
[PROOFSTEP]
apply (cancel_epi (α_ _ _ _).hom).mp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⊗ Y ⊗ ⨁ f ⟶ Z
w : ∀ (j : J), (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.ι f j) ≫ g = (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.ι f j) ≫ h
⊢ (α_ X Y (⨁ f)).hom ≫ g = (α_ X Y (⨁ f)).hom ≫ h
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⊗ Y ⊗ ⨁ f ⟶ Z
w : ∀ (j : J), (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.ι f j) ≫ g = (𝟙 X ⊗ 𝟙 Y ⊗ biproduct.ι f j) ≫ h
j✝ : J
⊢ (𝟙 (X ⊗ Y) ⊗ biproduct.ι f j✝) ≫ (α_ X Y (⨁ f)).hom ≫ g = (𝟙 (X ⊗ Y) ⊗ biproduct.ι f j✝) ≫ (α_ X Y (⨁ f)).hom ≫ h
[PROOFSTEP]
simp_rw [← tensor_id, associator_naturality_assoc, w]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⟶ Y ⊗ Z ⊗ ⨁ f
w : ∀ (j : J), g ≫ (𝟙 Y ⊗ 𝟙 Z ⊗ biproduct.π f j) = h ≫ (𝟙 Y ⊗ 𝟙 Z ⊗ biproduct.π f j)
⊢ g = h
[PROOFSTEP]
apply (cancel_mono (α_ _ _ _).inv).mp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⟶ Y ⊗ Z ⊗ ⨁ f
w : ∀ (j : J), g ≫ (𝟙 Y ⊗ 𝟙 Z ⊗ biproduct.π f j) = h ≫ (𝟙 Y ⊗ 𝟙 Z ⊗ biproduct.π f j)
⊢ g ≫ (α_ Y Z (⨁ f)).inv = h ≫ (α_ Y Z (⨁ f)).inv
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X Y Z : C
f : J → C
g h : X ⟶ Y ⊗ Z ⊗ ⨁ f
w : ∀ (j : J), g ≫ (𝟙 Y ⊗ 𝟙 Z ⊗ biproduct.π f j) = h ≫ (𝟙 Y ⊗ 𝟙 Z ⊗ biproduct.π f j)
j✝ : J
⊢ (g ≫ (α_ Y Z (⨁ f)).inv) ≫ (𝟙 (Y ⊗ Z) ⊗ biproduct.π f j✝) = (h ≫ (α_ Y Z (⨁ f)).inv) ≫ (𝟙 (Y ⊗ Z) ⊗ biproduct.π f j✝)
[PROOFSTEP]
simp_rw [← tensor_id, Category.assoc, ← associator_inv_naturality, ← Category.assoc, w]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), (biproduct.ι f j ⊗ 𝟙 X) ≫ g = (biproduct.ι f j ⊗ 𝟙 X) ≫ h
⊢ g = h
[PROOFSTEP]
apply (cancel_epi (rightDistributor f X).inv).mp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), (biproduct.ι f j ⊗ 𝟙 X) ≫ g = (biproduct.ι f j ⊗ 𝟙 X) ≫ h
⊢ (rightDistributor f X).inv ≫ g = (rightDistributor f X).inv ≫ h
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), (biproduct.ι f j ⊗ 𝟙 X) ≫ g = (biproduct.ι f j ⊗ 𝟙 X) ≫ h
j✝ : J
⊢ biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv ≫ g =
    biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv ≫ h
[PROOFSTEP]
simp? [rightDistributor_inv, Preadditive.comp_sum_assoc, biproduct.ι_π_assoc,
    dite_comp] says simp only [rightDistributor_inv, Preadditive.comp_sum_assoc, ne_eq, biproduct.ι_π_assoc, dite_comp,
    zero_comp, Finset.sum_dite_eq, Finset.mem_univ, eqToHom_refl, Category.id_comp, ite_true]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), (biproduct.ι f j ⊗ 𝟙 X) ≫ g = (biproduct.ι f j ⊗ 𝟙 X) ≫ h
j✝ : J
⊢ biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv ≫ g =
    biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv ≫ h
[PROOFSTEP]
simp only [rightDistributor_inv, Preadditive.comp_sum_assoc, ne_eq, biproduct.ι_π_assoc, dite_comp, zero_comp,
  Finset.sum_dite_eq, Finset.mem_univ, eqToHom_refl, Category.id_comp, ite_true]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : (⨁ f) ⊗ X ⟶ Y
w : ∀ (j : J), (biproduct.ι f j ⊗ 𝟙 X) ≫ g = (biproduct.ι f j ⊗ 𝟙 X) ≫ h
j✝ : J
⊢ (biproduct.ι f j✝ ⊗ 𝟙 X) ≫ g = (biproduct.ι f j✝ ⊗ 𝟙 X) ≫ h
[PROOFSTEP]
apply w
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : X ⟶ (⨁ f) ⊗ Y
w : ∀ (j : J), g ≫ (biproduct.π f j ⊗ 𝟙 Y) = h ≫ (biproduct.π f j ⊗ 𝟙 Y)
⊢ g = h
[PROOFSTEP]
apply (cancel_mono (rightDistributor f Y).hom).mp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : X ⟶ (⨁ f) ⊗ Y
w : ∀ (j : J), g ≫ (biproduct.π f j ⊗ 𝟙 Y) = h ≫ (biproduct.π f j ⊗ 𝟙 Y)
⊢ g ≫ (rightDistributor f Y).hom = h ≫ (rightDistributor f Y).hom
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : X ⟶ (⨁ f) ⊗ Y
w : ∀ (j : J), g ≫ (biproduct.π f j ⊗ 𝟙 Y) = h ≫ (biproduct.π f j ⊗ 𝟙 Y)
j✝ : J
⊢ (g ≫ (rightDistributor f Y).hom) ≫ biproduct.π (fun j => f j ⊗ Y) j✝ =
    (h ≫ (rightDistributor f Y).hom) ≫ biproduct.π (fun j => f j ⊗ Y) j✝
[PROOFSTEP]
simp? [rightDistributor_hom, Preadditive.sum_comp, Preadditive.comp_sum_assoc, biproduct.ι_π,
    comp_dite] says simp only [rightDistributor_hom, Category.assoc, Preadditive.sum_comp, ne_eq, biproduct.ι_π,
    comp_dite, comp_zero, Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, ite_true]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : X ⟶ (⨁ f) ⊗ Y
w : ∀ (j : J), g ≫ (biproduct.π f j ⊗ 𝟙 Y) = h ≫ (biproduct.π f j ⊗ 𝟙 Y)
j✝ : J
⊢ (g ≫ (rightDistributor f Y).hom) ≫ biproduct.π (fun j => f j ⊗ Y) j✝ =
    (h ≫ (rightDistributor f Y).hom) ≫ biproduct.π (fun j => f j ⊗ Y) j✝
[PROOFSTEP]
simp only [rightDistributor_hom, Category.assoc, Preadditive.sum_comp, ne_eq, biproduct.ι_π, comp_dite, comp_zero,
  Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, ite_true]
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y : C
g h : X ⟶ (⨁ f) ⊗ Y
w : ∀ (j : J), g ≫ (biproduct.π f j ⊗ 𝟙 Y) = h ≫ (biproduct.π f j ⊗ 𝟙 Y)
j✝ : J
⊢ g ≫ (biproduct.π f j✝ ⊗ 𝟙 Y) = h ≫ (biproduct.π f j✝ ⊗ 𝟙 Y)
[PROOFSTEP]
apply w
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z
w : ∀ (j : J), ((biproduct.ι f j ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫ g = ((biproduct.ι f j ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫ h
⊢ g = h
[PROOFSTEP]
apply (cancel_epi (α_ _ _ _).inv).mp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z
w : ∀ (j : J), ((biproduct.ι f j ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫ g = ((biproduct.ι f j ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫ h
⊢ (α_ (⨁ f) X Y).inv ≫ g = (α_ (⨁ f) X Y).inv ≫ h
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z
w : ∀ (j : J), ((biproduct.ι f j ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫ g = ((biproduct.ι f j ⊗ 𝟙 X) ⊗ 𝟙 Y) ≫ h
j✝ : J
⊢ (biproduct.ι f j✝ ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ (⨁ f) X Y).inv ≫ g = (biproduct.ι f j✝ ⊗ 𝟙 (X ⊗ Y)) ≫ (α_ (⨁ f) X Y).inv ≫ h
[PROOFSTEP]
simp_rw [← tensor_id, associator_inv_naturality_assoc, w]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z
w : ∀ (j : J), g ≫ ((biproduct.π f j ⊗ 𝟙 Y) ⊗ 𝟙 Z) = h ≫ ((biproduct.π f j ⊗ 𝟙 Y) ⊗ 𝟙 Z)
⊢ g = h
[PROOFSTEP]
apply (cancel_mono (α_ _ _ _).hom).mp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z
w : ∀ (j : J), g ≫ ((biproduct.π f j ⊗ 𝟙 Y) ⊗ 𝟙 Z) = h ≫ ((biproduct.π f j ⊗ 𝟙 Y) ⊗ 𝟙 Z)
⊢ g ≫ (α_ (⨁ f) Y Z).hom = h ≫ (α_ (⨁ f) Y Z).hom
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z
w : ∀ (j : J), g ≫ ((biproduct.π f j ⊗ 𝟙 Y) ⊗ 𝟙 Z) = h ≫ ((biproduct.π f j ⊗ 𝟙 Y) ⊗ 𝟙 Z)
j✝ : J
⊢ (g ≫ (α_ (⨁ f) Y Z).hom) ≫ (biproduct.π f j✝ ⊗ 𝟙 (Y ⊗ Z)) = (h ≫ (α_ (⨁ f) Y Z).hom) ≫ (biproduct.π f j✝ ⊗ 𝟙 (Y ⊗ Z))
[PROOFSTEP]
simp_rw [← tensor_id, Category.assoc, ← associator_naturality, ← Category.assoc, w]
