∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Semiring S] {f : R →+* S} {g : S → R}
  (hf : Function.RightInverse g ⇑f) (x : R ⧸ RingHom.ker f), (RingHom.quotientKerEquivOfRightInverse hf) x = f.kerLift x