feat(Tactic/CategoryTheory): extend @[to_app] to natural transformations

[dagurtomas]

This extends the @[to_app] attribute so it also generates componentwise lemmas from equalities of natural transformations between functors, while preserving the existing bicategory behavior. It also ensures generated component lemmas remain usable by dsimp when they are definitionally true.

[github-actions]

PR summary bb325b73e4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ foo
+ inv_hom_id
+ markDefEqIfPossible
+ rflProof?
+ toAppAttributeExpr
+ unbundled_comp_assoc
+ unbundled_eq
+ unbundled_eq_of_eq

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.

---

No changes to technical debt.

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