chore: use rfl in proofs where possible #1336

	name: build & test
	on:
	push:
	branches:
	- "main"
	pull_request:
	merge_group:

	permissions:
	contents: write

	jobs:
	build:
	name: build and test code
	runs-on: ubuntu-latest
	steps:
	- name: Checkout 🛎️
	uses: actions/checkout@v3

	- 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: Compile Library 🧐
	run: \|
	lake -R exe cache get # download cache of mathlib docs.
	lake -R build SSA

	- name: Compile Alive Examples
	run: \|
	lake -R exe cache get # download cache of mathlib docs.
	lake -R build AliveExamples

	- name: Compile Alive Scaling
	run: \|
	lake -R exe cache get # download cache of mathlib docs.
	lake -R build AliveScaling

	- name: Compile Executable 🧐
	run: \|
	lake -R exe cache get # download cache of mathlib docs.
	lake -R build mlirnatural
	- name: LLVM Exhaustive Enumeration
	run: \|
	sudo apt install llvm-15 # for opt-15, used to simplify LLVM for reference semantics.
	cd test/bruteforce-correctness && ./run.sh

	# - name: Run executable ⚙️
	# run: \|
	# ./build/bin/mlirnatural instcombine-test1 "32,2,3" \| grep "^some -2$"

Provide feedback