∀ (M : Type u_1) (N : Type u_2) (α : Type u_5) [inst : AddMonoid M] [inst_1 : AddMonoid N] [inst_2 : AddAction M α]
  [inst_3 : AddAction N α] [inst_4 : VAddCommClass M N α],
  AddAction.prodOfVAddCommClass M N α = { vadd := fun mn a => mn.1 +ᵥ mn.2 +ᵥ a, add_vadd := ⋯, zero_vadd := ⋯ }