Remark: Lean 3 apply ih sometimes didn't work here, I had to give the motive explicitly. See lines 268 and 358 (or search for refine @)

It looks like you did many of the renames without simultaneously writing the #aligns? You do you, but I'm confused how you're going to write the #align's later. It seems prone to error!

Yeah, I think Yakov was also talking about this at the porting meeting. What I did with the bool files was just got everything working and then diffed the file with the mathbin port and did the aligns after :-)

This is now compiling and ready for review (thanks for the comments even when the PR wasn't ready!) I don't know what the tag needs-mathlib-SHA means. The last mathlib3 commit which changed logic.relation is 5ca6e9d2bb25feeebdefe9bd9de163897bdecd05 and the changes made in that commit have been ported here. I took this file from a version of mathlib3port from about two weeks ago and have updated mathlib3port since.

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

This is now compiling and ready for review (thanks for the comments even when the PR wasn't ready!) I don't know what the tag needs-mathlib-SHA means. The last mathlib3 commit which changed logic.relation is 5ca6e9d2bb25feeebdefe9bd9de163897bdecd05 and the changes made in that commit have been ported here. I took this file from a version of mathlib3port from about two weeks ago and have updated mathlib3port since.

@kbuzzard Just to directly answer this question: the mathport SHA you should provide is the latest version of mathlib for which you have incorporated changes from the file that is considered to be ported by this PR (namely logic.relation in this case). So if you started with the version from two weeks ago, then during the PR you incorporated changes to the mathlib3 file and consider it up to date with today's logic.relation, then you would use today's mathlib SHA in the PR comment. It's also okay to not update your PR with changes in the meantime and just report a SHA from two weeks ago.

The important part is that you shouldn't use mathlib from two weeks ago and report today's mathlib SHA if there were important changes in those two weeks, since then those changes will fall through the cracks when we go to do upgrades later.