∀ {M : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass P] (f : M →* P)
  (x y : (Con.ker f).Quotient),
  (↑(Con.kerLift f)).toFun (x * y) = (↑(Con.kerLift f)).toFun x * (↑(Con.kerLift f)).toFun y