mathlib

cf345987 - chore(tactic/norm_cast): minor cleanup (#10993)