∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] {s : NonUnitalSubring S} {f : F} {x : R},
  x ∈ NonUnitalSubring.comap f s ↔ f x ∈ s