-- Module: Mathlib.CategoryTheory.Monoidal.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
inst_4 : HasFiniteBiproducts.{v_1, u_1} C
J : Type
inst_5 : Finite J
X : C
f : J → C
Y : C
val : Fintype J
intro :
  ∀ (j : J),
    Eq.{v_1 + 1} (α :=
      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ⟶
        tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
      (CategoryStruct.comp (Y :=
          biproduct.{0, v_1, u_1} fun (j : J) ↦
            tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
          (Iso.hom
              (Iso.trans (Y :=
                tensorObj.{v_1, u_1} (𝒞 := inst)
                  (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
                (leftDistributor X f ⊗ᵢ asIso (𝟙 Y) :
                  tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ≅
                    tensorObj.{v_1, u_1} (𝒞 := inst)
                      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
                (rightDistributor (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y :
                  tensorObj.{v_1, u_1} (𝒞 := inst)
                      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y ≅
                    biproduct.{0, v_1, u_1} fun (j : J) ↦
                      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)) :
            tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ⟶
              biproduct.{0, v_1, u_1} fun (j : J) ↦
                tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
          (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y) j :
            (biproduct.{0, v_1, u_1} fun (j : J) ↦
                tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y) ⟶
              tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y) :
        tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ⟶
          tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
      (CategoryStruct.comp (Y :=
          biproduct.{0, v_1, u_1} fun (j : J) ↦
            tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
          (Iso.hom
            (α_ X (biproduct.{0, v_1, u_1} f) Y ≪≫
              Iso.trans (Y :=
                tensorObj.{v_1, u_1} (𝒞 := inst) X
                  (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y))
                (asIso (𝟙 X) ⊗ᵢ rightDistributor f Y :
                  tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) Y) ≅
                    tensorObj.{v_1, u_1} (𝒞 := inst) X
                      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y))
                (Iso.trans (Y :=
                    biproduct.{0, v_1, u_1} fun (j : J) ↦
                      tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y))
                    (leftDistributor X fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y :
                      tensorObj.{v_1, u_1} (𝒞 := inst) X
                          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) ≅
                        biproduct.{0, v_1, u_1} fun (j : J) ↦
                          tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y))
                    (biproduct.mapIso fun (x : J) ↦ Iso.symm (α_ X (f x) Y) :
                      Iso.{v_1, u_1} (C := C)
                        (biproduct.{0, v_1, u_1} fun (j : J) ↦
                          tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y))
                        (biproduct.{0, v_1, u_1} fun (x : J) ↦
                          tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f x)) Y)) :
                  tensorObj.{v_1, u_1} (𝒞 := inst) X
                      (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) ≅
                    biproduct.{0, v_1, u_1} fun (x : J) ↦
                      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f x)) Y)))
          (biproduct.π (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
            j) :
        tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ⟶
          tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ≅
      biproduct.{0, v_1, u_1} fun (j : J) ↦
        tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
    (Iso.trans (Y :=
        tensorObj.{v_1, u_1} (𝒞 := inst)
          (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
        (leftDistributor X f ⊗ᵢ asIso (𝟙 Y) :
          tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ≅
            tensorObj.{v_1, u_1} (𝒞 := inst)
              (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
        (rightDistributor (fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y :
          tensorObj.{v_1, u_1} (𝒞 := inst)
              (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y ≅
            biproduct.{0, v_1, u_1} fun (j : J) ↦
              tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y) :
      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ≅
        biproduct.{0, v_1, u_1} fun (j : J) ↦
          tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f j)) Y)
    (α_ X (biproduct.{0, v_1, u_1} f) Y ≪≫
        Iso.trans (Y :=
          tensorObj.{v_1, u_1} (𝒞 := inst) X
            (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y))
          (asIso (𝟙 X) ⊗ᵢ rightDistributor f Y :
            tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) (biproduct.{0, v_1, u_1} f) Y) ≅
              tensorObj.{v_1, u_1} (𝒞 := inst) X
                (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y))
          (Iso.trans (Y :=
              biproduct.{0, v_1, u_1} fun (j : J) ↦
                tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y))
              (leftDistributor X fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y :
                tensorObj.{v_1, u_1} (𝒞 := inst) X
                    (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) ≅
                  biproduct.{0, v_1, u_1} fun (j : J) ↦
                    tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y))
              (biproduct.mapIso fun (x : J) ↦ Iso.symm (α_ X (f x) Y) :
                Iso.{v_1, u_1} (C := C)
                  (biproduct.{0, v_1, u_1} fun (j : J) ↦
                    tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y))
                  (biproduct.{0, v_1, u_1} fun (x : J) ↦
                    tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f x)) Y)) :
            tensorObj.{v_1, u_1} (𝒞 := inst) X
                (biproduct.{0, v_1, u_1} fun (j : J) ↦ tensorObj.{v_1, u_1} (𝒞 := inst) (f j) Y) ≅
              biproduct.{0, v_1, u_1} fun (x : J) ↦
                tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f x)) Y) :
      tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (biproduct.{0, v_1, u_1} f)) Y ≅
        biproduct.{0, v_1, u_1} fun (x : J) ↦
          tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X (f x)) Y)

Tactic:
ext