mathlib3

d322063b - add comment explaining why `star_ring_aut_apply` is not a simp lemma