feat: congr_simp as realizable constant
#13142
copyright-header.yml
on: pull_request
check-lean-files
29s
congr_simp as realizable constant
#13142