-- 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
w :
  ∀ (i : N.ι),
    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)))
w₁ :
  ∀ (i : N.ι),
    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)))
w₂ :
  ∀ (i : N.ι) (j : M.ι),
    Eq (α :=
      F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)) ⟶
        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)))
        (biproduct.ι.{0, v₁, u₁} (C := D)
            (fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) j :
          F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)) ⟶
            biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.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))))
      (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)))
        (biproduct.ι.{0, v₁, u₁} (C := D)
          (fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) j)
        (biproduct.desc fun (j : M.ι) ↦ F.map (Functor.map (embedding C) (f j i))))
w₃ :
  ∀ (i : N.ι) (j : M.ι),
    Eq (α :=
      F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)) ⟶
        F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)))
      (F.map
        (CategoryStruct.comp.{v₁, max 1 u₁}
          (fun (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) (k : M.ι) ↦
            if h : j = k then eqToHom ⋯ else 0)
          (CategoryStruct.comp.{v₁, max 1 u₁} f fun (j : N.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0)))
      (F.map (Functor.map (embedding C) (f j i)))
w₄ :
  ∀ (i : N.ι) (j : M.ι),
    Eq (α :=
      Quiver.Hom.{v₁, max 1 u₁} (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
        (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)))
      (CategoryStruct.comp.{v₁, max 1 u₁}
        (fun (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) (k : M.ι) ↦
          if h : j = k then eqToHom ⋯ else 0)
        (CategoryStruct.comp.{v₁, max 1 u₁} f fun (j : N.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0))
      (Functor.map (embedding C) (f j i))
w₅ :
  ∀ (i : N.ι) (j : M.ι),
    Eq (α :=
      (fun (i_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι)
            (j_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)).ι) ↦
          Quiver.Hom.{v₁, u₁} ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).X i_1)
            ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)).X j_1))
        PUnit.unit PUnit.unit)
      (CategoryStruct.comp.{v₁, max 1 u₁}
          (fun (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι) (k : M.ι) ↦
            if h : j = k then eqToHom ⋯ else 0)
          (CategoryStruct.comp.{v₁, max 1 u₁} f fun (j : N.ι) (x : PUnit.{1}) ↦ if h : j = i then eqToHom ⋯ else 0)
          PUnit.unit PUnit.unit :
        (fun (i_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι)
              (j_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)).ι) ↦
            Quiver.Hom.{v₁, u₁} ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).X i_1)
              ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)).X j_1))
          PUnit.unit PUnit.unit)
      (Functor.map (embedding C) (f j i) PUnit.unit PUnit.unit :
        (fun (i_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).ι)
              (j_1 : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)).ι) ↦
            Quiver.Hom.{v₁, u₁} ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j)).X i_1)
              ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i)).X j_1))
          PUnit.unit PUnit.unit)
⊢ Eq (α :=
    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)))
    (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)))
    (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)))

Tactic:
classical
  ext i : 1
  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]
  ext j : 1
  simp only [ι_additiveObjIsoBiproduct_inv_assoc, isoBiproductEmbedding_inv,
    biproduct.ι_desc, ← F.map_comp]
  congr 1
  funext ⟨⟩ ⟨⟩
  simp [comp_apply, dite_comp, comp_dite]

Premises used: CategoryTheory.Mat_.additiveObjIsoBiproduct_hom_π, CategoryTheory.Category.assoc, CategoryTheory.Mat_.embedding_obj_ι, CategoryTheory.Mat_.ι_additiveObjIsoBiproduct_inv_assoc, CategoryTheory.Mat_.embedding_obj_X, CategoryTheory.dite_comp, CategoryTheory.Mat_.isoBiproductEmbedding_hom, CategoryTheory.Limits.biproduct.ι_desc, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Limits.biproduct.matrix_π, CategoryTheory.Mat_.isoBiproductEmbedding_inv, CategoryTheory.Mat_.comp_apply, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.biproduct.lift_π, CategoryTheory.Mat_.additiveObjIsoBiproduct, CategoryTheory.cancel_epi, CategoryTheory.comp_dite, CategoryTheory.Iso.inv