feat: HasFPowerSeriesAt.eventually_differentiableAt #2

	name: Autolabel PRs

	on:
	pull_request:
	types: [opened]
	push:
	paths:
	- scripts/autolabel.lean
	- .github/workflows/add_label_from_diff.yaml

	jobs:
	add_topic_label:
	name: Add topic label
	runs-on: ubuntu-latest
	# Don't run on forks, where we wouldn't have permissions to add the label anyway.
	if: github.repository == 'leanprover-community/mathlib4'
	permissions:
	issues: write
	checks: write
	pull-requests: write
	contents: read
	steps:
	- name: Checkout code
	uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
	with:
	fetch-depth: 0
	- name: Configure Lean
	uses: leanprover/lean-action@f807b338d95de7813c5c50d018f1c23c9b93b4ec # 2025-04-24
	with:
	auto-config: false
	use-github-cache: false
	use-mathlib-cache: false
	- name: lake exe autolabel
	run: \|
	# the checkout dance, to avoid a detached head
	git checkout master
	git checkout -
	lake exe autolabel "$NUMBER"
	env:
	GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
	GH_REPO: ${{ github.repository }}
	NUMBER: ${{ github.event.number }}

Provide feedback