Commit 2025-03-21 16:27 5133cb04

View on Github →

chore: deprime induction' in root files (#22533) And remove direct imports of Mathlib.Tactic.Cases, in which induction' is defined. The files deprimed in this PR are

Files at the top of the output of this run, up to and including Data.Multiset.Basic
Files that directly import Mathlib.Tactic.Cases and a downstream file to build
Data.Nat.Bitwise, for using induction' in a local tactic
Data.Nat.PartENat, Data.Real.Basic and Data.Sym.Sym2 for their easy-to-replace induction' Note that there are a variety of indentation styles for induction'; I have tried to keep the count of changed lines small without sacrificing prettiness.

Estimated changes

Modified Mathlib/Algebra/Order/Floor.lean

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

Modified Mathlib/Algebra/Order/Interval/Set/Group.lean

Modified Mathlib/Algebra/Order/Ring/Abs.lean

Modified Mathlib/Algebra/Ring/Int/Defs.lean

Modified Mathlib/Algebra/Ring/Parity.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/List/Dedup.lean

Modified Mathlib/Data/List/Forall2.lean

Modified Mathlib/Data/List/InsertIdx.lean

Modified Mathlib/Data/List/Lookmap.lean

Modified Mathlib/Data/List/Nodup.lean

Modified Mathlib/Data/List/Perm/Basic.lean

Modified Mathlib/Data/List/Perm/Lattice.lean

Modified Mathlib/Data/List/Scan.lean

Modified Mathlib/Data/List/TakeWhile.lean

Modified Mathlib/Data/Multiset/Basic.lean

Modified Mathlib/Data/Multiset/Count.lean

Modified Mathlib/Data/Multiset/MapFold.lean

Modified Mathlib/Data/Multiset/UnionInter.lean

Modified Mathlib/Data/Multiset/ZeroCons.lean

Modified Mathlib/Data/Nat/Bitwise.lean

Modified Mathlib/Data/Nat/PartENat.lean

Modified Mathlib/Data/PNat/Basic.lean

Modified Mathlib/Data/Real/Basic.lean

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

Modified Mathlib/Data/Sym/Sym2.lean