∀ (R : Type u_1) [inst : CommRing R] {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S] {e f : S}
  (he : IsIdempotentElem e) (hf : IsIdempotentElem f) (hef₁ : e + f = 1) (hef₂ : e * f = 0) (a : S),
  ((AlgEquiv.prodQuotientOfIsIdempotentElem R he hf hef₁ hef₂) a).2 = (Ideal.Quotient.mk (Ideal.span {f})) a