openpr_Q_v2_sweep2.txt

====================================================================================================
CASE Q  PR #25218  (open-pr, v2 prompt, sweep2)
file: Mathlib/AlgebraicGeometry/EllipticCurve/Modular/TateNormalForm.lean  line: 70.0
reviewer: @MichaelStollBayreuth  on 2025-06-01T20:07:09Z
advice_kind: docstring rewording
prompt_tokens: 8873  completion_tokens: 3548
HUMAN reviewer (ground truth):
  > ```suggestion
  > /-- The `Y` coordinate of a given point. For the point at infinity, this returns `0`
  > ```
====================================================================================================

[SYSTEM]
----------------------------------------------------------------------------------------------------
You are an expert reviewer for the Lean 4 / mathlib4 mathematical library. Given a NEW code hunk from an open pull request and a set of historically retrieved (past_hunk, past_comment) pairs, your job is to identify which past reviewer feedback would also apply to the new hunk.

Compared to a naive matcher you must do TWO extra things, because the answer is often only derivable by combining evidence:

A. STRUCTURAL PATTERN EXTRACTION. Past comments often contain `suggestion` code blocks (```suggestion ... ```) or inline code-shape rewrites. These suggested code snippets ARE concrete advice, not just commentary. Treat them as first-class evidence about preferred Lean/mathlib idioms (e.g.: term-mode constructor `:= ⟨_, _, _⟩` vs `by use _; exact _`, `instance` vs `theorem` for class-membership statements, `refine ⟨..., ?_⟩` vs `use ...; constructor`, `@[simp]` / `@[to_additive]` attributes, naming conventions, docstring phrasing, etc.).

B. CROSS-CANDIDATE SYNTHESIS. The applicable advice for the new hunk may require combining evidence from multiple candidates. Example: candidate X's context tells you that an identifier in the new hunk is a `class`; candidate Y shows the term-mode `instance ... := ⟨...⟩` template for proving class membership. Together they support the conclusion: "the new theorem proving class membership should be rewritten as an `instance` with a term-mode constructor". List supporting PRs for any synthesised finding.

Reasoning protocol (do this internally before producing JSON):

  1. STRUCTURAL FEATURES OF THE NEW HUNK. Identify each: tactic-mode vs term-mode? Uses `by use ...; exact ...`? Uses `use ...; constructor`? Declares an `instance` / a `theorem` / a `lemma` / a `def` / a `class`? Has `@[simp]`, `@[to_additive]`, `@[deprecated]`? Uses anonymous functions `fun x =>` vs `↦`? Has a docstring `/-- ... -/` of any specific shape?

  2. PATTERN INVENTORY FROM CANDIDATES. For each candidate, note any concrete pattern shown in its suggested-code or comment (term-mode template, attribute recommendation, naming convention, idiomatic rewrite, terminology preference, etc.). Also note which candidates' past hunks define or use identifiers that appear in the new hunk (these are clues about whether something is a class, an instance, an alias, etc.).

  3. APPLICABILITY CHECK. For each pattern from step 2, ask: does the new hunk's structure (step 1) instantiate the same shape that this pattern was applied to? If yes, that's a STRONG match. If two patterns combine to support a finding, list both supporting PRs.

  4. STRICT REFUSAL. If after this analysis no candidate (alone or in combination) gives concrete, well-grounded advice for the specific code in the new hunk, output an empty `strong_matches` list. Do not paper over with generic advice. Generic style observations belong in `weak_observations`, clearly marked. Do not invent advice that isn't traceable to specific past PRs in the retrieval pool.

Confidence:
  - "high"  — at least one strong match is grounded in concrete suggested-code or explicit prose from a candidate, and the new hunk clearly fits the same shape
  - "medium" — at least one strong match exists but requires synthesis or adaptation; OR a single candidate gives related but not identical advice
  - "low"   — only loose stylistic patterns; nothing actionable
  - "none"  — retrieved pool is unrelated; do not press an answer

Output JSON ONLY, matching this exact schema:

