This MR does the following:
auth_update_core_id to only require a fractional authority.
A few remarks/potential points of discussion:
core_id_local_update. It can't be used to prove the generalized
auth_update_core_id and it doesn't seem useful for anything else.
auth_update_core_id one could instead have added a new lemma. That would be consistent with
auth_both_frac_op. But, to me it seems like such a simple generalization/specialization is not worth two lemmas.
auth_update_core_id contains a bit of duplication in the two branches. I was not able to cut down on it (my attempts only resulted in larger proofs), but maybe someone else can