!4#5294 help wanted

Stream: mathlib4

[David Ang]

This is my first time porting an entire file and I'm trying to port AlgebraicGeometry.EllipticCurve.Weierstrass in !4#5294. I encountered multiple issues and solved most of them but still need some help. I added a few porting notes but here are the main ones:

• CoordinateRing used to be a def with derive [inhabited, comm_ring], but the corresponding deriving Inhabited, CommRing doesn't work, and I had to replace it with an abbrev. This might cause the same slowness problem mentioned in the class_group.mk topic in #maths, which is not present in this file but will show up in the future AlgebraicGeometry.EllipticCurve.Point file. I'm not sure how to add the local attribute as mentioned in the comments so I can't say if this is fine.
• quotientXYIdealEquiv is a series of three algebra equivalences linked by trans that gives a deterministic timeout. I tried separating it into three defs but the first one required ~800k heartbeats to compile, and I can't get the second one to compile at all.
• ./scripts/fix-lints.py seems to be broken for me locally, and upon inspecting manually I don't know how to fix many of the linter problems. For instance, the linter tells me that the simps tag in variableChange and baseChange should be simps!, but simps! doesn't generate lemmas like variableChange_Δ', which I needed to prove variableChange_j.

[Eric Wieser]

fix-lints only fixes a very small set of linter issues