Commit 2026-05-17 17:16 954b00a4

View on Github →

feat(Tactic/ToFun): allow configuring the name of the generated declaration (#34257) This allows removing a few more duplicate lemmas. A few of these lemmas were misnamed (i.e., not using the fun_ naming convention): we correct this.

Estimated changes

deleted theorem contDiffAt_fun_id
deleted theorem contDiffOn_fun_id
deleted theorem contDiffWithinAt_fun_id
deleted theorem contDiff_fun_id
deleted theorem differentiableAt_fun_id
deleted theorem differentiable_fun_id
deleted theorem fderivWithin_id'
deleted theorem fderiv_id'
added theorem Foo.Bar.baz''
added theorem Foo.Bar.baz'
added theorem Foo.Bar.baz
added theorem Foo.bar''
added theorem Foo.bar'
added theorem Foo.bar
added theorem Test.Foo.bar
added theorem Test.Foo.Bar.baz''
added theorem Test.Foo.Bar.baz'
added theorem Test.Foo.Bar.baz