mathlib

297619ec - chore(number_theory/sum_four_squares): squeeze simps (#18461)

chore(number_theory/sum_four_squares): squeeze simps (#18461) This proof goes from 20s to 8s. Adding a missing `norm_cast` lemma makes it possible to replace some `simp`s with `push_cast`