∀ {R : Type u_3} {S : Type u_2} {T : Type u_1} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Semiring T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [Subsingleton T] (x x_1 : S),
  default (x * x_1) = default x * default x_1