chore(RingTheory/AdjoinRoot): clean up instances (leanprover-community#37127)

Clean up `AdjoinRoot` instances using `inferInstanceAs`.

Author: JovanGerb

Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean

@@ -110,7 +110,6 @@ noncomputable instance : Algebra R[X] W'.CoordinateRing :=
 instance : IsScalarTower R R[X] W'.CoordinateRing :=
   Quotient.isScalarTower R R[X] _
 
-set_option backward.isDefEq.respectTransparency false in
 instance [Subsingleton R] : Subsingleton W'.CoordinateRing :=
   Module.subsingleton R[X] _
 
@@ -119,7 +118,6 @@ variable (W') in
 noncomputable abbrev mk : R[X][Y] →+* W'.CoordinateRing :=
   AdjoinRoot.mk W'.polynomial
 
-set_option backward.isDefEq.respectTransparency false in
 open scoped Classical in
 variable (W') in
 /-- The power basis `{1, Y}` for `R[W]` over `R[X]`. -/
@@ -148,18 +146,15 @@ lemma coe_basis : (CoordinateRing.basis W' : Fin 2 → W'.CoordinateRing) = ![1,
   fin_cases n
   exacts [basis_zero, basis_one]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma smul (x : R[X]) (y : W'.CoordinateRing) : x • y = mk W' (C x) * y :=
   (algebraMap_smul W'.CoordinateRing x y).symm
 
-set_option backward.isDefEq.respectTransparency false in
 lemma smul_basis_eq_zero {p q : R[X]} (hpq : p • (1 : W'.CoordinateRing) + q • mk W' Y = 0) :
     p = 0 ∧ q = 0 := by
   have h := Fintype.linearIndependent_iff.mp (CoordinateRing.basis W').linearIndependent ![p, q]
   rw [Fin.sum_univ_succ, basis_zero, Fin.sum_univ_one, Fin.succ_zero_eq_one, basis_one] at h
   exact ⟨h hpq 0, h hpq 1⟩
 
-set_option backward.isDefEq.respectTransparency false in
 lemma exists_smul_basis_eq (x : W'.CoordinateRing) :
     ∃ p q : R[X], p • (1 : W'.CoordinateRing) + q • mk W' Y = x := by
   have h := (CoordinateRing.basis W').sum_equivFun x
@@ -408,7 +403,6 @@ lemma mk_XYIdeal'_mul_mk_XYIdeal' [DecidableEq F] {x₁ x₂ y₁ y₂ : F} (h
 
 /-! ## Norms on the affine coordinate ring -/
 
-set_option backward.isDefEq.respectTransparency false in
 lemma norm_smul_basis (p q : R[X]) : Algebra.norm R[X] (p • (1 : W'.CoordinateRing) + q • mk W' Y) =
     p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) -
       q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) := by
@@ -751,6 +745,7 @@ private lemma add_eq_zero (P Q : W.Point) : P + Q = 0 ↔ P = -Q := by
       exact fun hxy => by simpa only [add_some hxy] using some_ne_zero _
     · exact fun ⟨hx, hy⟩ => add_of_Y_eq hx hy
 
+set_option backward.isDefEq.respectTransparency false in
 lemma toClass_eq_zero (P : W.Point) : toClass P = 0 ↔ P = 0 := by
   constructor
   · intro hP

Mathlib/RingTheory/AdjoinRoot.lean

@@ -68,11 +68,7 @@ section CommRing
 
 variable [CommRing R] (f g : R[X])
 
-instance instCommRing : CommRing (AdjoinRoot f) :=
-  Ideal.Quotient.commRing _
-
-instance : Inhabited (AdjoinRoot f) :=
-  ⟨0⟩
+deriving instance CommRing, Inhabited for AdjoinRoot
 
 instance : DecidableEq (AdjoinRoot f) :=
   Classical.decEq _
@@ -97,10 +93,10 @@ def of : R →+* AdjoinRoot f :=
   (mk f).comp C
 
 instance instSMulAdjoinRoot [DistribSMul S R] [IsScalarTower S R R] : SMul S (AdjoinRoot f) :=
-  Submodule.Quotient.instSMul' _
+  inferInstanceAs <| SMul S (_ ⧸ _)
 
 instance [DistribSMul S R] [IsScalarTower S R R] : DistribSMul S (AdjoinRoot f) :=
-  Submodule.Quotient.distribSMul' _
+  inferInstanceAs <| DistribSMul S (_ ⧸ _)
 
 @[simp]
 theorem smul_mk [DistribSMul S R] [IsScalarTower S R R] (a : S) (x : R[X]) :
@@ -113,25 +109,25 @@ theorem smul_of [DistribSMul S R] [IsScalarTower S R R] (a : S) (x : R) :
 instance (R₁ R₂ : Type*) [SMul R₁ R₂] [DistribSMul R₁ R] [DistribSMul R₂ R] [IsScalarTower R₁ R R]
     [IsScalarTower R₂ R R] [IsScalarTower R₁ R₂ R] (f : R[X]) :
     IsScalarTower R₁ R₂ (AdjoinRoot f) :=
-  Submodule.Quotient.isScalarTower _ _
+  inferInstanceAs <| IsScalarTower R₁ R₂ (_ ⧸ _)
 
 instance (R₁ R₂ : Type*) [DistribSMul R₁ R] [DistribSMul R₂ R] [IsScalarTower R₁ R R]
     [IsScalarTower R₂ R R] [SMulCommClass R₁ R₂ R] (f : R[X]) :
     SMulCommClass R₁ R₂ (AdjoinRoot f) :=
-  Submodule.Quotient.smulCommClass _ _
+  inferInstanceAs <| SMulCommClass R₁ R₂ (_ ⧸ _)
 
 instance isScalarTower_right [DistribSMul S R] [IsScalarTower S R R] :
     IsScalarTower S (AdjoinRoot f) (AdjoinRoot f) :=
-  Ideal.Quotient.isScalarTower_right
+  inferInstanceAs <| IsScalarTower S (_ ⧸ _) (_ ⧸ _)
 
 instance [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (f : R[X]) :
     DistribMulAction S (AdjoinRoot f) :=
-  Submodule.Quotient.distribMulAction' _
+  inferInstanceAs <| DistribMulAction S (_ ⧸ _)
 
 /-- `R[x]/(f)` is `R`-algebra -/
 @[stacks 09FX "second part"]
 instance [CommSemiring S] [Algebra S R] : Algebra S (AdjoinRoot f) :=
-  Ideal.Quotient.algebra S
+  inferInstanceAs <| Algebra S (_ ⧸ _)
 
 /- TODO : generalise base ring -/
 /-- `R`-algebra homomorphism from `R[x]` to `AdjoinRoot f` sending `X` to the `root`. -/
@@ -152,11 +148,12 @@ theorem algebraMap_eq' [CommSemiring S] [Algebra S R] :
   rfl
 
 instance finiteType [CommSemiring S] [Algebra S R] [FiniteType S R] :
-    FiniteType S (AdjoinRoot f) := by
-  unfold AdjoinRoot; infer_instance
+    FiniteType S (AdjoinRoot f) :=
+  inferInstanceAs <| FiniteType S (_ ⧸ (_ : Ideal R[X]))
 
 instance finitePresentation [CommRing S] [Algebra S R] [FinitePresentation S R] :
-    FinitePresentation S (AdjoinRoot f) := .quotient (Submodule.fg_span_singleton f)
+    FinitePresentation S (AdjoinRoot f) :=
+  .quotient (Submodule.fg_span_singleton f)
 
 /-- The adjoined root. -/
 def root : AdjoinRoot f :=
@@ -400,7 +397,6 @@ theorem isDomain_of_prime (hf : Prime f) : IsDomain (AdjoinRoot f) :=
   (Ideal.Quotient.isDomain_iff_prime (span {f} : Ideal R[X])).mpr <|
     (Ideal.span_singleton_prime hf.ne_zero).mpr hf
 
-set_option backward.isDefEq.respectTransparency false in
 theorem noZeroSMulDivisors_of_prime_of_degree_ne_zero [IsDomain R] (hf : Prime f)
     (hf' : f.degree ≠ 0) : IsTorsionFree R (AdjoinRoot f) :=
   haveI := isDomain_of_prime hf
@@ -551,7 +547,7 @@ instance span_maximal_of_irreducible [Fact (Irreducible f)] : (span {f}).IsMaxim
   PrincipalIdealRing.isMaximal_of_irreducible <| Fact.out
 
 noncomputable instance instGroupWithZero [Fact (Irreducible f)] : GroupWithZero (AdjoinRoot f) :=
-  Quotient.groupWithZero (span {f} : Ideal K[X])
+  fast_instance% Quotient.groupWithZero (span {f} : Ideal K[X])
 
 /-- If `R` is a field and `f` is irreducible, then `AdjoinRoot f` is a field -/
 @[stacks 09FX "first part, see also 09FI"]
@@ -601,7 +597,6 @@ variable [CommRing R] {g : R[X]}
 theorem isIntegral_root' (hg : g.Monic) : IsIntegral R (root g) :=
   ⟨g, hg, eval₂_root g⟩
 
-set_option backward.isDefEq.respectTransparency false in
 /-- `AdjoinRoot.modByMonicHom` sends the equivalence class of `f` mod `g` to `f %ₘ g`.
 
 This is a well-defined right inverse to `AdjoinRoot.mk`, see `AdjoinRoot.mk_leftInverse`. -/
@@ -624,7 +619,6 @@ theorem mk_leftInverse (hg : g.Monic) : Function.LeftInverse (mk g) (modByMonicH
 theorem mk_surjective : Function.Surjective (mk g) :=
   Ideal.Quotient.mk_surjective
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The elements `1, root g, ..., root g ^ (d - 1)` form a basis for `AdjoinRoot g`,
 where `g` is a monic polynomial of degree `d`. -/
 def powerBasisAux' (hg : g.Monic) : Basis (Fin g.natDegree) R (AdjoinRoot g) :=
@@ -652,14 +646,12 @@ def powerBasisAux' (hg : g.Monic) : Basis (Fin g.natDegree) R (AdjoinRoot g) :=
 -- This lemma could be autogenerated by `@[simps]` but unfortunately that would require
 -- unfolding that causes a timeout.
 -- This lemma should have the simp tag but this causes a lint issue.
-set_option backward.isDefEq.respectTransparency false in
 theorem powerBasisAux'_repr_symm_apply (hg : g.Monic) (c : Fin g.natDegree →₀ R) :
     (powerBasisAux' hg).repr.symm c = mk g (∑ i : Fin _, monomial i (c i)) :=
   rfl
 
 -- This lemma could be autogenerated by `@[simps]` but unfortunately that would require
 -- unfolding that causes a timeout.
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem powerBasisAux'_repr_apply_to_fun (hg : g.Monic) (f : AdjoinRoot g) (i : Fin g.natDegree) :
     (powerBasisAux' hg).repr f i = (modByMonicHom hg f).coeff ↑i :=
@@ -683,11 +675,9 @@ def powerBasis' (hg : g.Monic) : PowerBasis R (AdjoinRoot g) where
       have := Finset.mem_univ i
       contradiction
 
-set_option backward.isDefEq.respectTransparency false in
 lemma _root_.Polynomial.Monic.free_adjoinRoot (hg : g.Monic) : Module.Free R (AdjoinRoot g) :=
   .of_basis (powerBasis' hg).basis
 
-set_option backward.isDefEq.respectTransparency false in
 lemma _root_.Polynomial.Monic.finite_adjoinRoot (hg : g.Monic) : Module.Finite R (AdjoinRoot g) :=
   .of_basis (powerBasis' hg).basis
 
@@ -724,7 +714,6 @@ theorem minpoly_root (hf : f ≠ 0) : minpoly K (root f) = f * C f.leadingCoeff
     · exact q_monic.ne_zero
   · rwa [Ne, C_eq_zero, inv_eq_zero, leadingCoeff_eq_zero]
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The elements `1, root f, ..., root f ^ (d - 1)` form a basis for `AdjoinRoot f`,
 where `f` is an irreducible polynomial over a field of degree `d`. -/
 def powerBasisAux (hf : f ≠ 0) : Basis (Fin f.natDegree) K (AdjoinRoot f) := by
@@ -1084,7 +1073,6 @@ theorem Irreducible.exists_dvd_monic_irreducible_of_isIntegral {K L : Type*}
   have h3 := (AdjoinRoot.minpoly_root h) ▸ minpoly.dvd_map_of_isScalarTower K L (AdjoinRoot.root f)
   exact ⟨_, minpoly.monic h2, minpoly.irreducible h2, dvd_of_mul_right_dvd h3⟩
 
-set_option backward.isDefEq.respectTransparency false in
 /-- If `p : R[X]` is monic, then there exists a finite free extension of `R` that splits `p`. -/
 lemma Polynomial.Monic.exists_splits_map.{u}
     {R : Type u} [CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) :