∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {I J : TwoSidedIdeal R},
  { toFun := TwoSidedIdeal.ringCon, invFun := TwoSidedIdeal.mk, left_inv := ⋯, right_inv := ⋯ } I ≤
      { toFun := TwoSidedIdeal.ringCon, invFun := TwoSidedIdeal.mk, left_inv := ⋯, right_inv := ⋯ } J →
    ∀ x ∈ ↑I, x ∈ ↑J