-- 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₁, u₁, u₁} C D
inst_5 : F.Additive
L : Functor.{v₁, v₁, max 1 u₁, u₁} (Mat_ C) D
inst_6 : L.Additive
α : embedding C ⋙ L ≅ F
X Y : Mat_ C
f : Quiver.Hom.{v₁, max 1 u₁} X Y
⊢ Eq (α := L.obj X ⟶ Functor.obj (lift F) Y)
    (CategoryStruct.comp (Y :=
      biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X i)))
      (Iso.hom (additiveObjIsoBiproduct L X) :
        L.obj X ⟶
          biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X i)))
      (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : Y.ι) ↦ (embedding C ⋙ lift F).obj (Y.X i))
          (biproduct.matrix fun (j : X.ι) (k : Y.ι) ↦
              L.map (Functor.map (embedding C) (f j k)) ≫
                Iso.hom (α.app (Y.X k)) ≫ Iso.hom (Iso.app (Iso.symm (embeddingLiftIso F)) (Y.X k)) :
            Quiver.Hom.{v₁, u₁} (V := D)
              (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X i)))
              (biproduct.{0, v₁, u₁} fun (i : Y.ι) ↦ (embedding C ⋙ lift F).obj (Y.X i)))
          (Iso.inv (additiveObjIsoBiproduct (lift F) Y) :
            (biproduct.{0, v₁, u₁} fun (i : Y.ι) ↦ (embedding C ⋙ lift F).obj (Y.X i)) ⟶ Functor.obj (lift F) Y) :
        (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X i))) ⟶
          Functor.obj (lift F) Y))
    (CategoryStruct.comp (Y :=
      biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X i)))
      (Iso.hom (additiveObjIsoBiproduct L X) :
        L.obj X ⟶
          biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X i)))
      (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
          (biproduct.map fun (b : X.ι) ↦ Iso.hom (α.app (X.X b)))
          (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ (embedding C ⋙ lift F).obj (X.X i))
            (biproduct.map fun (b : X.ι) ↦ Iso.hom (Iso.app (Iso.symm (embeddingLiftIso F)) (X.X b)) :
              Quiver.Hom.{v₁, u₁} (V := D) (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
                (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ (embedding C ⋙ lift F).obj (X.X i)))
            (Iso.inv (additiveObjIsoBiproduct (lift F) X) ≫ Functor.map (lift F) f :
              (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ (embedding C ⋙ lift F).obj (X.X i)) ⟶ Functor.obj (lift F) Y)) :
        (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X i))) ⟶
          Functor.obj (lift F) Y))
have simp : Eq (α := L.obj X ⟶ Functor.obj (lift F) Y)
  (CategoryStruct.comp (Y :=
    biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X i)))
    (Iso.hom (additiveObjIsoBiproduct L X) :
      L.obj X ⟶ biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X i)))
    (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : Y.ι) ↦ (embedding C ⋙ lift F).obj (Y.X i))
        (biproduct.matrix fun (j : X.ι) (k : Y.ι) ↦
            L.map (Functor.map (embedding C) (f j k)) ≫
              Iso.hom (α.app (Y.X k)) ≫ Iso.hom (Iso.app (Iso.symm (embeddingLiftIso F)) (Y.X k)) :
          Quiver.Hom.{v₁, u₁} (V := D)
            (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X i)))
            (biproduct.{0, v₁, u₁} fun (i : Y.ι) ↦ (embedding C ⋙ lift F).obj (Y.X i)))
        (Iso.inv (additiveObjIsoBiproduct (lift F) Y) :
          (biproduct.{0, v₁, u₁} fun (i : Y.ι) ↦ (embedding C ⋙ lift F).obj (Y.X i)) ⟶ Functor.obj (lift F) Y) :
      (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X i))) ⟶
        Functor.obj (lift F) Y))
  (CategoryStruct.comp (Y :=
    biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X i)))
    (Iso.hom (additiveObjIsoBiproduct L X) :
      L.obj X ⟶ biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X i)))
    (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
        (biproduct.map fun (b : X.ι) ↦ Iso.hom (α.app (X.X b)))
        (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ (embedding C ⋙ lift F).obj (X.X i))
          (biproduct.map fun (b : X.ι) ↦ Iso.hom (Iso.app (Iso.symm (embeddingLiftIso F)) (X.X b)) :
            Quiver.Hom.{v₁, u₁} (V := D) (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ F.obj (X.X i))
              (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ (embedding C ⋙ lift F).obj (X.X i)))
          (CategoryStruct.comp (Y :=
              biproduct.{0, v₁, u₁} fun (j : Y.ι) ↦
                Functor.obj (lift F) (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X j)))
              (biproduct.matrix fun (i : X.ι) (j : Y.ι) ↦ Functor.map (lift F) (Functor.map (embedding C) (f i j)) :
                Quiver.Hom.{v₁, u₁} (V := D)
                  (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦
                    Functor.obj (lift F) (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X i)))
                  (biproduct.{0, v₁, u₁} fun (j : Y.ι) ↦
                    Functor.obj (lift F) (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X j))))
              (Iso.inv (additiveObjIsoBiproduct (lift F) Y) :
                (biproduct.{0, v₁, u₁} fun (i : Y.ι) ↦
                    Functor.obj (lift F) (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X i))) ⟶
                  Functor.obj (lift F) Y) :
            (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦
                Functor.obj (lift F) (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X i))) ⟶
              Functor.obj (lift F) Y)) :
      (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X i))) ⟶
        Functor.obj (lift F) Y))
Tactic: simp only [additiveObjIsoBiproduct_naturality']