-- 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₁, 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
dsimp :
  Eq (α := L.obj X ⟶ Functor.obj (lift F) Y)
    (L.map f ≫
      CategoryStruct.comp (Y :=
        biproduct.{0, v₁, u₁} fun (i : Y.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X i)))
        (Iso.hom (additiveObjIsoBiproduct L Y) :
          L.obj Y ⟶
            biproduct.{0, v₁, u₁} fun (i : Y.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X i)))
        (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : Y.ι) ↦ F.obj (Y.X i))
            (biproduct.map fun (b : Y.ι) ↦ Iso.hom (α.app (Y.X b)))
            (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : Y.ι) ↦ (embedding C ⋙ lift F).obj (Y.X i))
              (biproduct.map fun (b : Y.ι) ↦ Iso.hom (Iso.app (Iso.symm (embeddingLiftIso F)) (Y.X b)) :
                Quiver.Hom.{v₁, u₁} (V := D) (biproduct.{0, v₁, u₁} fun (i : Y.ι) ↦ F.obj (Y.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 : Y.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.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) :
                (biproduct.{0, v₁, u₁} fun (i : X.ι) ↦ (embedding C ⋙ lift F).obj (X.X i)) ⟶ Functor.obj (lift F) X)) :
          (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) X) ≫
      Functor.map (lift F) f)
⊢ Eq (α := L.obj X ⟶ Functor.obj (lift F) Y)
    (L.map f ≫
      Iso.hom
        ((fun (M : Mat_ C) ↦
            (Iso.trans (Y :=
                biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
                (additiveObjIsoBiproduct L M :
                  L.obj M ≅
                    biproduct.{0, v₁, u₁} fun (i : M.ι) ↦
                      L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
                (Iso.trans (Y := biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (M.X i))
                    (biproduct.mapIso fun (i : M.ι) ↦ α.app (M.X i))
                    (Iso.trans (Y := biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ (embedding C ⋙ lift F).obj (M.X i))
                      (biproduct.mapIso fun (i : M.ι) ↦ Iso.app (Iso.symm (embeddingLiftIso F)) (M.X i) :
                        Iso.{v₁, u₁} (C := D) (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (M.X i))
                          (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ (embedding C ⋙ lift F).obj (M.X i)))
                      (Iso.symm (additiveObjIsoBiproduct (lift F) M) :
                        (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦
                            Functor.obj (lift F) (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ≅
                          Functor.obj (lift F) M)) :
                  (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦
                      L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ≅
                    Functor.obj (lift F) M) :
              L.obj M ≅ Functor.obj (lift F) M))
          Y))
    (Iso.hom
        ((fun (M : Mat_ C) ↦
            (Iso.trans (Y :=
                biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
                (additiveObjIsoBiproduct L M :
                  L.obj M ≅
                    biproduct.{0, v₁, u₁} fun (i : M.ι) ↦
                      L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
                (Iso.trans (Y := biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (M.X i))
                    (biproduct.mapIso fun (i : M.ι) ↦ α.app (M.X i))
                    (Iso.trans (Y := biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ (embedding C ⋙ lift F).obj (M.X i))
                      (biproduct.mapIso fun (i : M.ι) ↦ Iso.app (Iso.symm (embeddingLiftIso F)) (M.X i) :
                        Iso.{v₁, u₁} (C := D) (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ F.obj (M.X i))
                          (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦ (embedding C ⋙ lift F).obj (M.X i)))
                      (Iso.symm (additiveObjIsoBiproduct (lift F) M) :
                        (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦
                            Functor.obj (lift F) (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ≅
                          Functor.obj (lift F) M)) :
                  (biproduct.{0, v₁, u₁} fun (i : M.ι) ↦
                      L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))) ≅
                    Functor.obj (lift F) M) :
              L.obj M ≅ Functor.obj (lift F) M))
          X) ≫
      Functor.map (lift F) f)

Tactic:
dsimp only [Iso.trans_hom, Iso.symm_hom, biproduct.mapIso_hom]

Premises used: CategoryTheory.Limits.biproduct.mapIso_hom, CategoryTheory.Iso.symm_hom, CategoryTheory.Iso.trans_hom