chore: attribute [induction_eliminator] #12605

FR-vdash-bot · 2024-05-02T17:13:19Z

Add attribute [induction_eliminator] to
AdjoinRoot.induction_on
ENat.recTopCoe
ENNReal.recTopCoe
Finset.induction
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.)
Multiset.induction
MvPolynomial.induction_on
OnePoint.rec
Opposite.rec'
Ordinal.limitRecOn
PartENat.casesOn
Polynomial.induction_on'
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
Trunc.induction_on

FR-vdash-bot · 2024-05-02T18:21:42Z

Mathlib/Algebra/Group/WithOne/Basic.lean

@@ -119,13 +119,13 @@ theorem map_coe (f : α →ₙ* β) (a : α) : map f (a : WithOne α) = f a :=
 @[to_additive (attr := simp)]
 theorem map_id : map (MulHom.id α) = MonoidHom.id (WithOne α) := by
  ext x
-  induction x using WithOne.cases_on <;> rfl
+  induction x <;> rfl


We have WithOne.recOneCoe and WithZero.recZeroCoe. Can we just remove WithOne.cases_on and WithZero.cases_on?

urkud · 2024-05-19T22:45:32Z

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

eric-wieser · 2024-05-21T22:28:23Z

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

eric-wieser · 2024-05-21T22:32:28Z

Another good split would be all the Free constructions.

This is a smaller version of #12605. This allows `using` to be dropped from `induction`.

…ects (#14135) Namely, for * `FreeMagma` / `FreeAddMagma` * `FreeSemigroup` / `FreeAddSemigroup` * `FreeMonoid` / `FreeAddMonoid` * `FreeCommRing` * `FreeAlgebra` Split from #12605 Co-authored-by: negiizhao <[email protected]>

…on`} with `induction` and `cases` (#14132) Spit from #12605, which picked up some conflicts here. Co-authored-by: negiizhao [[email protected]](mailto:[email protected])

Split from #12605. Co-authored-by: negiizhao [email protected]

…ects (#14135) Namely, for * `FreeMagma` / `FreeAddMagma` * `FreeSemigroup` / `FreeAddSemigroup` * `FreeMonoid` / `FreeAddMonoid` * `FreeCommRing` * `FreeAlgebra` Split from #12605 Co-authored-by: negiizhao <[email protected]>

…on`} with `induction` and `cases` (#14132) Spit from #12605, which picked up some conflicts here. Co-authored-by: negiizhao [[email protected]](mailto:[email protected])

eric-wieser · 2024-06-27T19:59:04Z

QuotientGroup.induction_on' (doesn't actually work)

leanprover/lean4#4577

