∀ {M : Type u_1} {P : Type u_2} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] (f : M →+* P)
  (n : (RingCon.ker f).Quotient), (Equiv.refl P) ↑((Setoid.quotientKerEquivRangeKerLift ⇑f) n) ∈ Set.range ⇑f