refactor(RepresentationTheory/Induced): add induced representations API and remove tech debt

[JX-Mo]

We remove all set_option backward.isDefEq.respectTransparency.types false in from Representation.Induced and Representation.FiniteIndex, with significant performance improvement.

• depends on: chore(RepresentationTheory/Coinduced): tech debt #43948

[JX-Mo]

!radar

[leanprover-radar]

Benchmark results for d1596c3 against f0ab343 are in. There are significant results. @JX-Mo

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

Large changes (2✅)

• ✅ build/module/Mathlib.RepresentationTheory.FiniteIndex//instructions: -10.2G (-23.06%)
• ✅ build/module/Mathlib.RepresentationTheory.Induced//instructions: -25.7G (-36.05%)

Small changes (2✅)

• ✅ build/module/Mathlib.MeasureTheory.Measure.CharacteristicFunction//instructions: -74.3M (-1.60%)
• ✅ build/module/Mathlib.Tactic.GRewrite//instructions: -24.2M (-1.22%)

[github-actions]

PR summary accf3eb508

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
+ coind_apply_apply
+ coinvariantsTensorIndInv_mk_tmul_indVMk
+ ind.lift
+ ind.lift_apply_mk
+ indToCoind_mk
+ ind_apply_mk
+ ind_conj_map_apply
+ instance : AddCommGroup (IndV φ ρ) := inferInstanceAs <|
+ instance : Module k (IndV φ ρ) := inferInstanceAs <|

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)

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

• +17 new declarations
• −0 removed declarations

+Rep.coinvariantsTensorIndInv_mk_tmul_indVMk
+Rep.indToCoind_mk
+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.coind_apply_apply
+Representation.ind.lift
+Representation.ind.lift_apply_mk
+Representation.ind_apply_mk
+Representation.ind_conj_map_apply
+Representation.instAddCommGroupIndV
+Representation.instModuleIndV

---

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

Current number	Change	Type (strong)
backward.defeqAttrib.useBackward	4137	-6
backward.isDefEq.respectTransparency.types	2351	-10

No changes to weak technical debt.

Current commit accf3eb508
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).

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[JX-Mo]

One thing I don't understand is that simp [indToCoind_mk _] works but simp [indToCoind_mk] fails.

[mathlib-dependent-issues]

This PR/issue depends on:

• chore(RepresentationTheory/Coinduced): tech debt #43948
  By Dependent Issues (🤖). Happy coding!

[JX-Mo]

!radar

[leanprover-radar]

Benchmark results for b9071c1 against f0ab343 are in. There are significant results. @JX-Mo

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

Large changes (2✅)

• ✅ build/module/Mathlib.RepresentationTheory.FiniteIndex//instructions: -10.2G (-23.08%)
• ✅ build/module/Mathlib.RepresentationTheory.Induced//instructions: -28.5G (-39.92%)

Small changes (2✅)

• ✅ build/module/Mathlib.Tactic.Convert//instructions: -132.2M (-1.40%)
• ✅ build/module/Mathlib.Tactic.GRewrite//instructions: -25.1M (-1.26%)

[Whysoserioushah]

One thing I don't understand is that simp [indToCoind_mk _] works but simp [indToCoind_mk] fails.

because simp does some preprocessing before trying to simp on goal with given lemmas and giving it one empty input stop it from doing that

[JX-Mo]

Is there any chance to make it behave as normal simp lemmas? We have the same problem for resCoindToHom_hom_apply_coe in #43959

[JX-Mo]

One important observation is that with the help ind.lift the auxiliary data indToCoindAux can be largely simplified #41808, reporting even more dramatic speed up
✅ build/module/Mathlib.RepresentationTheory.FiniteIndex//instructions: -20.9G (-47.18%) (reduced significance based on *//lines)
I wonder if it makes sense to introduce the new design to this PR.