∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  (∀ x ∈ RingHom.ker f, IsNilpotent x) →
    ∀ e₁ ∈ f.range,
      IsIdempotentElem e₁ →
        ∀ (e₂ : R),
          IsIdempotentElem e₂ →
            e₁ * f e₂ = 0 → f e₂ * e₁ = 0 → ∃ e', IsIdempotentElem e' ∧ f e' = e₁ ∧ e' * e₂ = 0 ∧ e₂ * e' = 0