∀ {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} (hf : Function.Surjective ⇑f) (a : A),
  (Ideal.quotientKerAlgEquivOfSurjective hf).symm (f a) = (Ideal.Quotient.mk (RingHom.ker f)) a