∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (φ : G →* H) (ψ : H → G)
  (hφ : Function.RightInverse ψ ⇑φ) (a : G ⧸ φ.ker),
  (QuotientGroup.quotientKerEquivOfRightInverse φ ψ hφ) a = (QuotientGroup.kerLift φ) a