-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Mat (goal)
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
rw :
  F.map f =
    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)))
      (CategoryStruct.comp (Y :=
          biproduct.{0, v₁, u₁} fun (j : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X j)))
          (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))))
          (Iso.inv (additiveObjIsoBiproduct F N) :
            (biproduct.{0, v₁, u₁} fun (i : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i))) ⟶
              F.obj N) :
        (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ⟶
          F.obj N)
rw₁ :
  F.map f =
    CategoryStruct.comp (Y :=
      biproduct.{0, v₁, u₁} fun (j : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X j)))
      (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)))
      (Iso.inv (additiveObjIsoBiproduct F N) :
        (biproduct.{0, v₁, u₁} fun (i : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i))) ⟶
          F.obj N)
rw₂ :
  Eq (α :=
    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)))
    (F.map f ≫ Iso.hom (additiveObjIsoBiproduct F N) :
      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)))
    (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)))
⊢ 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 N)
    (Iso.inv (additiveObjIsoBiproduct F M) ≫ F.map f :
      (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ⟶
        F.obj N)
    (CategoryStruct.comp (Y :=
        biproduct.{0, v₁, u₁} fun (j : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X j)))
        (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))))
        (Iso.inv (additiveObjIsoBiproduct F N) :
          (biproduct.{0, v₁, u₁} fun (i : N.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (N.X i))) ⟶
            F.obj N) :
      (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ⟶
        F.obj N)
have rw₃ : Eq (α :=
  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)))
  (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)))
  (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: rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, additiveObjIsoBiproduct_naturality]