diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
index b480f80ad5a50..0582c0182b257 100644
--- a/Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
+++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
@@ -277,19 +277,30 @@ lemma nonsingular_iff_variableChange (x y : R) :
   simp only [variableChange]
   congr! 3 <;> ring1
 
-lemma nonsingular_zero_of_Δ_ne_zero (h : W'.Equation 0 0) (hΔ : W'.Δ ≠ 0) :
-    W'.Nonsingular 0 0 := by
-  simp only [equation_zero, nonsingular_zero] at *
+private lemma equation_zero_iff_nonsingular_zero_of_Δ_ne_zero (hΔ : W'.Δ ≠ 0) :
+    W'.Equation 0 0 ↔ W'.Nonsingular 0 0 := by
+  simp only [equation_zero, nonsingular_zero, iff_self_and]
   contrapose! hΔ
-  simp only [b₂, b₄, b₆, b₈, Δ, h, hΔ]
+  simp only [b₂, b₄, b₆, b₈, Δ, hΔ]
   ring1
 
 /-- A Weierstrass curve is nonsingular at every point if its discriminant is non-zero. -/
-lemma nonsingular_of_Δ_ne_zero {x y : R} (h : W'.Equation x y) (hΔ : W'.Δ ≠ 0) :
-    W'.Nonsingular x y :=
-  (nonsingular_iff_variableChange x y).mpr <|
-    nonsingular_zero_of_Δ_ne_zero ((equation_iff_variableChange x y).mp h) <| by
-      rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]
+lemma equation_iff_nonsingular_of_Δ_ne_zero {x y : R} (hΔ : W'.Δ ≠ 0) :
+    W'.Equation x y ↔ W'.Nonsingular x y := by
+  rw [equation_iff_variableChange, nonsingular_iff_variableChange,
+    equation_zero_iff_nonsingular_zero_of_Δ_ne_zero <| by
+      rwa [variableChange_Δ, inv_one, Units.val_one, one_pow, one_mul]]
+
+/-- An elliptic curve is nonsingular at every point. -/
+lemma equation_iff_nonsingular [Nontrivial R] [W'.IsElliptic] {x y : R} :
+    W'.toAffine.Equation x y ↔ W'.toAffine.Nonsingular x y :=
+  W'.toAffine.equation_iff_nonsingular_of_Δ_ne_zero <| W'.coe_Δ' ▸ W'.Δ'.ne_zero
+
+@[deprecated (since := "2025-03-01")] alias nonsingular_zero_of_Δ_ne_zero :=
+  equation_iff_nonsingular_of_Δ_ne_zero
+@[deprecated (since := "2025-03-01")] alias nonsingular_of_Δ_ne_zero :=
+  equation_iff_nonsingular_of_Δ_ne_zero
+@[deprecated (since := "2025-03-01")] alias nonsingular := equation_iff_nonsingular
 
 end Nonsingular
 
@@ -389,35 +400,27 @@ This depends on `W`, and has argument order: `x₁`, `x₂`, `y₁`, `ℓ`. -/
 def addY (x₁ x₂ y₁ ℓ : R) : R :=
   W'.negY (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
 
-lemma equation_neg_iff (x y : R) : W'.Equation x (W'.negY x y) ↔ W'.Equation x y := by
+lemma equation_neg (x y : R) : W'.Equation x (W'.negY x y) ↔ W'.Equation x y := by
   rw [equation_iff, equation_iff, negY]
   congr! 1
   ring1
 
-lemma nonsingular_neg_iff (x y : R) : W'.Nonsingular x (W'.negY x y) ↔ W'.Nonsingular x y := by
-  rw [nonsingular_iff, equation_neg_iff, ← negY, negY_negY, ← @ne_comm _ y, nonsingular_iff]
+@[deprecated (since := "2025-02-01")] alias equation_neg_of := equation_neg
+@[deprecated (since := "2025-02-01")] alias equation_neg_iff := equation_neg
+
+lemma nonsingular_neg (x y : R) : W'.Nonsingular x (W'.negY x y) ↔ W'.Nonsingular x y := by
+  rw [nonsingular_iff, equation_neg, ← negY, negY_negY, ← @ne_comm _ y, nonsingular_iff]
   exact and_congr_right' <| (iff_congr not_and_or.symm not_and_or.symm).mpr <|
     not_congr <| and_congr_left fun h => by rw [← h]
 
