!4#3130

Stream: PR reviews

[Scott Morrison]

Ah, I was still fixing the regression in nontriviality in !4#3130, and succeeded, but the PR has been merged underneath me!

I think it would be good for every tactic regression, to make sure there is an open issue for it, and the porting note should link to the issue. Getting these things fixed is as important as moving theory files along (but doesn't need to hold them up).

[Scott Morrison]

Pinging @Johan Commelin, @Jeremy Tan, and @Chris Hughes as they were the ones involved on this PR, but I think this request holds quite generally.

[Scott Morrison]

Similarly, for people porting files that use obviously, I would like there to be a clear record if aesop / aesop_cat can't fill in the proof, and you write one by hand. There must be a porting note saying "obviously used to do this" at each new proof, so we can rip them back out when automation catches up.

[Scott Morrison]

The fix is in at https://github.com/leanprover-community/mathlib4/pull/3175/files