prove some nonimplications for Equations 2712 and 3545 #1035

	name: Lint Style

	on:
	push:
	branches:
	- main
	paths:
	- '*/.lean'
	- 'lean-toolchain'
	- 'lakefile.toml'
	- 'lake-manifest.json'
	pull_request:
	branches:
	- main
	paths:
	- '*/.lean'
	- 'lean-toolchain'
	- 'lakefile.toml'
	- 'lake-manifest.json'
	workflow_dispatch: # Allow manual triggering of the workflow from the GitHub Actions interface

	# Set permissions for the workflow
	permissions:
	contents: read # Grant read access to repository contents
	pages: write # Grant write access to GitHub Pages
	id-token: write # Grant write access to ID tokens

	jobs:
	style_lint:
	runs-on: ubuntu-latest
	steps:
	- name: Check for long lines
	if: always() # Ensure the step runs regardless of the success or failure of previous steps
	run: \|
	# Find Lean files with lines longer than 100 characters, excluding URLs
	! (find equational_theories -name "*.lean" -type f -exec grep -E -H -n '^.{101,}$' {} \; \| grep -v -E 'https?://')

	- name: Don't 'import Mathlib', use precise imports
	if: always() # Ensure the step runs regardless of the success or failure of previous steps
	run: \|
	# Find and disallow any file that imports the entire Mathlib, encouraging precise imports instead
	! (find equational_theories -name "*.lean" -type f -print0 \| xargs -0 grep -E -n '^import Mathlib$')

Provide feedback