{
  "summary": "<one sentence describing what we found>",
  "confidence": "high"|"medium"|"low"|"none",
  "strong_matches": [
    {
      "past_pr": <int>,
      "past_file": "<string>",
      "past_comment_excerpt": "<verbatim short quote from the past comment OR the relevant snippet from its suggestion block>",
      "applies_because": "<one or two sentences linking past code/comment to the new hunk's structure>",
      "suggested_adaptation": "<one sentence on what the reviewer might say on the new hunk>",
      "supporting_past_prs": [<int>, ...]
    }
  ],
  "weak_observations": [
    {
      "observation": "<short string>",
      "supporting_past_prs": [<int>, ...]
    }
  ]
}

Quote short — under 40 words per excerpt. Be precise about which PR(s) support each finding via supporting_past_prs.

[USER]
----------------------------------------------------------------------------------------------------
NEW HUNK from open PR #25218 (file: Mathlib/AlgebraicGeometry/EllipticCurve/Modular/TateNormalForm.lean):
```
@@ -0,0 +1,267 @@
... [30 lines above hidden]
+
+* `IsTateNF W`: A typeclass saying that the Weierstrass curve `W` is in Tate normal form.
+* `toTateNF W`: Given a point `P` satisfying the condition `P, 2P, 3P ≠ 0`, this is a variable
+  change that brings the Weierstrass curve `W` to Tate normal form.
+
+## References
+
+* [James Parson, Moduli of Elliptic Curves](https://math.stanford.edu/~conrad/vigregroup/vigre03/moduli.pdf)
+-/
+
+noncomputable section
+
+namespace WeierstrassCurve
+
+/-- The Tate normal form is $$y^2 + (1-c)xy - by = x^3 - bx^2$$. -/
+@[mk_iff]
+class IsTateNF {R : Type*} [Zero R] (W : WeierstrassCurve R) : Prop where
+  a₂₃ : W.a₂ = W.a₃
+  a₄  : W.a₄ = 0
+  a₆  : W.a₆ = 0
+
+namespace Affine.Point
+
+variable {R : Type*} [CommRing R] {W : WeierstrassCurve R} (P : W.toAffine.Point)
+
+/-- Typeclass for a given point not being zero (the point at infinity). -/
+@[mk_iff]
+class NeZero : Prop where
+  neZero : P ≠ 0
+
+instance : DecidablePred (Affine.Point.NeZero (W:=W))
+| zero   => isFalse (fun ⟨h⟩ ↦ h rfl)
+| some _ => isTrue ⟨Point.noConfusion⟩
+
+/-- The `X` coordinate of a given point. For the point of infinity, this returns `0`
+(junk value). -/
+def X : W.toAffine.Point → R
+  | 0 => 0
+  | @some _ _ _ x _ _ => x
+
+/-- The `Y` coordinate of a given point. For the point of infinity, this returns `0`
```

RETRIEVED CANDIDATES (top-20 by hunk-embedding similarity, sorted by sim desc):

