mathlib3

c24f1f2b - chore(number_theory/padics/*): tidy some proofs (#13652)