∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Semiring S] {I : Ideal R} [inst_2 : I.IsTwoSided] (f : R →+* S)
  (H : I ≤ RingHom.ker f), RingHom.ker (Ideal.Quotient.lift I f H) = Ideal.map (Ideal.Quotient.mk I) (RingHom.ker f)