--- candidate 1 (sim=0.793, past_pr=#16864, file=Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean) ---
PAST HUNK:
```
@@ -0,0 +1,662 @@
... [7 lines above hidden]
+import Mathlib.Algebra.CharP.Defs
+
+/-!
+
+# Some normal forms of elliptic curves
+
+This file defines some normal forms of Weierstrass equations of elliptic curves.
+
+## Main definitions and results
+
+The following normal form is in [silverman2009], section III.1, page 42.
+
+- `WeierstrassCurve.IsCharNeTwoNF` is a predicate asserts that a `WeierstrassCurve` is of form
```
PAST COMMENT (from reviewer):
```suggestion
- `WeierstrassCurve.IsCharNeTwoNF` is a predicate that asserts that a `WeierstrassCurve` is of form
```
also elsewhere

--- candidate 2 (sim=0.792, past_pr=#16864, file=Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean) ---
PAST HUNK:
```
@@ -0,0 +1,662 @@
... [5 lines above hidden]
+-/
+import Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
+import Mathlib.Algebra.CharP.Defs
+
+/-!
+
+# Some normal forms of elliptic curves
+
+This file defines some normal forms of Weierstrass equations of elliptic curves.
+
+## Main definitions and results
+
+The following normal form is in [silverman2009], section III.1, page 42.
```
PAST COMMENT (from reviewer):
```suggestion
The following normal forms are in [silverman2009], section III.1, page 42.
```

--- candidate 3 (sim=0.782, past_pr=#9433, file=Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean) ---
PAST HUNK:
```
@@ -86,240 +90,769 @@ local macro "pderiv_simp" : tactic =>
... [609 lines above hidden]
+
+lemma dblX_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
+    (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 ≠ W.negY Q * P z ^ 3) :
+    W.dblX P / W.dblZ P ^ 2 = W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
+      (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)) := by
+  rw [dblX, toAffine_slope_of_eq hP hQ hPz hQz hx hy, dblZ,
+    ← (div_eq_div_iff (pow_ne_zero 2 hPz) (pow_ne_zero 2 hQz)).mpr hx,
+    toAffine_addX_of_eq hPz <| sub_ne_zero_of_ne <| Y_ne_negY_of_Y_ne' hP hQ hx hy]
+
+variable (V) in
+/-- The $Y$-coordinate of the doubling of a point representative, before applying the final negation
+that maps $Y$ to $-Y - a_1XZ - a_3Z^3$. -/
+def dblY' (P : Fin 3 → R) : R :=
```
PAST COMMENT (from reviewer):
What about `negDblY`?

--- candidate 4 (sim=0.782, past_pr=#9433, file=Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean) ---
PAST HUNK:
```
@@ -86,240 +90,769 @@ local macro "pderiv_simp" : tactic =>
... [740 lines above hidden]
+
+lemma addX_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
+    (hQz : Q z ≠ 0) : W.addX P Q =
+      ((P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2
+        + W.a₁ * (P y * Q z ^ 3 - Q y * P z ^ 3) * P z * Q z * addZ P Q
+        - W.a₂ * P z ^ 2 * Q z ^ 2 * addZ P Q ^ 2 - P x * Q z ^ 2 * addZ P Q ^ 2
+        - Q x * P z ^ 2 * addZ P Q ^ 2) / (P z * Q z) ^ 2 := by
+  rw [← addX_eq' hP hQ, mul_div_cancel_right₀ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz]
+
+lemma addX_smul (P Q : Fin 3 → R) (u v : Rˣ) :
+    V.addX (u • P) (v • Q) = ((u * v) ^ 2) ^ 2 * V.addX P Q := by
+  simp only [addX, smul_fin3_ext]
+  ring1
```
PAST COMMENT (from reviewer):
Is there a reason you're avoiding `ring`? Is `ring1` faster or better in some way?

--- candidate 5 (sim=0.780, past_pr=#9744, file=Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean) ---
PAST HUNK:
```
@@ -17,8 +17,8 @@ under the geometric group law defined in `Mathlib.AlgebraicGeometry.EllipticCurv
 
 Let `W` be a Weierstrass curve over a field `F` given by a Weierstrass equation $W(X, Y) = 0$ in
 affine coordinates. As in `Mathlib.AlgebraicGeometry.EllipticCurve.Affine`, the set of nonsingular
-rational points $W(F)$ of `W` consist of the unique point at infinity $0$ and nonsingular affine
-points $(x, y)$. With this description, there is an addition-preserving injection between $W(F)$
+rational points $W⟮F⟯$ of `W` consist of the unique point at infinity $0$ and nonsingular affine
```
PAST COMMENT (from reviewer):
Those are the weird parenthesis used for for `IntermediateField` (or something similar), right? I guess LaTeX will not love them

--- candidate 6 (sim=0.774, past_pr=#8485, file=Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean) ---
PAST HUNK:
```
@@ -0,0 +1,967 @@
... [575 lines above hidden]
+@[simp]
+lemma neg_map_some (X Y : R) : W.neg_map ⟦![X, Y, 1]⟧ = ⟦![X, -Y - W.a₁ * X - W.a₃, 1]⟧ := by
+  rw [neg_map_eq, neg_some]
+
+open scoped Classical
+
+/-- The addition of two point representatives. -/
+@[pp_dot]
+noncomputable def add (P Q : Fin 3 → R) : Fin 3 → R :=
+  if P z = 0 then Q else if Q z = 0 then P else if P x * Q z = P z * Q x then
+    if P y * Q z = P z * W.negY Q then ![0, 1, 0] else
+      ![W.addX_of_Yne P, W.addY_of_Yne P, W.addZ_of_Yne P]
+  else ![W.addX_of_Xne P Q, W.addY_of_Xne P Q, addZ_of_Xne P Q]
```
PAST COMMENT (from reviewer):
Hmm thanks! I can reproduce ... so this should give rise to multiplication-by-n formula in projective coordinates, and I wonder how it compares with $(\phi\psi:\omega:\psi^3)$ ...

--- candidate 7 (sim=0.774, past_pr=#8485, file=Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean) ---
PAST HUNK:
```
@@ -0,0 +1,967 @@
... [575 lines above hidden]
+@[simp]
+lemma neg_map_some (X Y : R) : W.neg_map ⟦![X, Y, 1]⟧ = ⟦![X, -Y - W.a₁ * X - W.a₃, 1]⟧ := by
+  rw [neg_map_eq, neg_some]
+
+open scoped Classical
+
+/-- The addition of two point representatives. -/
+@[pp_dot]
+noncomputable def add (P Q : Fin 3 → R) : Fin 3 → R :=
+  if P z = 0 then Q else if Q z = 0 then P else if P x * Q z = P z * Q x then
+    if P y * Q z = P z * W.negY Q then ![0, 1, 0] else
+      ![W.addX_of_Yne P, W.addY_of_Yne P, W.addZ_of_Yne P]
+  else ![W.addX_of_Xne P Q, W.addY_of_Xne P Q, addZ_of_Xne P Q]
```
PAST COMMENT (from reviewer):
I think these could be called `![W.dblX P, W.dblY P, W.dblZ P]` and `![W.addX P, W.addY P, addZ P]` just like the Jacobian case. In fact, I've found that you can remove a `P z ^ 2` factor from the projective doubling formula to make it valid in all cases (O+O or P+P for P 2-torsion); the resulting formula is homogeneous of degree 4 rather than 6. From the projective addition formula, you can also remove a factor of `P z * Q z`, and the resulting formula is homogeneous of degree 6 rather than 8, and applies in the case P=-Q≠Q, but not in the cases P=O or Q=O (gives (0,0,0)). I don't think this simplifies the proof that the reduction map is a homomorphism though.

I think this is the best you can do in projective coordinates, which is not as nice as the Jacobian formulas, wh
... [truncated]

--- candidate 8 (sim=0.773, past_pr=#9405, file=Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean) ---
PAST HUNK:
```
@@ -86,240 +107,1237 @@ local macro "pderiv_simp" : tactic =>
... [575 lines above hidden]
+  have hPy : P y - W.negY P ≠ 0 := sub_ne_zero_of_ne <| Y_ne_negY_of_Y_ne' hP hQ hx hy
+  simp only [mul_comm <| P z ^ _, ne_eq, ← div_eq_div_iff (pow_ne_zero _ hPz) (pow_ne_zero _ hQz)]
+    at hx hy
+  rw [Affine.slope_of_Yne hx <| negY_of_Z_ne_zero hQz ▸ hy, ← negY_of_Z_ne_zero hPz, dblZ]
+  field_simp [pow_ne_zero 2 hPz]
+  ring1
+
+variable (V) in
+/-- The $X$-coordinate of the doubling of a point representative. -/
+def dblX (P : Fin 3 → R) : R :=
+  (3 * P x ^ 2 + 2 * V.a₂ * P x * P z ^ 2 + V.a₄ * P z ^ 4 - V.a₁ * P y * P z) ^ 2
+    + V.a₁ * (3 * P x ^ 2 + 2 * V.a₂ * P x * P z ^ 2 + V.a₄ * P z ^ 4 - V.a₁ * P y * P z) * P z
+      * (P y - V.negY P) - V.a₂ * P z ^ 2 * (P y - V.negY P) ^ 2 - 2 * P x * (P y - V.negY P) ^ 2
```
PAST COMMENT (from reviewer):
What do you think about replacing the appearances of the RHS of [WeierstrassCurve.Jacobian.eval_polynomialX](https://leanprover-community.github.io/mathlib4_docs/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.html#WeierstrassCurve.Jacobian.eval_polynomialX) by the LHS in this definition and in `dblY` below? We could replace `P y - V.negY P` with the evaluation of `polynomialY` too, but that wouldn't be shorter.

--- candidate 9 (sim=0.773, past_pr=#9436, file=Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean) ---
PAST HUNK:
```
@@ -86,240 +106,1237 @@ local macro "pderiv_simp" : tactic =>
... [1155 lines above hidden]
+lemma nonsingularLift_addMap {P Q : PointClass F} (hP : W.NonsingularLift P)
+    (hQ : W.NonsingularLift Q) : W.NonsingularLift <| W.addMap P Q := by
+  rcases P, Q with ⟨⟨_⟩, ⟨_⟩⟩
+  exact nonsingular_add hP hQ
+
+end Addition
+
+section Point
+
+/-! ### Nonsingular rational points -/
+
+/-- A nonsingular rational point on `W`. -/
+structure Point where
```
PAST COMMENT (from reviewer):
`W'` would be fine, ~~or you could introduce `(W : Jacobian R)` globally and `(W : Jacobian F)` only in sections that deal with fields, and it will shadow the global W within the section. However, beware that you might be unable to change explicitness of W within the sections, see [lean4#3227](https://github.com/leanprover/lean4/issues/3227).~~ (given that the lemmas for the ring case and for the field case are interspersed, this probably isn't an option)

--- candidate 10 (sim=0.773, past_pr=#9436, file=Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean) ---
PAST HUNK:
```
@@ -86,240 +106,1237 @@ local macro "pderiv_simp" : tactic =>
... [1155 lines above hidden]
+lemma nonsingularLift_addMap {P Q : PointClass F} (hP : W.NonsingularLift P)
+    (hQ : W.NonsingularLift Q) : W.NonsingularLift <| W.addMap P Q := by
+  rcases P, Q with ⟨⟨_⟩, ⟨_⟩⟩
+  exact nonsingular_add hP hQ
+
+end Addition
+
+section Point
+
+/-! ### Nonsingular rational points -/
+
+/-- A nonsingular rational point on `W`. -/
+structure Point where
```
PAST COMMENT (from reviewer):
```suggestion
variable (V) in
/-- A nonsingular rational point on `V`. -/
@[ext] structure Point where
```
Please correct references to `W` in the docstrings that should actually be `V`.

--- candidate 11 (sim=0.772, past_pr=#18531, file=Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean) ---
PAST HUNK:
```
@@ -32,23 +32,20 @@ splitting field of `R` are precisely the $X$-coordinates of the non-zero 2-torsi
... [3 lines above hidden]
  * `WeierstrassCurve.Δ`: the discriminant of a Weierstrass curve.
- * `WeierstrassCurve.ofJ0`: a Weierstrass curve whose j-invariant is 0.
- * `WeierstrassCurve.ofJ1728`: a Weierstrass curve whose j-invariant is 1728.
- * `WeierstrassCurve.ofJ`: a Weierstrass curve whose j-invariant is neither 0 nor 1728.
  * `WeierstrassCurve.map`: the Weierstrass curve mapped over a ring homomorphism.
  * `WeierstrassCurve.twoTorsionPolynomial`: the 2-torsion polynomial of a Weierstrass curve.
- * `EllipticCurve`: an elliptic curve over a commutative ring.
- * `EllipticCurve.j`: the j-invariant of an elliptic curve.
- * `EllipticCurve.ofJ0`: an elliptic curve whose j-invariant is 0.
- * `EllipticCurve.ofJ1728`: an elliptic curve whose j-invariant is 1728.
- * `EllipticCurve.ofJ'`: an elliptic curve whose j-invariant is neither 0 nor 1728.
- * `EllipticCurve.ofJ`: an elliptic curve whose j-invariant equal to j.
+ * `WeierstrassCurve.IsElliptic`: typeclass asserts that a Weierstrass curve is an elliptic curve.
```
PAST COMMENT (from reviewer):
```suggestion
 * `WeierstrassCurve.IsElliptic`: typeclass asserting that a Weierstrass curve is an elliptic curve.
```

--- candidate 12 (sim=0.771, past_pr=#9417, file=Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean) ---
PAST HUNK:
```
@@ -446,4 +450,711 @@ alias nonsingular_of_affine_of_Z_ne_zero := nonsingular_of_Z_ne_zero
... [648 lines above hidden]
+    addZ_of_X_eq hP hQ hPz hQz hx]; ring1)) -(P z * Q z) * negAddY_of_X_eq' hP hQ hx
+
+lemma addY_of_X_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
+    (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z) : W.addY P Q = addU P Q := by
+  rw [addU, ← mul_div_mul_right _ _ <| pow_ne_zero 2 <| mul_ne_zero hPz hQz,
+    ← addY_of_X_eq' hP hQ hPz hQz hx, ← pow_succ',
+    mul_div_cancel_right₀ _ <| pow_ne_zero 3 <| mul_ne_zero hPz hQz]
+
+lemma addY_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
+    (hQz : Q z ≠ 0) (hx : P x * Q z ≠ Q x * P z) :
+    W.addY P Q / W.addZ P Q = W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
+      (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)) := by
+  erw [addY, negY_of_Z_ne_zero <| addZ_ne_zero_of_X_ne hP hQ hx, addX_of_Z_ne_zero hP hQ hPz hQz hx,
```
PAST COMMENT (from reviewer):
Do you understand why you need `erw` here whereas for most of the PR `rw` has been fine?

--- candidate 13 (sim=0.771, past_pr=#9417, file=Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean) ---
PAST HUNK:
```
@@ -446,4 +450,711 @@ alias nonsingular_of_affine_of_Z_ne_zero := nonsingular_of_Z_ne_zero
... [609 lines above hidden]
+  field_simp [mul_ne_zero (pow_ne_zero 2 <| mul_ne_zero hPz hQz) <| pow_ne_zero 3 hd]
+  ring1
+
+lemma negAddY_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
+    (hQz : Q z ≠ 0) (hx : P x * Q z ≠ Q x * P z) : W.negAddY P Q / W.addZ P Q =
+      W.toAffine.negAddY (P x / P z) (Q x / Q z) (P y / P z)
+        (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)) := by
+  rw [negAddY_eq hP hQ hPz hQz, addZ_eq hP hQ hPz hQz, toAffine_slope_of_ne hPz hQz hx,
+    toAffine_negAddY_of_ne hPz hQz <| sub_ne_zero.mpr hx]
+
+variable (W') in
+/-- The $Y$-coordinate of the addition of two distinct point representatives. -/
+def addY (P Q : Fin 3 → R) : R :=
```
PAST COMMENT (from reviewer):
In all of these definitions I would add "returns a junk value if P=Q" just to be clear that this is what's happening (I was confused at first when reviewing this PR, so maybe others will be confused when reading it). My confusion stems from the fact that I was incorrectly assuming that in projective coordinates you can get away with one formula for addition, but apparently this is not correct. I guess that in affine coordinates there are many formulae (P+0, P+P, 0+P, P+(-P) etc) so presumably there are still gains to be had with two formulae.

--- candidate 14 (sim=0.771, past_pr=#5294, file=Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean) ---
PAST HUNK:
```
@@ -0,0 +1,995 @@
... [816 lines above hidden]
+    Finsupp.add_apply, map_smul, Finsupp.smul_apply, ← basis_zero, ← basis_one,
+    Basis.repr_self_apply, if_pos, if_neg, smul_eq_mul]
+  ring1
+#align weierstrass_curve.coordinate_ring.norm_smul_basis WeierstrassCurve.CoordinateRing.norm_smul_basis
+
+lemma coe_norm_smul_basis (p q : R[X]) :
+    ↑(Algebra.norm R[X] <| p • (1 : W.CoordinateRing) + q • mk W Y) =
+      mk W ((C p + C q * X) * (C p + C q * (-Y - C (C W.a₁ * X + C W.a₃)))) :=
+  AdjoinRoot.mk_eq_mk.mpr
+    ⟨C q ^ 2, by simp only [norm_smul_basis, WeierstrassCurve.polynomial]; C_simp; ring1⟩
+#align weierstrass_curve.coordinate_ring.coe_norm_smul_basis WeierstrassCurve.CoordinateRing.coe_norm_smul_basis
+
+-- porting note: BUG `cases` tactic does not modify assumptions
```
PAST COMMENT (from reviewer):
Please move to identify where exactly this is failing, and restore (in comments) the original lines.

--- candidate 15 (sim=0.771, past_pr=#5294, file=Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean) ---
PAST HUNK:
```
@@ -0,0 +1,995 @@
... [854 lines above hidden]
+                      max_lt_iff.mpr ⟨hdp.trans_lt _, hdpq.trans_lt _⟩).trans
+              (max_eq_right_of_lt _).symm <;> rw [hdq] <;>
+              exact WithBot.coe_lt_coe.mpr <| by linarith only [hpq]
+          · rw [sub_sub]
+            convert (degree_sub_eq_left_of_degree_lt <| (degree_add_le _ _).trans_lt <|
+                      max_lt_iff.mpr ⟨hdpq.trans_lt _, hdq.trans_lt _⟩).trans
+              (max_eq_left_of_lt _).symm <;> rw [hdp] <;>
+              exact WithBot.coe_lt_coe.mpr <| by linarith only [hpq]
+#align weierstrass_curve.coordinate_ring.degree_norm_smul_basis WeierstrassCurve.CoordinateRing.degree_norm_smul_basis
+
+variable {W}
+
+-- porting note: replaced `dec_trivial` with explicit lemma
```
PAST COMMENT (from reviewer):
Again, please move to the exact location of the regression, so it's obvious without opening mathlib3 where one should hope to write `dec_trivial`.

--- candidate 16 (sim=0.757, past_pr=#18531, file=Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean) ---
PAST HUNK:
```
@@ -14,7 +14,7 @@ This file defines the type of points on a Weierstrass curve as an inductive, con
 at infinity and affine points satisfying a Weierstrass equation with a nonsingular condition. This
 file also defines the negation and addition operations of the group law for this type, and proves
 that they respect the Weierstrass equation and the nonsingular condition. The fact that they form an
-abelian group is proven in `Mathlib.AlgebraicGeometry.EllipticCurve.Group`.
+abelian group is proven in `Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean`.
```
PAST COMMENT (from reviewer):
I think this works?
```
under the geometric group law defined in `Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean` and
in `Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean`.
```

--- candidate 17 (sim=0.750, past_pr=#5841, file=Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean) ---
PAST HUNK:
```
@@ -35,6 +35,7 @@ splitting field of `R` are precisely the $X$-coordinates of the non-zero 2-torsi
 
  * `WeierstrassCurve`: a Weierstrass curve over a commutative ring.
  * `WeierstrassCurve.Δ`: the discriminant of a Weierstrass curve.
+ * `WeierstrassCurve.VariableChange`: a change of variable of Weierstrass curves.
```
PAST COMMENT (from reviewer):
I see - let's do `changeCurve` and `changeRing` then

--- candidate 18 (sim=0.750, past_pr=#5841, file=Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean) ---
PAST HUNK:
```
@@ -35,6 +35,7 @@ splitting field of `R` are precisely the $X$-coordinates of the non-zero 2-torsi
 
  * `WeierstrassCurve`: a Weierstrass curve over a commutative ring.
  * `WeierstrassCurve.Δ`: the discriminant of a Weierstrass curve.
+ * `WeierstrassCurve.VariableChange`: a change of variable of Weierstrass curves.
```
PAST COMMENT (from reviewer):
What about `changeCoordinate`? I'm trying to compare it with `baseChange` (which should probably be called `changeBase` if we decide to rename everything), where it's clear what we're changing (whereas `changeCurve` doesn't say exactly what). SageMath uses `change_ring`/`base_extend` and `change_weierstrass_model` (too long) while Magma uses `ChangeRing`/`BaseExtend`/`BaseChange` and no corresponding variable change function.

--- candidate 19 (sim=0.743, past_pr=#13448, file=Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean) ---
PAST HUNK:
```
@@ -634,7 +634,7 @@ inductive Point
 #align weierstrass_curve.point WeierstrassCurve.Affine.Point
 
 /-- For an algebraic extension `S` of `R`, the type of nonsingular `S`-rational points on `W`. -/
-scoped[WeierstrassCurve] notation3 W "⟮" S "⟯" => Affine.Point <| baseChange W S
+scoped[WeierstrassCurve] notation3:9000 W "⟮" S "⟯" => Affine.Point <| baseChange W S
```
PAST COMMENT (from reviewer):
I believe `notation3` uses the Lean 3 `notation` delaborator, which happens to be more flexible? I don't know what the arbitrary number `9000` is, but I would just do `notation3:max` like other places in the repo:
```suggestion
scoped[WeierstrassCurve] notation3:max W "⟮" S "⟯" => Affine.Point <| baseChange W S
```
I did something similar for `R[X][Y]` in #13356 (which is currently stuck in a merge but I've just fixed it).

--- candidate 20 (sim=0.741, past_pr=#24886, file=Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Formula.lean) ---
PAST HUNK:
```
@@ -10,10 +10,10 @@ import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
 
 Let `W` be a Weierstrass curve over a field `F` with coefficients `aᵢ`. The nonsingular affine
 points on `W` can be given negation and addition operations defined by a secant-and-tangent process.
- * Given a nonsingular affine point `P`, its *negation* `-P` is defined to be the unique third
+* Given a nonsingular affine point `P`, its *negation* `-P` is defined to be the unique third
     nonsingular point of intersection between `W` and the vertical line through `P`.
     Explicitly, if `P` is `(x, y)`, then `-P` is `(x, -y - a₁x - a₃)`.
- * Given two nonsingular affine points `P` and `Q`, their *addition* `P + Q` is defined to be the
+* Given two nonsingular affine points `P` and `Q`, their *addition* `P + Q` is defined to be the
     negation of the unique third nonsingular point of intersection between `W` and the line `L`
     through `P` and `Q`. Explicitly, let `P` be `(x₁, y₁)` and let `Q` be `(x₂, y₂)`.
       * If `x₁ = x₂` and `y₁ = -y₂ - a₁x₂ - a₃`, then `L` is vertical.
```
PAST COMMENT (from reviewer):
This one is still odd


Decide which candidates' comments genuinely apply to the NEW hunk. If none, say so. Output JSON only.

[ASSISTANT]
----------------------------------------------------------------------------------------------------
{
  "summary": "Docstring wording: prefer “typeclass asserting that …” over “typeclass saying that …” for `IsTateNF` in the top-level bullets.",
  "confidence": "high",
  "strong_matches": [
    {
      "past_pr": 18531,
      "past_file": "Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean",
      "past_comment_excerpt": "typeclass asserting that a Weierstrass curve is an elliptic curve.",
      "applies_because": "The new file’s bullet says “A typeclass saying that …”; prior feedback prefers the idiom “typeclass asserting that …” for such descriptions.",
      "suggested_adaptation": "Change the bullet to “`IsTateNF W`: a typeclass asserting that the Weierstrass curve `W` is in Tate normal form.”",
      "supporting_past_prs": [
        18531,
        16864
      ]
    }
  ],
  "weak_observations": [
    {
      "observation": "Including “returns 0 (junk value)” in the `X` coordinate docstring aligns with prior advice to note junk-return cases explicitly.",
      "supporting_past_prs": [
        9417
      ]
    }
  ]
}