-- Module: Mathlib.CategoryTheory.Preadditive.Mat
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
M : Mat_ C
i : M.ι
w :
  ∀ (j : M.ι),
    Eq.{v₁ + 1} (α :=
      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) (M.X i)))
      (CategoryStruct.comp.{v₁, max 1 u₁} (Y :=
          biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
          (biproduct.ι.{0, v₁, max 1 u₁} (C := Mat_ C)
            (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) j)
          (CategoryStruct.comp.{v₁, max 1 u₁} (Y :=
            biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
            (CategoryStruct.comp.{v₁, max 1 u₁} (Y := M)
              (biproduct.desc.{0, v₁, max 1 u₁}
                fun (i : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) (k : M.ι) ↦
                if h : i = k then eqToHom ⋯ else 0)
              (biproduct.lift.{0, v₁, max 1 u₁}
                fun (i j : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) ↦
                if h : j = i then eqToHom ⋯ else 0))
            (biproduct.π.{0, v₁, max 1 u₁} (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
              i)) :
        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) (M.X i)))
      (CategoryStruct.comp.{v₁, max 1 u₁} (Y :=
          biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
          (biproduct.ι.{0, v₁, max 1 u₁} (C := Mat_ C)
            (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) j)
          (CategoryStruct.comp.{v₁, max 1 u₁}
            (CategoryStruct.id.{v₁, max 1 u₁}
              (biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
            (biproduct.π.{0, v₁, max 1 u₁} (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
              i)) :
        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) (M.X i)))
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, max 1 u₁}
      (biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
      (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
    (CategoryStruct.comp.{v₁, max 1 u₁} (Y :=
      biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
      (CategoryStruct.comp.{v₁, max 1 u₁} (Y := M)
        (biproduct.desc.{0, v₁, max 1 u₁}
          fun (i : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) (k : M.ι) ↦
          if h : i = k then eqToHom ⋯ else 0)
        (biproduct.lift.{0, v₁, max 1 u₁}
          fun (i j : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) ↦
          if h : j = i then eqToHom ⋯ else 0))
      (biproduct.π.{0, v₁, max 1 u₁} (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) i))
    (CategoryStruct.comp.{v₁, max 1 u₁}
      (CategoryStruct.id.{v₁, max 1 u₁}
        (biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
      (biproduct.π.{0, v₁, max 1 u₁} (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) i))

Tactic:
apply biproduct.hom_ext'

Premises used: CategoryTheory.Limits.biproduct.hom_ext'