diff --git a/Mathlib/RingTheory/Smooth/Basic.lean b/Mathlib/RingTheory/Smooth/Basic.lean
index c3fbf0a1423383..f0fd4687f0867c 100644
--- a/Mathlib/RingTheory/Smooth/Basic.lean
+++ b/Mathlib/RingTheory/Smooth/Basic.lean
@@ -108,7 +108,7 @@ lemma FormallySmooth.comp_surjective [FormallySmooth R A] (I : Ideal B) (hI : I
   exact ⟨l.comp g, by rw [← AlgHom.comp_assoc, ← this, AlgHom.comp_assoc, hg, AlgHom.comp_id]⟩
 
 set_option backward.isDefEq.respectTransparency false in
-instance mvPolynomial (σ : Type*) : FormallySmooth R (MvPolynomial σ R) := by
+instance instFormallySmoothMvPolynomial (σ : Type*) : FormallySmooth R (MvPolynomial σ R) := by
   let P : Generators R (MvPolynomial σ R) σ :=
     .ofSurjective X (by simp [aeval_X_left, Function.Surjective])
   have : Subsingleton ↥P.toExtension.ker :=
@@ -118,6 +118,8 @@ instance mvPolynomial (σ : Type*) : FormallySmooth R (MvPolynomial σ R) := by
   have := P.toExtension.h1Cotangentι_injective.subsingleton
   exact ⟨inferInstance, P.equivH1Cotangent.symm.subsingleton⟩
 
+@[deprecated (since := "2026-05-22")] alias mvPolynomial := instFormallySmoothMvPolynomial
+
 end
 
 namespace FormallySmooth
diff --git a/Mathlib/RingTheory/Smooth/Quotient.lean b/Mathlib/RingTheory/Smooth/Quotient.lean
index 039c9fdb9e1a5d..1ec859b7b3ccc9 100644
--- a/Mathlib/RingTheory/Smooth/Quotient.lean
+++ b/Mathlib/RingTheory/Smooth/Quotient.lean
@@ -104,14 +104,14 @@ lemma Algebra.FormallySmooth.of_surjective_of_ker_eq_map_of_flat [Module.Flat R
     (sq0 : (RingHom.ker (algebraMap R R')) ^ 2 = ⊥) (smoothq : Algebra.FormallySmooth R' S') :
     Algebra.FormallySmooth R S := by
   let P := (Algebra.Generators.self R S).toExtension
-  let : Algebra.FormallySmooth R P.Ring := Algebra.mvPolynomial S
+  let : Algebra.FormallySmooth R P.Ring := instFormallySmoothMvPolynomial S
   let IP := (RingHom.ker (algebraMap R R')).map (algebraMap R P.Ring)
   let Gen : Algebra.Generators R' S' S := {
     val := algebraMap S S'
     σ' := fun s' ↦ MvPolynomial.X (Classical.choose (surjS s'))
     aeval_val_σ' s' := by simp [Classical.choose_spec (surjS s')] }
   let P' := Gen.toExtension
-  let : Algebra.FormallySmooth R' P'.Ring := Algebra.mvPolynomial S
+  let : Algebra.FormallySmooth R' P'.Ring := instFormallySmoothMvPolynomial S
   let : Algebra P.Ring P'.Ring := MvPolynomial.algebraMvPolynomial
   let : IsScalarTower R P.Ring P'.Ring :=
     IsScalarTower.of_algebraMap_eq (fun x ↦ (MvPolynomial.map_C _ x).symm)