chore(RingTheory/TensorProduct): extra lemmas about {nat,int}Cast (#…

…7391)

Mathlib/RingTheory/TensorProduct.lean

@@ -226,6 +226,9 @@ instance : AddMonoidWithOne (A ⊗[R] B) where
 
 theorem natCast_def (n : ℕ) : (n : A ⊗[R] B) = (n : A) ⊗ₜ (1 : B) := rfl
 
+theorem natCast_def' (n : ℕ) : (n : A ⊗[R] B) = (1 : A) ⊗ₜ (n : B) := by
+  rw [natCast_def, ←nsmul_one, smul_tmul, nsmul_one]
+
 instance : AddCommMonoid (A ⊗[R] B) := by infer_instance
 
 -- providing this instance separately makes some downstream code substantially faster
@@ -410,6 +413,9 @@ instance instRing : Ring (A ⊗[R] B) where
 
 theorem intCast_def (z : ℤ) : (z : A ⊗[R] B) = (z : A) ⊗ₜ (1 : B) := rfl
 
+theorem intCast_def' (z : ℤ) : (z : A ⊗[R] B) = (1 : A) ⊗ₜ (z : B) := by
+  rw [intCast_def, ←zsmul_one, smul_tmul, zsmul_one]
+
 -- verify there are no diamonds
 example : (instRing : Ring (A ⊗[R] B)).toAddCommGroup = addCommGroup := rfl
 example : (algebraInt _ : Algebra ℤ (ℤ ⊗[ℤ] B)) = leftAlgebra := rfl