chore: attribute [induction_eliminator]

[astrainfinita]

Add attribute [induction_eliminator] to AddOpposite.rec' AdjoinRoot.induction_on Cycle.induction_on ENat.recTopCoe ENNReal.recTopCoe EReal.rec Finset.induction FreeAlgebra.induction FreeAddMagma.recOnAdd FreeAddMonoid.recOn FreeAddSemigroup.recOnAdd FreeCommRing.induction_on FreeSemigroup.recOnMul FreeMagma.recOnMul FreeMonoid.recOn LocalizedModule.induction_on Magma.AssocQuotient.induction_on ManyOneDegree.ind_on Module.Ray.ind (and add Orientation.ind for Orientation, an abbrev of it. I wish that we do not need to add it in the future.) MulOpposite.rec' Multiset.induction MvPolynomial.induction_on OnePoint.rec Opposite.rec' Ordinal.limitRecOn OreLocalization.ind PartENat.casesOn Polynomial.induction_on' Projectivization.ind QuotientAddGroup.induction_on' (and add AddCircle.induction_on for AddCircle, an abbrev of it. I wish that we do not need to add it in the future.) QuotientGroup.induction_on' (doesn't actually work) Real.Angle.induction_on SimplexCategory.rec Specialization.rec Sym2.ind TensorProduct.induction_on TrivSqZeroExt.ind Trunc.induction_on Unitization.ind

---

[urkud]

Does it make induction use these theorems by default? Should Finset default to cons_induction?

[eric-wieser]

193 files is pretty large to review; can this be split? I've made #13096 for the really basic WithX cases.

[eric-wieser]

Another good split would be all the Free constructions.

[urkud]

I'm merging master.

[urkud]

I cherry-picked parts about WithTop/WithBot-based types to #13264

[eric-wieser]

Should Finset default to cons_induction?

I think this kind of question is what makes this PR currently hard to review. Some types have only one induction principle, so this change is clearly good. Others have multiple, and I think we should review those separately to decide which one is the one true principle.

I think Finset and Polynomial/MvPolynomial fall into this category.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#13476~~
• ~~leanprover-community/mathlib4#13264~~ By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

PR summary ded55f8c38

Import changes

No significant changes to the import graph

---

Declarations diff

+ Orientation.ind + induction_on

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[eric-wieser]

I've split off a few more: #14132, #14135, #14136.

[eric-wieser]

QuotientGroup.induction_on' (doesn't actually work)

https://github.com/leanprover/lean4/issues/4577

[eric-wieser]

193 files is pretty large to review

Now down to 140 files!

I think the Finset ones are possibly controversial; I'd much prefer cons_induction to be the default, but I suspect that stance is also controversial.

[YaelDillies]

What's the status here? I think this is a useful PR

[urkud]

@FR-vdash-bot What parts of this is not in master yet? Do you need help with merging master?