∀ {F : Type u_3} {R : Type u_2} {S : Type u_1} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F) (s : NonUnitalSubring R) {a b : S},
  a ∈ (AddSubgroup.map (↑f) s.toAddSubgroup).carrier →
    b ∈ (AddSubgroup.map (↑f) s.toAddSubgroup).carrier → a + b ∈ (AddSubgroup.map (↑f) s.toAddSubgroup).carrier