[Merged by Bors] - fix: Improve definition of SimplexCategoryGenRel.IsAdmissible

[linesthatinterlace]

Give SimplexCategoryGenRel.IsAdmissible an inductive definition equivalent to its prior definition.

---

When working on another PR, I noticed that the definition of SimplexCategoryGenRel.IsAdmissible could be substantially improved. In particular, it admits a nice natural inductive definition, which then obviously gives you the option of inducting on it directly, but just in general makes it much nicer and smoother to work with (and it isn't hard to prove it is equivalent to the previous definition).

I think there's probably more golfing one could do in this file but for now I've tried to do enough to demonstrate the value of the new definition at least.

[github-actions]

PR summary 2528a23415

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ IsAdmissible.simplicialEvalσ_succ_getElem
+ IsChain.cons
+ IsChain.of_cons
+ getElem_lt
+ isAdmissible_cons_cons_iff
+ isAdmissible_cons_iff
+ isAdmissible_iff_isChain_and_le
+ isAdmissible_iff_pairwise_and_le
+ isAdmissible_of_isChain_of_forall_getElem_le
+ isAdmissible_singleton_iff
+ isChain
+ mono
+ of_cons
+ pairwise
+ simplicialEvalσ_of_le_mem
- nil

You can run this locally as follows

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

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

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

---

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

Current number	Change	Type
4856	-1	exceptions for the docPrime linter

Current commit 0e7bf6534a
Reference commit 2528a23415

You can run this locally as

./scripts/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).

[robin-carlier]

Thanks!

This definitely improves some of the proofs, I could check that #21746 only needs minimal modifications for this, so that’s nice. #21747 needs a lot of refactor to adapt previous merges anyways, and makes almost no use of admissible lists, so things should be fine.

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[robin-carlier]

A few more minor nits + possible golfs, but basically looks good!

The merge conflict seems to come from some typos being fixed, so should be ok to resolve.

[robin-carlier]

Thanks!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by robin-carlier.

[joelriou]

Thanks!

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build
• Post-Build Step