∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_2} [inst_1 : AddGroup H] (φ : G →+ H) (x y : G ⧸ φ.ker),
  (↑(QuotientAddGroup.kerLift φ)).toFun (x + y) =
    (↑(QuotientAddGroup.kerLift φ)).toFun x + (↑(QuotientAddGroup.kerLift φ)).toFun y