∀ (R : Type u_2) [inst : Ring R] {X Y Z : FGModuleCat R} (f : X ⟶ Y) (g : Y ⟶ Z),
  FGModuleCat.ofHom
      (↑ULift.moduleEquiv.symm ∘ₗ
        ModuleCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g).hom ∘ₗ ↑ULift.moduleEquiv) =
    CategoryTheory.CategoryStruct.comp
      (FGModuleCat.ofHom (↑ULift.moduleEquiv.symm ∘ₗ ModuleCat.Hom.hom f.hom ∘ₗ ↑ULift.moduleEquiv))
      (FGModuleCat.ofHom (↑ULift.moduleEquiv.symm ∘ₗ ModuleCat.Hom.hom g.hom ∘ₗ ↑ULift.moduleEquiv))