Skip to content

[Merged by Bors] - chore: use to_fun to auto-generate more duplicate lemmas#34279

Closed
grunweg wants to merge 4 commits into
leanprover-community:masterfrom
grunweg:tofun-golf
Closed

[Merged by Bors] - chore: use to_fun to auto-generate more duplicate lemmas#34279
grunweg wants to merge 4 commits into
leanprover-community:masterfrom
grunweg:tofun-golf

Conversation

@grunweg

@grunweg grunweg commented Jan 22, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

We use the new functionality of to_fun from #34257 to remove a few more duplicate lemmas.

Open in Gitpod

@github-actions

github-actions Bot commented Jan 22, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary ac4a84c72d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

- Differentiable.fun_pow
- DifferentiableAt.fun_pow
- DifferentiableOn.fun_pow
- Finset.analyticAt_fun_sum
- Finset.analyticOnNhd_fun_sum
- Finset.analyticOn_fun_sum
- Finset.analyticWithinAt_fun_sum
- HasDerivAt.fun_pow
- HasFDerivAt.fun_pow'
- HasFDerivWithinAt.fun_pow'
- HasStrictFDerivAt.fun_pow'
- analyticAt_iff_analytic_fun_mul
- derivWithin_fun_pow
- deriv_fun_pow
- fderivWithin_fun_pow
- fderivWithin_fun_pow'
- fderiv_fun_pow
- fderiv_fun_pow'
- iteratedDerivWithin_fun_id
- iteratedDeriv_fun_add
- iteratedDeriv_fun_const_smul
- iteratedDeriv_fun_id
- iteratedDeriv_fun_mul
- iteratedDeriv_fun_neg
- iteratedDeriv_fun_sub

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.
No changes to weak technical debt.

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 22, 2026
@mathlib4-merge-conflict-bot mathlib4-merge-conflict-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 Jan 29, 2026
@mathlib4-merge-conflict-bot

mathlib4-merge-conflict-bot commented Jan 29, 2026

Copy link
Copy Markdown
Collaborator

This pull request has conflicts, please merge master and resolve them.

@mathlib-dependent-issues mathlib-dependent-issues Bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 17, 2026
@mathlib-dependent-issues

mathlib-dependent-issues Bot commented May 17, 2026

Copy link
Copy Markdown

This PR/issue depends on:

grunweg added 3 commits May 18, 2026 00:27
@grunweg
chore: a few more lemmas
64f2ba0
@grunweg
fix: statement of fderiv_pow
e1a41a6 
The current version is an exact duplicate of fderiv_fun_pow, likely a copy-paste
error. Fix it to match what it says.
@grunweg
Five more
66ae3c6
@github-actions github-actions 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 17, 2026
@grunweg grunweg added the t-analysis Analysis (normed *, calculus) label May 18, 2026
@grunweg grunweg changed the title chore: use to_fun more chore: use to_fun to auto-generate more duplicate lemmas May 18, 2026
j-loreaux
j-loreaux reviewed May 19, 2026
View reviewed changes

@j-loreaux j-loreaux left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+

Comment thread Mathlib/Analysis/Calculus/Deriv/Pow.lean Outdated
Comment on lines 108 to 109
@[to_fun HasDerivAt.fun_pow]
theorem HasDerivAt.pow (h : HasDerivAt f f' x) (n : ℕ) :

@j-loreaux j-loreaux May 19, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Isn't this the name to_fun generates anyway? Is there no feature like with to_additive where it tells you the autogenerated name matches the one you provided?

@grunweg grunweg May 19, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Indeed, that's the auto-generated name. (Perhaps it wasn't until recently?) Removed.

@mathlib-bors

mathlib-bors Bot commented May 19, 2026

Copy link
Copy Markdown
Contributor

✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@mathlib-triage mathlib-triage Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label May 19, 2026
@grunweg

grunweg commented May 19, 2026

Copy link
Copy Markdown
Contributor Author

Thanks for the review!
bors merge

mathlib-bors Bot pushed a commit that referenced this pull request May 19, 2026
@grunweg
chore: use to_fun to auto-generate more duplicate lemmas (#34279)
1fb6b28 
We use the new functionality of `to_fun` from #34257 to remove a few more duplicate lemmas.
@mathlib-triage mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 19, 2026
@grunweg

grunweg commented May 19, 2026

Copy link
Copy Markdown
Contributor Author

#39598 makes to_fun warn if the auto-generated name matches the provided one. Good idea!

@mathlib-bors

mathlib-bors Bot commented May 19, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title chore: use to_fun to auto-generate more duplicate lemmas [Merged by Bors] - chore: use to_fun to auto-generate more duplicate lemmas May 19, 2026
@mathlib-bors mathlib-bors Bot closed this May 19, 2026
RaggedR pushed a commit to RaggedR/mathlib4 that referenced this pull request May 22, 2026
@grunweg
chore: use to_fun to auto-generate more duplicate lemmas (leanprove…
68b1d55 
…r-community#34279)

We use the new functionality of `to_fun` from leanprover-community#34257 to remove a few more duplicate lemmas.
b-mehta pushed a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026
@grunweg @b-mehta
chore: use to_fun to auto-generate more duplicate lemmas (leanprove…
d2e8329 
…r-community#34279)

We use the new functionality of `to_fun` from leanprover-community#34257 to remove a few more duplicate lemmas.
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
@grunweg @Bergschaf
chore: use to_fun to auto-generate more duplicate lemmas (leanprove…
a9cf6a0 
…r-community#34279)

We use the new functionality of `to_fun` from leanprover-community#34257 to remove a few more duplicate lemmas.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@j-loreaux j-loreaux j-loreaux left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@grunweg @mathlib4-merge-conflict-bot @j-loreaux @mathlib4-dependent-issues-bot