chore(RingTheory/LocalRing/ResidueField): deprecateisLocalHom_residue (#28497)

Author: euprunin

Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean

@@ -187,13 +187,8 @@ end FiniteDimensional
 
 end ResidueField
 
-theorem isLocalHom_residue : IsLocalHom (IsLocalRing.residue R) := by
-  constructor
-  intro a ha
-  by_contra h
-  rw [residue_def, Ideal.Quotient.eq_zero_iff_mem.mpr ((IsLocalRing.mem_maximalIdeal _).mpr h)]
-    at ha
-  exact ha.ne_zero rfl
+@[deprecated (since := "2025-10-06")]
+  alias isLocalHom_residue := instIsLocalHomResidueFieldRingHomResidue
 
 end
 

Mathlib/RingTheory/Valuation/ValuationSubring.lean

@@ -642,9 +642,8 @@ theorem ker_unitGroupToResidueFieldUnits :
 
 theorem surjective_unitGroupToResidueFieldUnits :
     Function.Surjective A.unitGroupToResidueFieldUnits :=
-  (IsLocalRing.surjective_units_map_of_local_ringHom _ Ideal.Quotient.mk_surjective
-        IsLocalRing.isLocalHom_residue).comp
-    (MulEquiv.surjective _)
+  IsLocalRing.surjective_units_map_of_local_ringHom _ Ideal.Quotient.mk_surjective
+    (inferInstanceAs (IsLocalHom (IsLocalRing.residue A))) |>.comp (MulEquiv.surjective _)
 
 /-- The quotient of the unit group of `A` by the principal unit group of `A` agrees with
 the units of the residue field of `A`. -/