mathlib3port error

Stream: mathlib4

[Kevin Buzzard]

The autoporter seemed to spit out some nonsense in CategoryTheory.Sites.CoverLifting, which surprised me because in my experience it's super-accurate syntactically. This Lean 3 code here got translated into this which isn't syntactically valid. In short, Lean 3 X := X inside a structure whose field was renamed to pt in mathlib4, was translated into pt rather than pt := X. Not a big deal but I thought I'd mention it because I noticed it.

[Gabriel Ebner]

pt is short for pt := pt in Lean 4, so maybe mathport wants to tell us that we should rename X to pt?