feat(CategoryTheory): command that generates instances for MorphismProperty

[erdOne]

Co-authored-by: Calle Sönne

---

[github-actions]

PR summary 9f0a085912

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.MorphismProperty.Tactic (new file)	385

---

Declarations diff

+ Bar2
+ Config
+ ContainsIdentities
+ Foo.Bar
+ Foo.Bar3
+ IsStableUnderComposition
+ addMorphismPropertyInstancesAux
+ comp_mem
+ getArgs
+ hom
+ instance : ContainsIdentities (@Foo.Bar n) := ⟨fun _ ↦ ⟨inferInstance⟩⟩
+ instance : ContainsIdentities (@Foo.Bar3 C _) := ⟨fun _ ↦ ⟨⟩⟩
+ instance : IsStableUnderComposition (@Foo.Bar n) := ⟨fun _ _ _ _ ↦ ⟨inferInstance⟩⟩
+ instance : IsStableUnderComposition (@Foo.Bar3 C _) := ⟨fun _ _ _ _ ↦ ⟨⟩⟩
+ instance : IsStableUnderComposition @Foo.Bar2 := ⟨fun _ _ _ _ ↦ ⟨⟩⟩
+ instance : RespectsIso (@Foo.Bar n)
+ lemma1
+ lemma2
+ lemma3
+ of_isIso
+++ foo
+++ instance {X} : Bar (𝟙 X)

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.

---

No changes to technical debt.

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

[chrisflav]

This is very cool! Looking forward to using this. I left some small comments on the tests. Since I don't know anything about meta programming, I can't comment on the implementation.

[jcommelin]

@erdOne Do you think you could already demonstrate how this will be used in mathlib? Or should that wait for a follow up PR?

[erdOne]

It's #18784

[grunweg]

By the way: I think the CI failure would be fixed by merging master. (Sorry for the inconvenience, that's a one-time effect of a recent change to the script writing the "summary" comment on this PR.)
If you do so, your PR will even appear on the review queue.