-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
inst_3 : Preadditive.{v₁, u₁} D
inst_4 : HasFiniteBiproducts.{v₁, u₁} D
F : Functor.{v₁, v₁, max 1 u₁, u₁} (Mat_ C) D
inst_5 : F.Additive
M N : Mat_ C
f : Quiver.Hom.{v₁, max 1 u₁} M N
i : N.ι
w :
  Eq (α :=
    (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ⟶
      F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)))
    (Iso.inv (additiveObjIsoBiproduct F M) ≫
        F.map f ≫ F.map fun (j : N.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0 :
      (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ⟶
        F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)))
    (biproduct.desc fun (j : M.ι) ↦ F.map (Functor.map (embedding C) (f j i)) :
      (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ⟶
        F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)))
⊢ CategoryStruct.comp (Y :=
      biproduct.{0, v₁, u₁} fun (i : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)))
      (F.map f ≫ Iso.hom (additiveObjIsoBiproduct F N) :
        F.obj M ⟶
          biproduct.{0, v₁, u₁} fun (i : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)))
      (biproduct.π (fun (i : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i))) i :
        (biproduct.{0, v₁, u₁} fun (i : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i))) ⟶
          F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i))) =
    CategoryStruct.comp (Y :=
      biproduct.{0, v₁, u₁} fun (i : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)))
      (CategoryStruct.comp (Y :=
          biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
          (Iso.hom (additiveObjIsoBiproduct F M) :
            F.obj M ⟶
              biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
          (biproduct.matrix fun (i : M.ι) (j : N.ι) ↦ F.map (Functor.map (embedding C) (f i j)) :
            Quiver.Hom.{v₁, u₁} (V := D)
              (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
              (biproduct.{0, v₁, u₁} fun (j : N.ι) ↦
                F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X j)))) :
        F.obj M ⟶
          biproduct.{0, v₁, u₁} fun (j : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X j)))
      (biproduct.π (fun (i : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i))) i :
        (biproduct.{0, v₁, u₁} fun (i : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i))) ⟶
          F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)))

Tactic:
simp only [Category.assoc, additiveObjIsoBiproduct_hom_π, isoBiproductEmbedding_hom,
    embedding_obj_ι, embedding_obj_X, biproduct.lift_π, biproduct.matrix_π,
    ← cancel_epi (additiveObjIsoBiproduct F M).inv, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Mat_.additiveObjIsoBiproduct_hom_π, CategoryTheory.Category.assoc, CategoryTheory.Mat_.embedding_obj_ι, CategoryTheory.Mat_.embedding_obj_X, CategoryTheory.Mat_.isoBiproductEmbedding_hom, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Limits.biproduct.matrix_π, CategoryTheory.Limits.biproduct.lift_π, CategoryTheory.Mat_.additiveObjIsoBiproduct, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv