∀ {R₁ : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A]
  [inst_3 : Semiring B] [inst_4 : Algebra R₁ B] (f : A →ₐ[R₁] B) (a : A),
  (Ideal.kerLiftAlg f) ((Ideal.Quotient.mk (RingHom.ker f)) a) = f a