mathlib3

363a286b - chore(*): speedup slow proofs (#7148)

chore(*): speedup slow proofs (#7148) Some proofs using heavy `rfl` or heavy `obviously` can be sped up considerably. Done in this PR for some outstanding examples.