∀ {M : Type u_3} [inst : Monoid M] {A : Type u_1} [inst_1 : AddMonoid A] [inst_2 : DistribMulAction M A] {B₁ : Type u_2}
  [inst_3 : AddMonoid B₁] [inst_4 : DistribMulAction M B₁], AddMonoidHomClass (A →+[M] B₁) A B₁