chore(Combinatorics/SimpleGraph): avoid structure relation predicates

[YaelDillies]

Relation predicates used to be defs over a forall, which was optimal for usability in fields of other structures. This changed in #35591 and #35192 as a byproduct of reducing apparent code duplication. Unfortunately, the usability issue was overlooked.

This PR restores usability by dropping the use of those relation classes that are structures, ie Std.Irrefl and Std.Transitive. It also uses more widely the simp auto-param on SimpleGraph.loopless.

---

I would also be happy to revert #35591 and #35192 since this demonstrates a good use case for the def versions of the relation predicates.

[github-actions]

PR summary f7c1d6ebc9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ covBy_irrefl

You can run this locally as follows

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh 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).

[SnirBroshi]

Since this exists now, can you make this theorem produce an Std.Irrefl?

[SnirBroshi]

Can you elaborate on the issue with relation classes? I thought the only issue was that I didn't know we can write loopless.irrefl := ... in where when making #35191, and we can switch all constructions of SimpleGraphs to use that instead of angle brackets.

Also @Vierkantor said that Std.Irrefl is probably better than ∀ v, ¬ Adj v v, though I'm not sure what are the pros and cons.

[YaelDillies]

You can see from the diff that the predicate is largely more often unfolded than its API is used. Empirically, it is useful for the fields to be universal quantifiers, as then the variables can be introduced with where or given as arguments with no extra dot notation.

I get your point about loopless.irrefl, but I see the need for it as non-justifiable given how little it buys us compared to the loss of usability and discoverability.

I am teaching a Lean course in six months, which is why I am caring about usability and discoverability more now.