-- 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
j : X.ι
k : Y.ι
⊢ Eq (α :=
    L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X j)) ⟶
      F.obj ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X k)).X PUnit.unit))
    (CategoryStruct.comp (Y :=
      biproduct.{0, v₁, u₁} fun (i : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X k)).ι) ↦
        F.obj ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X k)).X i))
      (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)) :
        L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X j)) ⟶ (embedding C ⋙ lift F).obj (Y.X k))
      (biproduct.π
        (fun (i : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X k)).ι) ↦
          F.obj ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X k)).X i))
        PUnit.unit))
    (CategoryStruct.comp (Y :=
      biproduct.{0, v₁, u₁} fun (i : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X k)).ι) ↦
        F.obj ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X k)).X i))
      (Iso.hom (α.app (X.X j)) ≫
        CategoryStruct.comp (Y := (embedding C ⋙ lift F).obj (X.X j))
          (Iso.hom (Iso.app (Iso.symm (embeddingLiftIso F)) (X.X j)))
          (Functor.map (lift F) (Functor.map (embedding C) (f j k))))
      (biproduct.π
        (fun (i : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X k)).ι) ↦
          F.obj ((Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (Y.X k)).X i))
        PUnit.unit))
have e_a : Eq (α := L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X j)) ⟶ F.obj (Y.X k))
  (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : PUnit.{1}) ↦ F.obj (Y.X k))
      (L.map (Functor.map (embedding C) (f j k)) ≫
        α.hom.app (Y.X k) ≫ biproduct.lift fun (x : PUnit.{1}) ↦ 𝟙 (F.obj (Y.X k)))
      (biproduct.π (fun (i : PUnit.{1}) ↦ F.obj (Y.X k)) PUnit.unit) :
    L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X j)) ⟶ F.obj (Y.X k))
  (CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : PUnit.{1}) ↦ F.obj (Y.X k))
      (α.hom.app (X.X j) ≫
          CategoryStruct.comp (Y := biproduct.{0, v₁, u₁} fun (i : PUnit.{1}) ↦ F.obj (X.X j))
            (biproduct.lift fun (x : PUnit.{1}) ↦ 𝟙 (F.obj (X.X j)) :
              F.obj (X.X j) ⟶ biproduct.{0, v₁, u₁} fun (i : PUnit.{1}) ↦ F.obj (X.X j))
            (biproduct.matrix fun (i j_1 : PUnit.{1}) ↦ F.map (f j k) :
              Quiver.Hom.{v₁, u₁} (V := D) (biproduct.{0, v₁, u₁} fun (i : PUnit.{1}) ↦ F.obj (X.X j))
                (biproduct.{0, v₁, u₁} fun (i : PUnit.{1}) ↦ F.obj (Y.X k))) :
        L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X j)) ⟶
          biproduct.{0, v₁, u₁} fun (i : PUnit.{1}) ↦ F.obj (Y.X k))
      (biproduct.π (fun (i : PUnit.{1}) ↦ F.obj (Y.X k)) PUnit.unit :
        (biproduct.{0, v₁, u₁} fun (i : PUnit.{1}) ↦ F.obj (Y.X k)) ⟶ F.obj (Y.X k)) :
    L.obj (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (X.X j)) ⟶ F.obj (Y.X k))
Tactic: dsimp