no goals
C : Type u₁
inst✝⁵ : Category C
inst✝⁴ : Preadditive C
D : Type u₁
inst✝³ : Category D
inst✝² : Preadditive D
inst✝¹ : HasFiniteBiproducts D
F : Mat_ C ⥤ D
inst✝ : Functor.Additive F
M N : Mat_ C
f : M ⟶ N
⊢ (additiveObjIsoBiproduct F M).inv ≫ F.map f =
    (biproduct.matrix fun i j => F.map ((embedding C).map (f i j))) ≫ (additiveObjIsoBiproduct F N).inv
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, additiveObjIsoBiproduct_naturality]