∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (N : AddSubgroup G) [nN : N.Normal]
  {φ : G →+ H} (hφ : Function.Surjective ⇑φ) (HN : N = φ.ker) (g : G), (QuotientAddGroup.liftEquiv N hφ HN) ↑g = φ g