Commit 2025-09-11 10:26 2cf10f2e

View on Github →

chore: deprime induction in all remaining places (#29542) The second commit removes the Mathlib.Tactic.Cases imports from all mathlib files (except Mathlib.Tactic) to prove that induction' has been completely removed from the main body of mathlib.

Estimated changes

Modified Mathlib/Algebra/Order/Group/Action.lean

Modified Mathlib/Combinatorics/Quiver/Path/Decomposition.lean

Modified Mathlib/Data/Countable/Basic.lean

Modified Mathlib/Data/Multiset/Antidiagonal.lean

Modified Mathlib/Data/Multiset/Bind.lean

Modified Mathlib/Data/Multiset/DershowitzManna.lean

Modified Mathlib/Data/Multiset/Pi.lean

modified theorem Multiset.mem_pi

Modified Mathlib/Data/Multiset/Powerset.lean

Modified Mathlib/Data/Num/Lemmas.lean

Modified Mathlib/Data/Num/Prime.lean

Modified Mathlib/Data/Num/ZNum.lean

Modified Mathlib/Data/PFunctor/Univariate/M.lean

Modified Mathlib/Data/QPF/Univariate/Basic.lean

Modified Mathlib/Data/Seq/Basic.lean

Modified Mathlib/Data/Seq/Computation.lean

Modified Mathlib/Data/Seq/Defs.lean

Modified Mathlib/Data/Seq/Parallel.lean

Modified Mathlib/Data/Set/Finite/Basic.lean

Modified Mathlib/Data/Setoid/Partition.lean

Modified Mathlib/Data/Stream/Init.lean

modified theorem Stream'.append_take_drop

modified theorem Stream'.cons_get_inits_core

modified theorem Stream'.get_inits

modified theorem Stream'.get_tails

modified theorem Stream'.get_unfolds_head_tail

modified theorem Stream'.take_theorem

Modified Mathlib/Data/Sym/Sym2/Order.lean

Modified Mathlib/Data/Vector/Basic.lean

Modified Mathlib/Data/W/Basic.lean

Modified Mathlib/Data/W/Cardinal.lean

Modified Mathlib/Data/WSeq/Basic.lean

Modified Mathlib/Data/WSeq/Defs.lean

Modified Mathlib/Data/WSeq/Relation.lean

Modified Mathlib/Tactic/Common.lean

Modified scripts/noshake.json