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