Naturality of AddCommGrpCat.uliftZMultiplesAddEquiv

Mathlib's uliftZMultiplesAddEquiv G : (of (ULift ℤ) ⟶ G) ≃+ G is evaluation at 1, so it commutes with postcomposition. Mathlib states the equivalence but not this naturality, which the degree-zero comparison between Ext and sheaf cohomology uses.

theorem AddCommGrpCat.uliftZMultiplesAddEquiv_comp {G H : AddCommGrpCat} (φ : of (ULift.{u, 0} ℤ) ⟶ G) (g : G ⟶ H) : H.uliftZMultiplesAddEquiv (CategoryTheory.CategoryStruct.comp φ g) = (CategoryTheory.ConcreteCategory.hom g) (G.uliftZMultiplesAddEquiv φ)

uliftZMultiplesAddEquiv is evaluation at 1, so it is natural in the target.