-- 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
M : Mat_ C
i : M.ι
⊢ Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, max 1 u₁}
      (biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
      (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
    (CategoryStruct.comp.{v₁, max 1 u₁} (Y :=
      biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
      (CategoryStruct.comp.{v₁, max 1 u₁} (Y := M)
        (biproduct.desc.{0, v₁, max 1 u₁}
          fun (i : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) (k : M.ι) ↦
          if h : i = k then eqToHom ⋯ else 0)
        (biproduct.lift.{0, v₁, max 1 u₁}
          fun (i j : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) ↦
          if h : j = i then eqToHom ⋯ else 0))
      (biproduct.π.{0, v₁, max 1 u₁} (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) i))
    (CategoryStruct.comp.{v₁, max 1 u₁}
      (CategoryStruct.id.{v₁, max 1 u₁}
        (biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
      (biproduct.π.{0, v₁, max 1 u₁} (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) i))
have w : ∀ (j : M.ι),
  Eq.{v₁ + 1} (α :=
    Quiver.Hom.{v₁, max 1 u₁} (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
      (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
    (CategoryStruct.comp.{v₁, max 1 u₁} (Y :=
        biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
        (biproduct.ι.{0, v₁, max 1 u₁} (C := Mat_ C)
          (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) j)
        (CategoryStruct.comp.{v₁, max 1 u₁} (Y :=
          biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
          (CategoryStruct.comp.{v₁, max 1 u₁} (Y := M)
            (biproduct.desc.{0, v₁, max 1 u₁}
              fun (i : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) (k : M.ι) ↦
              if h : i = k then eqToHom sorry else 0)
            (biproduct.lift.{0, v₁, max 1 u₁}
              fun (i j : M.ι) (x : (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)).ι) ↦
              if h : j = i then eqToHom sorry else 0))
          (biproduct.π.{0, v₁, max 1 u₁} (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
            i)) :
      Quiver.Hom.{v₁, max 1 u₁} (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
        (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
    (CategoryStruct.comp.{v₁, max 1 u₁} (Y :=
        biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
        (biproduct.ι.{0, v₁, max 1 u₁} (C := Mat_ C)
          (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)) j)
        (CategoryStruct.comp.{v₁, max 1 u₁}
          (CategoryStruct.id.{v₁, max 1 u₁}
            (biproduct.{0, v₁, max 1 u₁} fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
          (biproduct.π.{0, v₁, max 1 u₁} (fun (i : M.ι) ↦ Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i))
            i)) :
      Quiver.Hom.{v₁, max 1 u₁} (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X j))
        (Functor.obj.{v₁, v₁, u₁, max 1 u₁} (embedding C) (M.X i)))
Tactic: apply biproduct.hom_ext'