refactor(Archive/FriendshipGraphs): golf everything

[Parcly-Taxel]

Also remove the file's set_options and @[expose]. Like #43434, no deprecations are added since this is a leaf file in Archive.

[github-actions]

PR summary dd0517510f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ IsFriendship
+ degree_le_two
+ exists_isUniversal_of_regular
+ isRegular_of_not_exists_isUniversal
- ExistsPolitician
- Friendship
- adjMatrix_mul_const_one_mod_p_of_regular
- adjMatrix_sq_mod_p_of_regular
- adjMatrix_sq_mul_const_one_of_regular
- card_mod_p_of_regular
- existsPolitician_of_degree_eq_two
- existsPolitician_of_degree_le_one
- existsPolitician_of_degree_le_two
- false_of_three_le_degree
- isRegularOf_not_existsPolitician
- neighborFinset_eq_of_degree_eq_two

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit dd05175).

• +0 new declarations
• −0 removed declarations

No declaration differences.

---

Decrease in strong tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (strong)
backward.isDefEq.respectTransparency	4678	-1
backward.isDefEq.respectTransparency.types	2429	-1

Decrease in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
exposed public sections	5058	-1

Current commit dd0517510f
Reference commit 2b0bd99647

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).