∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {f : Polynomial R}
  [inst_3 : SizeOf R] [inst_4 : SizeOf S] (map : Polynomial R →ₐ[R] S) (map_surjective : Function.Surjective ⇑map)
  (ker_map : RingHom.ker map = Ideal.span {f}),
  sizeOf { map := map, map_surjective := map_surjective, ker_map := ker_map } = 1 + sizeOf map + sizeOf ker_map