∀ {G : Type u_6} [inst : Group G] [inst_1 : SizeOf G] (toGroupSeminorm : GroupSeminorm G)
  (eq_one_of_map_eq_zero' : ∀ (x : G), toGroupSeminorm.toFun x = 0 → x = 1),
  sizeOf { toGroupSeminorm := toGroupSeminorm, eq_one_of_map_eq_zero' := eq_one_of_map_eq_zero' } =
    1 + sizeOf toGroupSeminorm