{R : Type u} →
  {S : Type v} →
    {F : Type u_1} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : FunLike F R S] → (f : F) → [RingHomClass F R S] → Function.Bijective ⇑f → Ideal S ≃o Ideal R