∀ {R : Type u} [inst : Ring R] (M N : ModuleCat R) (x : ↑M × ↑N),
  (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.biprod.snd)
      ((CategoryTheory.ConcreteCategory.hom (M.biprodIsoProd N).inv) x) =
    x.2