docs: Adding some documentation for lemmas #1499


	on:
	push:
	branches:
	- master
	pull_request:

	name: continuous integration

	jobs:
	doc_lint:
	name: doc lint
	runs-on: ubuntu-latest
	steps:

	- uses: actions/checkout@v4

	- name: Install elan
	run: \|
	set -o pipefail
	curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf \| sh -s -- --default-toolchain none -y
	~/.elan/bin/lean --version
	echo "$HOME/.elan/bin" >> $GITHUB_PATH

	- name: check versions
	run: \|
	lean --version
	lake --version

	- name: build cache
	run: \|
	lake exe cache get

	- name: build HepLean
	id: build
	uses: liskin/gh-problem-matcher-wrap@v3
	with:
	linters: gcc
	run: \|
	bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake build -KCI \| tee stdout.log"

	- name: check file imports
	run: \|
	bash -o pipefail -c "env LEAN_ABORT_ON_PANIC=1 lake exe check_file_imports"

	- name: runLinter on HepLean
	if: ${{ always() && steps.build.outcome == 'success' \|\| steps.build.outcome == 'failure' }}
	id: lint
	uses: liskin/gh-problem-matcher-wrap@v3
	with:
	linters: gcc
	run: env LEAN_ABORT_ON_PANIC=1 lake exe runLinter HepLean

	style_lint:
	name: Python based style linter
	runs-on: ubuntu-latest
	steps:
	- name: cleanup
	run: \|
	find . -name . -o -prune -exec rm -rf -- {} +

	- uses: actions/checkout@v4

	# Run the case checker action
	- name: Check Case Sensitivity
	uses: credfeto/[email protected]

	- name: Look for ignored files
	uses: credfeto/[email protected]

	- name: install Python
	if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }}
	uses: actions/setup-python@v5
	with:
	python-version: 3.8

	- name: lint
	run: \|
	chmod u+x scripts/lint-style.sh
	./scripts/lint-style.sh

Provide feedback