chore: remove unnecessary import in Batteries.Lean.LawfulMonad (#1042) #523

	# This job merges every commit to `main` into `nightly-testing`, resolving merge conflicts in favor of `nightly-testing`.

	name: Merge main to nightly

	on:
	push:
	branches:
	- main

	jobs:
	merge-to-nightly:
	if: github.repository_owner == 'leanprover-community'
	runs-on: ubuntu-latest
	steps:
	- name: Checkout repository
	uses: actions/checkout@v4
	with:
	fetch-depth: 0
	token: ${{ secrets.NIGHTLY_TESTING }}

	- name: Configure Git User
	run: \|
	git config user.name "leanprover-community-mathlib4-bot"
	git config user.email "[email protected]"

	- name: Merge main to nightly favoring nightly changes
	run: \|
	git checkout nightly-testing
	git merge main --strategy-option ours --no-commit --allow-unrelated-histories
	git commit -m "Merge main into nightly-testing"
	git push origin nightly-testing

Provide feedback