feat(/Fin/): add lemmas (#21175) #1356

	name: Zulip Emoji Merge Delegate

	on:
	push:
	branches:
	- master

	jobs:
	zulip-emoji-merged:
	runs-on: ubuntu-latest

	steps:
	- name: Checkout mathlib repository
	uses: actions/checkout@v4
	with:
	fetch-depth: 0 # donwload the full repository

	- name: Set up Python
	uses: actions/setup-python@v5
	with:
	python-version: '3.x'

	- name: Install dependencies
	run: \|
	python -m pip install --upgrade pip
	pip install zulip

	- name: Run Zulip Emoji Merge Delegate Script
	env:
	ZULIP_API_KEY: ${{ secrets.ZULIP_API_KEY }}
	ZULIP_EMAIL: [email protected]
	ZULIP_SITE: https://leanprover.zulipchat.com
	run: \|
	# scan the commits of the past 10 minutes, assuming that the timezone of the current machine
	# is the same that performed the commit
	git log --since="10 minutes ago" --pretty=oneline

	printf $'Scanning commits:\n%s\n\nContinuing\n' "$(git log --since="10 minutes ago" --pretty=oneline)"
	while read -r pr_number; do
	printf $'Running the python script with pr "%s"\n' "${pr_number}"
	python scripts/zulip_emoji_merge_delegate.py "$ZULIP_API_KEY" "$ZULIP_EMAIL" "$ZULIP_SITE" "[Merged by Bors]" "${pr_number}"
	done < <(git log --oneline -n 10 \| awk -F# '{ gsub(/)$/, ""); print $NF}')

Provide feedback