Commit 2025-08-19 20:13 93f9c334

View on Github →

feat(Tactic/ToAdditive): make to_additive translate binder names (#28104) Currently, to_additive does not translate binder names like (one : motive 0 (zero_mem _)) in AddSubmonoid.closure_induction. This makes induction tactic create confusing case names. This PR makes to_additive also translate binder names in the declaration.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/Submodule/Lattice.lean

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

Modified Mathlib/Algebra/Ring/Submonoid/Basic.lean

Modified Mathlib/Algebra/Ring/Subring/Basic.lean

Modified Mathlib/Algebra/Ring/Subsemiring/Basic.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/StarOrder.lean

Modified Mathlib/Lean/Expr/Basic.lean

added def Lean.Expr.mapForallBinderNames

Modified Mathlib/LinearAlgebra/Span/Defs.lean

Modified Mathlib/RingTheory/NonUnitalSubring/Basic.lean

Modified Mathlib/RingTheory/TwoSidedIdeal/Operations.lean

Modified Mathlib/Tactic.lean

Modified Mathlib/Tactic/ToAdditive/Frontend.lean

deleted def ToAdditive.will.applyNameDict

deleted def ToAdditive.will.capitalizeFirstLike

deleted def ToAdditive.will.capitalizeLike

deleted def ToAdditive.will.endCapitalNames

deleted def ToAdditive.will.fixAbbreviation

deleted def ToAdditive.will.guessName

deleted def ToAdditive.will.nameDict

added def ToAdditive.will.renameBinderNames

Created Mathlib/Tactic/ToAdditive/GuessName.lean

added def ToAdditive.applyNameDict

added def ToAdditive.capitalizeFirstLike

added def ToAdditive.capitalizeLike

added def ToAdditive.endCapitalNames

added def ToAdditive.fixAbbreviation

added def ToAdditive.guessName

added def ToAdditive.nameDict

Modified Mathlib/Topology/ContinuousMap/StarOrdered.lean