mathlib3

631890bf - chore(data/rat/basic): tidy some proofs (#13603)