refactor: back rfl
tactic primarily via apply_rfl
#4891
copyright-header.yml
on: pull_request
check-lean-files
24s