∀ {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  (f : F) [RingHomClass F R S] (I : Ideal S) {x y : R}, x ∈ ⇑f ⁻¹' ↑I → y ∈ ⇑f ⁻¹' ↑I → x + y ∈ ⇑f ⁻¹' ↑I