∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀]
  [inst_2 : DecidablePred fun x => x = 0] [inst_3 : DecidablePred fun x => x = 0] (m : G₀) (n : H₀),
  Commute ((MonoidWithZeroHom.inl G₀ H₀) m) ((MonoidWithZeroHom.inr G₀ H₀) n)