…le types (#14205) Namely: * `AList` * `Cycle` * `ConjAct` * `Projectivization` * `Lex` * `NatOrdinal` * `WithLawson` * `WithLower` * `WithUpper` * `WithScott` * `WithUpperSet` * `WithLowerSet` * `Speicalization` (which had an incorrectly-stated induction principle) These are just for the cases which have docstrings of the form "Use as `induction .* using .*`". Inspired by #12605.

Split from #12605

Split from #12605 Also cleans up some proofs that used `revert` instead of `induction`.

eric-wieser · 2024-06-30T21:33:04Z

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.

Split from #12605. Co-authored-by: negiizhao [email protected]

…ects (#14135) Namely, for * `FreeMagma` / `FreeAddMagma` * `FreeSemigroup` / `FreeAddSemigroup` * `FreeMonoid` / `FreeAddMonoid` * `FreeCommRing` * `FreeAlgebra` Split from #12605 Co-authored-by: negiizhao <[email protected]>

…on`} with `induction` and `cases` (#14132) Spit from #12605, which picked up some conflicts here. Co-authored-by: negiizhao [[email protected]](mailto:[email protected])

…le types (#14205) Namely: * `AList` * `Cycle` * `ConjAct` * `Projectivization` * `Lex` * `NatOrdinal` * `WithLawson` * `WithLower` * `WithUpper` * `WithScott` * `WithUpperSet` * `WithLowerSet` * `Speicalization` (which had an incorrectly-stated induction principle) These are just for the cases which have docstrings of the form "Use as `induction .* using .*`". Inspired by #12605.

Split from #12605

Split from #12605 Also cleans up some proofs that used `revert` instead of `induction`.

YaelDillies · 2025-01-23T08:36:57Z

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

chore: attribute [induction_eliminator]

9839531

FR-vdash-bot added the WIP Work in progress label May 2, 2024

FR-vdash-bot added 3 commits May 3, 2024 01:27

more

7cb4b9e

oops

2ba2115

more

9d917ea

FR-vdash-bot commented May 2, 2024

View reviewed changes

FR-vdash-bot added 4 commits May 4, 2024 00:32

fix

861900a

more

ae1436d

fix

6b964db

more

1efbb9e

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 3, 2024

Merge branch 'master' into FR_induction

c0e01e2

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 15, 2024

FR-vdash-bot added 2 commits May 16, 2024 12:07

fix

7d3bf6f

fix

ee673ce

FR-vdash-bot added awaiting-review awaiting-CI and removed WIP Work in progress labels May 16, 2024

github-actions bot removed the awaiting-CI label May 16, 2024

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 20, 2024

This was referenced May 21, 2024

feat(Algebra/Group/WithOne): add some API #13094

Closed

[Merged by Bors] - chore: add induction_eliminator to With{Top,Bot,Zero,One} #13096

Closed

Merge remote-tracking branch 'origin/master' into FR_induction

ddffab9

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 21, 2024

mathlib-bors bot pushed a commit that referenced this pull request May 22, 2024

chore: add induction_eliminator to With{Top,Bot,Zero,One} (#13096)

cdceebb

This is a smaller version of #12605. This allows `using` to be dropped from `induction`.

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 22, 2024

FR-vdash-bot removed the awaiting-review label May 22, 2024

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 26, 2024

Merge branch 'master' into FR_induction

1fe135a

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 26, 2024

Merge branch 'master' into FR_induction

7f35690

kbuzzard pushed a commit that referenced this pull request Jun 26, 2024

chore: register MulOpposite.rec with induction and cases (#14136)

c15f60a

Split from #12605. Co-authored-by: negiizhao [email protected]

This was referenced Jun 27, 2024

[Merged by Bors] - chore: register TensorProduct with induction_eliminator #14204

Closed

[Merged by Bors] - chore: add cases_eliminator and induction_eliminator to some simple types #14205

Closed

mathlib-bors bot pushed a commit that referenced this pull request Jun 30, 2024

chore: register TensorProduct with induction_eliminator (#14204)

69ed7ba

Split from #12605

Merge branch 'master' into FR_induction

25e538f

eric-wieser mentioned this pull request Jun 30, 2024

[Merged by Bors] - chore: register Sym2 with induction #14288

Closed

Merge remote-tracking branch 'origin/master' into FR_induction

4619254

mathlib-bors bot pushed a commit that referenced this pull request Jun 30, 2024

chore: register Sym2 with induction (#14288)

4e1da24

Split from #12605 Also cleans up some proofs that used `revert` instead of `induction`.

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 30, 2024

Merge branch 'master' into FR_induction

ded55f8

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 30, 2024

dagurtomas pushed a commit that referenced this pull request Jul 2, 2024

chore: register MulOpposite.rec with induction and cases (#14136)

1cdaa0a

Split from #12605. Co-authored-by: negiizhao [email protected]

dagurtomas pushed a commit that referenced this pull request Jul 2, 2024

chore: register TensorProduct with induction_eliminator (#14204)

fc2eed6

Split from #12605

dagurtomas pushed a commit that referenced this pull request Jul 2, 2024

chore: register Sym2 with induction (#14288)

daa4f13

Split from #12605 Also cleans up some proofs that used `revert` instead of `induction`.

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 7, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

chore: attribute [induction_eliminator] #12605

chore: attribute [induction_eliminator] #12605

FR-vdash-bot commented May 2, 2024 •

edited by eric-wieser

Loading

FR-vdash-bot May 2, 2024

urkud commented May 19, 2024

eric-wieser commented May 21, 2024

eric-wieser commented May 21, 2024

eric-wieser commented Jun 27, 2024

eric-wieser commented Jun 30, 2024

YaelDillies commented Jan 23, 2025

chore: attribute [induction_eliminator] #12605

Are you sure you want to change the base?

chore: attribute [induction_eliminator] #12605

Conversation

FR-vdash-bot commented May 2, 2024 • edited by eric-wieser Loading

FR-vdash-bot May 2, 2024

Choose a reason for hiding this comment

urkud commented May 19, 2024

eric-wieser commented May 21, 2024

eric-wieser commented May 21, 2024

eric-wieser commented Jun 27, 2024

eric-wieser commented Jun 30, 2024

YaelDillies commented Jan 23, 2025

FR-vdash-bot commented May 2, 2024 •

edited by eric-wieser

Loading