mathlib

8eaeec26 - chore(a few random files): golfing using the new tactic `congrm` (#14593)

chore(a few random files): golfing using the new tactic `congrm` (#14593) This PR is simply intended to showcase some possible applications of the new tactic `congrm`, introduced in #14153. Co-authored-by: Gabriel Ebner <gebner@gebner.org>