chore(RepresentationTheory/Coinduced): more tech debt

[JX-Mo]

No description provided.

[github-actions]

PR summary acb47f5b06

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ coe_coindMap_apply
+ coe_coindMap_apply_apply
+ coe_coind_apply
+ instance : CoeFun (coindV φ σ) (fun _ => H → A) := ⟨Subtype.val⟩
+ resCoindAdjunction_homEquiv
- coindMap_coe_apply
- coindMap_coe_apply_apply

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 -- stale, waiting for the new build)

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

• +4 new declarations
• −0 removed declarations

+Rep.resCoindAdjunction_counit_app_hom_toFun
+Rep.resCoindAdjunction_homEquiv
+Rep.resCoindAdjunction_unit_app_hom_toFun_coe
+Representation.coind_apply_apply

---

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

Current number	Change	Type (strong)
backward.isDefEq.respectTransparency.types	2356	-5
adaptation notes	394	-1

No changes to weak technical debt.

Current commit acb47f5b06
Reference commit f0ab343610

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

[JX-Mo]

!radar

[leanprover-radar]

Benchmark results for 9725ea0 against f0ab343 are in. No significant results found. @JX-Mo

• ✅ build//instructions: -8.4G (-0.01%)

Small changes (5✅)

• ✅ build/module/Mathlib.MeasureTheory.Measure.CharacteristicFunction//instructions: -76.9M (-1.65%)
• ✅ build/module/Mathlib.RepresentationTheory.Coinduced//instructions: -3.3G (-8.32%) (reduced significance based on *//lines)
• ✅ build/module/Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro//instructions: -712.6M (-5.51%)
• ✅ build/module/Mathlib.Tactic.Convert//instructions: -92.1M (-0.98%)
• ✅ build/module/Mathlib.Tactic.GRewrite//instructions: -23.6M (-1.19%)

[JX-Mo]

I am not completely sure about this -isSimp. It is here because it fires unnecessarily in FiniteIndex.lean

[JX-Mo]

The original raw rlfs are expensive

[JX-Mo]

ext does not fire directly, so I have to writeapply Rep.hom_ext (which is tagged @[ext] however). I didn't figure this out, but it works anyway

[JX-Mo]

WIP