chore(Algebra): improve IsTorsionFree.to_faithfulSMul (leanprover-community#34463)

... after leanprover-community#34203

Author: YaelDillies

Mathlib/Algebra/Algebra/Basic.lean

@@ -440,13 +440,13 @@ instance (priority := 100) FaithfulSMul.to_isTorsionFree [Nontrivial R] [IsCance
 end FaithfulSMul
 
 namespace Module
-variable {R A : Type*} [CommRing R] [IsDomain R] [Ring A] [Algebra R A]
+variable {R A : Type*} [CommRing R] [Ring A] [Algebra R A]
 
-instance IsTorsionFree.to_faithfulSMul [IsCancelMulZero R] [Nontrivial A]
+instance (priority := 101) IsTorsionFree.to_faithfulSMul [IsCancelMulZero R] [Nontrivial A]
     [IsTorsionFree R A] : FaithfulSMul R A where
   eq_of_smul_eq_smul h := smul_left_injective _ one_ne_zero <| h 1
 
-variable [IsDomain A]
+variable [IsDomain R] [IsDomain A]
 
 lemma isTorsionFree_iff_faithfulSMul : IsTorsionFree R A ↔ FaithfulSMul R A :=
   ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