∀ {I : Type u} {f : I → Type v} {γ : Type w} [Nonempty I] [inst : (i : I) → AddZeroClass (f i)]
  [inst_1 : AddZeroClass γ] (g : (i : I) → γ →+ f i),
  (∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(Pi.addMonoidHom g)