+@[deprecated (since := "2025-02-01")] alias nonsingular_neg_of := nonsingular_neg
+@[deprecated (since := "2025-02-01")] alias nonsingular_neg_iff := nonsingular_neg
+
 lemma equation_add_iff (x₁ x₂ y₁ ℓ : R) : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ) ↔
     (W'.addPolynomial x₁ y₁ ℓ).eval (W'.addX x₁ x₂ ℓ) = 0 := by
   rw [Equation, negAddY, addPolynomial, linePolynomial, polynomial]
   eval_simp
 
-lemma equation_neg_of {x y : R} (h : W'.Equation x <| W'.negY x y) : W'.Equation x y :=
-  (W'.equation_neg_iff ..).mp h
-
-/-- The negation of an affine point in `W` lies in `W`. -/
-lemma equation_neg {x y : R} (h : W'.Equation x y) : W'.Equation x <| W'.negY x y :=
-  (W'.equation_neg_iff ..).mpr h
-
-lemma nonsingular_neg_of {x y : R} (h : W'.Nonsingular x <| W'.negY x y) : W'.Nonsingular x y :=
-  (W'.nonsingular_neg_iff ..).mp h
-
-/-- The negation of a nonsingular affine point in `W` is nonsingular. -/
-lemma nonsingular_neg {x y : R} (h : W'.Nonsingular x y) : W'.Nonsingular x <| W'.negY x y :=
-  (W'.nonsingular_neg_iff ..).mpr h
-
 lemma nonsingular_negAdd_of_eval_derivative_ne_zero {x₁ x₂ y₁ ℓ : R}
     (hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ))
     (hx : (W'.addPolynomial x₁ y₁ ℓ).derivative.eval (W'.addX x₁ x₂ ℓ) ≠ 0) :
@@ -528,7 +531,7 @@ lemma equation_negAdd {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h
 lemma equation_add {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂)
     (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) :
     W.Equation (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂) (W.addY x₁ x₂ y₁ <| W.slope x₁ x₂ y₁ y₂) :=
-  equation_neg <| equation_negAdd h₁ h₂ hxy
+  (equation_neg ..).mpr <| equation_negAdd h₁ h₂ hxy
 
 lemma C_addPolynomial_slope {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂)
     (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) : C (W.addPolynomial x₁ y₁ <| W.slope x₁ x₂ y₁ y₂) =
@@ -567,7 +570,7 @@ lemma nonsingular_negAdd {x₁ x₂ y₁ y₂ : F} (h₁ : W.Nonsingular x₁ y
 lemma nonsingular_add {x₁ x₂ y₁ y₂ : F} (h₁ : W.Nonsingular x₁ y₁) (h₂ : W.Nonsingular x₂ y₂)
     (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) :
     W.Nonsingular (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂) (W.addY x₁ x₂ y₁ <| W.slope x₁ x₂ y₁ y₂) :=
-  nonsingular_neg <| nonsingular_negAdd h₁ h₂ hxy
+  (nonsingular_neg ..).mpr <| nonsingular_negAdd h₁ h₂ hxy
 
 /-- The formula `x(P₁ + P₂) = x(P₁ - P₂) - ψ(P₁)ψ(P₂) / (x(P₂) - x(P₁))²`,
 where `ψ(x,y) = 2y + a₁x + a₃`. -/
@@ -636,7 +639,7 @@ lemma some_ne_zero {x y : R} (h : W'.Nonsingular x y) : Point.some h ≠ 0 := by
 Given a nonsingular point `P` in affine coordinates, use `-P` instead of `neg P`. -/
 def neg : W'.Point → W'.Point
   | 0 => 0
-  | some h => some <| nonsingular_neg h
+  | some h => some <| (nonsingular_neg ..).mpr h
 
 instance : Neg W'.Point :=
   ⟨neg⟩
@@ -649,7 +652,7 @@ lemma neg_zero : (-0 : W'.Point) = 0 :=
   rfl
 
 @[simp]
-lemma neg_some {x y : R} (h : W'.Nonsingular x y) : -some h = some (nonsingular_neg h) :=
+lemma neg_some {x y : R} (h : W'.Nonsingular x y) : -some h = some ((nonsingular_neg ..).mpr h) :=
   rfl
 
 instance : InvolutiveNeg W'.Point where
@@ -668,10 +671,10 @@ noncomputable def add : W.Point → W.Point → W.Point
   | @some _ _ _ x₁ y₁ h₁, @some _ _ _ x₂ y₂ h₂ =>
     if hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂ then 0 else some <| nonsingular_add h₁ h₂ hxy
 
-noncomputable instance instAddPoint : Add W.Point :=
+noncomputable instance : Add W.Point :=
   ⟨add⟩
 
-noncomputable instance instAddZeroClassPoint : AddZeroClass W.Point :=
+noncomputable instance : AddZeroClass W.Point :=
   ⟨by rintro (_ | _) <;> rfl, by rintro (_ | _) <;> rfl⟩
 
 lemma add_def (P Q : W.Point) : P + Q = P.add Q :=
@@ -882,26 +885,24 @@ variable [Algebra R S] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebr
   [IsScalarTower R S K] [Algebra R L] [Algebra S L] [IsScalarTower R S L] (f : F →ₐ[S] K)
   (g : K →ₐ[S] L)
 
-/-- The function from `W⟮F⟯` to `W⟮K⟯` induced by an algebra homomorphism `f : F →ₐ[S] K`,
-where `W` is defined over a subring of a ring `S`, and `F` and `K` are field extensions of `S`. -/
-def mapFun : W'⟮F⟯ → W'⟮K⟯
-  | 0 => 0
-  | some h => some <| (baseChange_nonsingular _ _ f.injective).mpr h
-
 /-- The group homomorphism from `W⟮F⟯` to `W⟮K⟯` induced by an algebra homomorphism `f : F →ₐ[S] K`,
 where `W` is defined over a subring of a ring `S`, and `F` and `K` are field extensions of `S`. -/
 def map : W'⟮F⟯ →+ W'⟮K⟯ where
-  toFun := mapFun f
+  toFun P := match P with
+    | 0 => 0
+    | some h => some <| (baseChange_nonsingular _ _ f.injective).mpr h
   map_zero' := rfl
   map_add' := by
     rintro (_ | @⟨x₁, y₁, _⟩) (_ | @⟨x₂, y₂, _⟩)
     any_goals rfl
     by_cases hxy : x₁ = x₂ ∧ y₁ = (W'.baseChange F).toAffine.negY x₂ y₂
-    · simp only [add_of_Y_eq hxy.left hxy.right, mapFun]
+    · simp only [add_of_Y_eq hxy.left hxy.right]
       rw [add_of_Y_eq (congr_arg _ hxy.left) <| by rw [hxy.right, baseChange_negY]]
-    · simp only [add_some hxy, mapFun, ← baseChange_addX, ← baseChange_addY, ← baseChange_slope]
+    · simp only [add_some hxy, ← baseChange_addX, ← baseChange_addY, ← baseChange_slope]
       rw [add_some fun h => hxy ⟨f.injective h.1, f.injective (W'.baseChange_negY f .. ▸ h).2⟩]
 
+@[deprecated (since := "2025-03-01")] alias mapFun := map
+
 lemma map_zero : map f (0 : W'⟮F⟯) = 0 :=
   rfl
 
@@ -936,16 +937,4 @@ end Point
 
 end Affine
 
-/-! ## Elliptic curves -/
-
-section EllipticCurve
-
-variable {R : Type u} [CommRing R] (E : WeierstrassCurve R) [E.IsElliptic]
-
-lemma nonsingular [Nontrivial R] {x y : R} (h : E.toAffine.Equation x y) :
-    E.toAffine.Nonsingular x y :=
-  E.toAffine.nonsingular_of_Δ_ne_zero h <| E.coe_Δ' ▸ E.Δ'.ne_zero
-
-end EllipticCurve
-
 end WeierstrassCurve
diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
index d3ac4126c2796..9b609f1a5ecac 100644
--- a/Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
+++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
@@ -398,19 +398,21 @@ lemma XYIdeal'_eq {x y : F} (h : W.Nonsingular x y) :
     (XYIdeal' h : FractionalIdeal W.CoordinateRing⁰ W.FunctionField) = XYIdeal W x (C y) :=
   rfl
 
-lemma mk_XYIdeal'_mul_mk_XYIdeal'_of_Yeq {x y : F} (h : W.Nonsingular x y) :
-    ClassGroup.mk (XYIdeal' <| nonsingular_neg h) * ClassGroup.mk (XYIdeal' h) = 1 := by
+lemma mk_XYIdeal'_neg_mul {x y : F} (h : W.Nonsingular x y) :
+    ClassGroup.mk (XYIdeal' <| (nonsingular_neg ..).mpr h) * ClassGroup.mk (XYIdeal' h) = 1 := by
   rw [← _root_.map_mul]
-  exact
-    (ClassGroup.mk_eq_one_of_coe_ideal <| by exact (FractionalIdeal.coeIdeal_mul ..).symm.trans <|
-      FractionalIdeal.coeIdeal_inj.mpr <| XYIdeal_neg_mul h).mpr ⟨_, XClass_ne_zero W _, rfl⟩
+  exact (ClassGroup.mk_eq_one_of_coe_ideal <| (FractionalIdeal.coeIdeal_mul ..).symm.trans <|
+    FractionalIdeal.coeIdeal_inj.mpr <| XYIdeal_neg_mul h).mpr ⟨_, XClass_ne_zero W _, rfl⟩
+
+@[deprecated (since := "2025-03-01")] alias mk_XYIdeal'_mul_mk_XYIdeal'_of_Yeq :=
+  mk_XYIdeal'_neg_mul
 
 lemma mk_XYIdeal'_mul_mk_XYIdeal' {x₁ x₂ y₁ y₂ : F} (h₁ : W.Nonsingular x₁ y₁)
     (h₂ : W.Nonsingular x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) :
     ClassGroup.mk (XYIdeal' h₁) * ClassGroup.mk (XYIdeal' h₂) =
       ClassGroup.mk (XYIdeal' <| nonsingular_add h₁ h₂ hxy) := by
   rw [← _root_.map_mul]
-  exact (ClassGroup.mk_eq_mk_of_coe_ideal (by exact (FractionalIdeal.coeIdeal_mul ..).symm) <|
+  exact (ClassGroup.mk_eq_mk_of_coe_ideal (FractionalIdeal.coeIdeal_mul ..).symm <|
       XYIdeal'_eq _).mpr
     ⟨_, _, XClass_ne_zero W _, YClass_ne_zero W _, XYIdeal_mul_XYIdeal h₁.left h₂.left hxy⟩
 
@@ -496,28 +498,25 @@ namespace Point
 
 variable {F : Type u} [Field F] {W : Affine F}
 
-/-- The set function mapping a nonsingular affine point `(x, y)` of a Weierstrass curve `W` to the
-class of the non-zero fractional ideal `⟨X - x, Y - y⟩` in the ideal class group of `F[W]`. -/
-@[simp]
-noncomputable def toClassFun : W.Point → Additive (ClassGroup W.CoordinateRing)
-  | 0 => 0
-  | some h => Additive.ofMul <| ClassGroup.mk <| CoordinateRing.XYIdeal' h
-
 /-- The group homomorphism mapping a nonsingular affine point `(x, y)` of a Weierstrass curve `W` to
 the class of the non-zero fractional ideal `⟨X - x, Y - y⟩` in the ideal class group of `F[W]`. -/
 @[simps]
 noncomputable def toClass : W.Point →+ Additive (ClassGroup W.CoordinateRing) where
-  toFun := toClassFun
+  toFun P := match P with
+    | 0 => 0
+    | some h => Additive.ofMul <| ClassGroup.mk <| CoordinateRing.XYIdeal' h
   map_zero' := rfl
   map_add' := by
     rintro (_ | @⟨x₁, y₁, h₁⟩) (_ | @⟨x₂, y₂, h₂⟩)
-    any_goals simp only [toClassFun, ← zero_def, zero_add, add_zero]
+    any_goals simp only [← zero_def, zero_add, add_zero]
     by_cases hxy : x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
     · simp only [hxy.left, hxy.right, add_of_Y_eq rfl rfl]
-      exact (CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal'_of_Yeq h₂).symm
+      exact (CoordinateRing.mk_XYIdeal'_neg_mul h₂).symm
     · simp only [add_some hxy]
       exact (CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal' h₁ h₂ hxy).symm
 
+@[deprecated (since := "2025-02-01")] alias toClassFun := toClass
+
 lemma toClass_zero : toClass (0 : W.Point) = 0 :=
   rfl
 
@@ -544,15 +543,14 @@ lemma toClass_eq_zero (P : W.Point) : toClass P = 0 ↔ P = 0 := by
       apply (p.natDegree_norm_ne_one _).elim
       rw [← finrank_quotient_span_eq_natDegree_norm (CoordinateRing.basis W) h0,
         ← (quotientEquivAlgOfEq F hp).toLinearEquiv.finrank_eq,
-        (CoordinateRing.quotientXYIdealEquiv W h).toLinearEquiv.finrank_eq,
-        Module.finrank_self]
+        (CoordinateRing.quotientXYIdealEquiv W h).toLinearEquiv.finrank_eq, Module.finrank_self]
   · exact congr_arg toClass
 
 lemma toClass_injective : Function.Injective <| @toClass _ _ W := by
   rintro (_ | h) _ hP
   all_goals rw [← neg_inj, ← add_eq_zero, ← toClass_eq_zero, map_add, ← hP]
   · exact zero_add 0
-  · exact CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal'_of_Yeq h
+  · exact CoordinateRing.mk_XYIdeal'_neg_mul h
 
 noncomputable instance : AddCommGroup W.Point where
   nsmul := nsmulRec
@@ -615,6 +613,6 @@ variable {R : Type*} [Nontrivial R] [CommRing R] (E : WeierstrassCurve R) [E.IsE
 
 /-- An affine point on an elliptic curve `E` over a commutative ring `R`. -/
 def mk {x y : R} (h : E.toAffine.Equation x y) : E.toAffine.Point :=
-  WeierstrassCurve.Affine.Point.some <| nonsingular E h
+  .some <| (equation_iff_nonsingular ..).mp h
 
 end WeierstrassCurve.Affine.Point
diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
index a1c06467a6015..51830aece0ae7 100644
--- a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
+++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
@@ -184,7 +184,7 @@ section Jacobian
 /-! ### Jacobian coordinates -/
 
 /-- The scalar multiplication for a Jacobian point representative on a Weierstrass curve. -/
-scoped instance instSMulPoint : SMul R <| Fin 3 → R :=
+scoped instance : SMul R <| Fin 3 → R :=
   ⟨fun u P => ![u ^ 2 * P x, u ^ 3 * P y, u * P z]⟩
 
 lemma smul_fin3 (P : Fin 3 → R) (u : R) : u • P = ![u ^ 2 * P x, u ^ 3 * P y, u * P z] :=
@@ -200,12 +200,13 @@ lemma comp_smul (f : R →+* S) (P : Fin 3 → R) (u : R) : f ∘ (u • P) = f
 @[deprecated (since := "2025-01-30")] alias map_smul := comp_smul
 
 /-- The multiplicative action for a Jacobian point representative on a Weierstrass curve. -/
-scoped instance instMulActionPoint : MulAction R <| Fin 3 → R where
+scoped instance : MulAction R <| Fin 3 → R where
   one_smul _ := by simp_rw [smul_fin3, one_pow, one_mul, fin3_def]
   mul_smul _ _ _ := by simp_rw [smul_fin3, mul_pow, mul_assoc, fin3_def_ext]
 
 /-- The equivalence setoid for a Jacobian point representative on a Weierstrass curve. -/
-@[reducible] scoped instance instSetoidPoint : Setoid <| Fin 3 → R :=
+@[reducible]
+scoped instance : Setoid <| Fin 3 → R :=
   MulAction.orbitRel Rˣ <| Fin 3 → R
 
 variable (R) in
@@ -1238,7 +1239,8 @@ lemma neg_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
 
 private lemma nonsingular_neg_of_Z_ne_zero {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P z ≠ 0) :
     W.Nonsingular ![P x / P z ^ 2, W.toAffine.negY (P x / P z ^ 2) (P y / P z ^ 3), 1] :=
-  (nonsingular_some ..).mpr <| Affine.nonsingular_neg <| (nonsingular_of_Z_ne_zero hPz).mp hP
+  (nonsingular_some ..).mpr <| (Affine.nonsingular_neg ..).mpr <|
+    (nonsingular_of_Z_ne_zero hPz).mp hP
 
 lemma nonsingular_neg {P : Fin 3 → F} (hP : W.Nonsingular P) : W.Nonsingular <| W.neg P := by
   by_cases hPz : P z = 0
@@ -1490,7 +1492,7 @@ namespace Point
 lemma mk_point {P : PointClass R} (h : W'.NonsingularLift P) : (mk h).point = P :=
   rfl
 
-instance instZeroPoint [Nontrivial R] : Zero W'.Point :=
+instance [Nontrivial R] : Zero W'.Point :=
   ⟨⟨nonsingularLift_zero⟩⟩
 
 lemma zero_def [Nontrivial R] : (0 : W'.Point) = ⟨nonsingularLift_zero⟩ :=
@@ -1523,7 +1525,7 @@ Given a nonsingular Jacobian point `P` on `W`, use `-P` instead of `neg P`. -/
 def neg (P : W.Point) : W.Point :=
   ⟨nonsingularLift_negMap P.nonsingular⟩
 
-instance instNegPoint : Neg W.Point :=
+instance : Neg W.Point :=
   ⟨neg⟩
 
 lemma neg_def (P : W.Point) : -P = P.neg :=
@@ -1538,7 +1540,7 @@ Given two nonsingular Jacobian points `P` and `Q` on `W`, use `P + Q` instead of
 noncomputable def add (P Q : W.Point) : W.Point :=
   ⟨nonsingularLift_addMap P.nonsingular Q.nonsingular⟩
 
-noncomputable instance instAddPoint : Add W.Point :=
+noncomputable instance : Add W.Point :=
   ⟨add⟩
 
 lemma add_def (P Q : W.Point) : P + Q = P.add Q :=
diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
index 86240548967aa..a4897eac2f0af 100644
--- a/Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
+++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
@@ -196,7 +196,7 @@ lemma comp_smul (f : R →+* S) (P : Fin 3 → R) (u : R) : f ∘ (u • P) = f
   ext n; fin_cases n <;> simp only [smul_fin3, comp_fin3] <;> map_simp
 
 /-- The equivalence setoid for a projective point representative on a Weierstrass curve. -/
-scoped instance instSetoidPoint : Setoid <| Fin 3 → R :=
+scoped instance : Setoid <| Fin 3 → R :=
   MulAction.orbitRel Rˣ <| Fin 3 → R
 
 variable (R) in
@@ -1320,7 +1320,8 @@ lemma neg_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
 
 private lemma nonsingular_neg_of_Z_ne_zero {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P z ≠ 0) :
     W.Nonsingular ![P x / P z, W.toAffine.negY (P x / P z) (P y / P z), 1] :=
-  (nonsingular_some ..).mpr <| Affine.nonsingular_neg <| (nonsingular_of_Z_ne_zero hPz).mp hP
+  (nonsingular_some ..).mpr <| (Affine.nonsingular_neg ..).mpr <|
+    (nonsingular_of_Z_ne_zero hPz).mp hP
 
 lemma nonsingular_neg {P : Fin 3 → F} (hP : W.Nonsingular P) : W.Nonsingular <| W.neg P := by
   by_cases hPz : P z = 0
@@ -1567,7 +1568,7 @@ namespace Point
 lemma mk_point {P : PointClass R} (h : W'.NonsingularLift P) : (mk h).point = P :=
   rfl
 
-instance instZeroPoint [Nontrivial R] : Zero W'.Point :=
+instance [Nontrivial R] : Zero W'.Point :=
   ⟨⟨nonsingularLift_zero⟩⟩
 
 lemma zero_def [Nontrivial R] : (0 : W'.Point) = ⟨nonsingularLift_zero⟩ :=
@@ -1600,7 +1601,7 @@ Given a nonsingular projective point `P` on `W`, use `-P` instead of `neg P`. -/
 def neg (P : W.Point) : W.Point :=
   ⟨nonsingularLift_negMap P.nonsingular⟩
 
-instance instNegPoint : Neg W.Point :=
+instance : Neg W.Point :=
   ⟨neg⟩
 
 lemma neg_def (P : W.Point) : -P = P.neg :=
@@ -1615,7 +1616,7 @@ Given two nonsingular projective points `P` and `Q` on `W`, use `P + Q` instead
 noncomputable def add (P Q : W.Point) : W.Point :=
   ⟨nonsingularLift_addMap P.nonsingular Q.nonsingular⟩
 
-noncomputable instance instAddPoint : Add W.Point :=
+noncomputable instance : Add W.Point :=
   ⟨add⟩
 
 lemma add_def (P Q : W.Point) : P + Q = P.add Q :=