refactor(RepresentationTheory/FiniteIndex): simpler design of indToCoindAux using ind.lift

[JX-Mo]

This is split from #41808. We provide a simpler, shorter design of indToCoindAux employing the new API ind.lift. Radar shows dramatic speed up without deprecation from #41808
✅ build/module/Mathlib.RepresentationTheory.FiniteIndex//instructions: -19.9G (-46.11%) (reduced significance based on *//lines)

• depends on: refactor(RepresentationTheory/Coinduced): avoid unfolding resCoindHomEquiv and remove some tech debt #44249
• depends on: chore(RepresentationTheory): remove DecidableEq condition #44141
• depends on: refactor(RepresentationTheory/Induced): add induced representations API and remove tech debt #43949

[github-actions]

PR summary 38eeeebdf7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ IndV.inductionOn
+ IndV.lift
+ IndV.lift_apply_mk
+ IndV.mk_map_eq
+ IndV.mk_map_inv_eq
+ IndV.mk_map_inv_mul
+ IndV.mk_map_mul
+ coe_coindMap_apply
+ coe_coindMap_apply_apply
+ coe_coind_apply
+ coind.coe_lift_apply
+ coind.coe_unit_apply
+ coind.counit
+ coind.counit_apply
+ coind.evalOne
+ coind.evalOne_apply
+ coind.lift
+ coind.unit
+ coindToIndAux
+ coindToIndAux_mk
+ coinvariantsTensorIndInv_mk_tmul_indVMk
+ ind.lift
+ ind.lift_apply_mk
+ indCoindIso_hom_hom_toLinearMap
+ indCoindIso_inv_hom_toLinearMap
+ indToCoindAux_coe
+ indToCoindAux_coe_mul
+ indToCoindAux_mul_coe
+ indToCoindAux_of_notMem
+ indToCoindAux_one
+ indToCoind_apply_mk
+ ind_apply_mk
+ ind_conj_map_apply
+ instance : (coindFunctor.{max w u v} k S.subtype).IsLeftAdjoint
+ instance : AddCommGroup (IndV φ ρ) := inferInstanceAs <|
+ instance : CoeFun (coindV φ σ) (fun _ => H → A) := ⟨Subtype.val⟩
+ instance : Module k (IndV φ ρ) := inferInstanceAs <|
+ resCoindAdjunction_counit_app_hom_toLinearMap
+ resCoindAdjunction_homEquiv
+ resCoindAdjunction_unit_app_hom_toLinearMap
+ resCoindHomEquiv
+ resCoindHomEquiv_apply
+ resCoindHomEquiv_apply_hom
+ resCoindHomEquiv_symm_apply
+ resCoindHomEquiv_symm_apply_hom
++ coindToInd_apply
++- coindToInd
+-+ coindToInd_indToCoind
+-+ indToCoind
+-+ indToCoindAux
+-+ indToCoindAux_comm
+-+ indToCoind_coindToInd
- coindMap_coe_apply
- coindMap_coe_apply_apply
- instIsLeftAdjointSubtypeMemSubgroupCoindFunctorSubtype

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; merge master and push to refresh)

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

• +55 new declarations
• −3 removed declarations

-Rep.coindToInd.congr_simp
+Rep.coinvariantsTensorIndInv_mk_tmul_indVMk
+Rep.indCoindIso_hom
+Rep.indCoindIso_inv
+Rep.resCoindAdjunction_counit_app_hom_toLinearMap
+Rep.resCoindAdjunction_homEquiv
+Rep.resCoindAdjunction_unit_app_hom_toLinearMap
+Rep.resCoindHomEquiv_apply_hom
+Rep.resCoindHomEquiv_symm_apply_hom
+Rep.resFunctor_map
+Rep.resFunctor_obj
+Representation.IndV.inductionOn
+Representation.IndV.lift
+Representation.IndV.lift.congr_simp
+Representation.IndV.lift_apply_mk
+Representation.IndV.mk_map_eq
+Representation.IndV.mk_map_inv_eq
+Representation.IndV.mk_map_inv_mul
+Representation.IndV.mk_map_mul
+Representation.coe_coindMap_apply
+Representation.coe_coindMap_apply_apply
+Representation.coe_coind_apply
+Representation.coind.coe_lift_apply
+Representation.coind.coe_unit_apply
+Representation.coind.counit
+Representation.coind.counit_apply
+Representation.coind.evalOne
+Representation.coind.evalOne_apply
+Representation.coind.lift
+Representation.coind.unit
-Representation.coindMap_coe_apply
-Representation.coindMap_coe_apply_apply
+Representation.coindToInd
+Representation.coindToInd.congr_simp
+Representation.coindToIndAux
+Representation.coindToIndAux_mk
+Representation.coindToInd_apply
+Representation.coindToInd_indToCoind
+Representation.ind.lift
+Representation.ind.lift_apply_mk
+Representation.indToCoind
+Representation.indToCoindAux
+Representation.indToCoindAux_coe
+Representation.indToCoindAux_coe_mul
+Representation.indToCoindAux_comm
+Representation.indToCoindAux_mul_coe
+Representation.indToCoindAux_of_notMem
+Representation.indToCoindAux_one
+Representation.indToCoind_apply_mk
+Representation.indToCoind_coindToInd
+Representation.ind_apply_mk
+Representation.ind_conj_map_apply
+Representation.instAddCommGroupIndV
+Representation.instCoeFunSubtypeForallMemSubmoduleCoindV
+Representation.instModuleIndV
+Representation.resCoindHomEquiv
+Representation.resCoindHomEquiv_apply
+Representation.resCoindHomEquiv_symm_apply

---

Decrease in strong tech debt: (relative, absolute) = (2.66, 0.01)

Current number	Change	Type (strong)
4120	-7	backward.defeqAttrib.useBackward
2285	-10	backward.isDefEq.respectTransparency.types
389	-1	adaptation notes

No changes to weak technical debt.

Current commit 38eeeebdf7
Reference commit ed72f1faae

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 f43fbc1 against b63f6e8 are in. There are significant results. @JX-Mo

• ✅ build//instructions: -42.3G (-0.03%)

Large changes (1✅)

• ✅ build/module/Mathlib.RepresentationTheory.Induced//instructions: -28.5G (-41.12%)

Medium changes (1✅)

• ✅ build/module/Mathlib.RepresentationTheory.FiniteIndex//instructions: -9.1G (-21.16%)

Small changes (4✅)

• ✅ build/module/Mathlib.RepresentationTheory.Coinduced//instructions: -2.1G (-5.48%)
• ✅ build/module/Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality//instructions: -1.5G (-2.35%)
• ✅ build/module/Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro//instructions: -1.1G (-9.21%)
• ✅ build/module/Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality//instructions: -1.8G (-1.44%)

[mathlib-dependent-issues]

This PR/issue depends on:

• refactor(RepresentationTheory/Coinduced): avoid unfolding resCoindHomEquiv and remove some tech debt #44249
• chore(RepresentationTheory): remove DecidableEq condition #44141
• refactor(RepresentationTheory/Induced): add induced representations API and remove tech debt #43949
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

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