tiny change

Author: themathqueen

Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean

@@ -54,7 +54,7 @@ lemma includeLeftSubRight_apply (s : S) : includeLeftSubRight R S s = s ⊗ₜ[R
 lemma includeLeftSubRight_zero_of_mem_range {s : S} (hs : s ∈ Set.range ⇑(algebraMap R S)) :
     includeLeftSubRight R S s = 0 := by
   obtain ⟨_, hr⟩ := Set.mem_range.mp hs
-  simp [includeLeftSubRight, ← hr, algebraMap_eq_smul_one]
+  simp [← hr, algebraMap_eq_smul_one]
 
 /-- `includeLeftSubRight R S` vanishes at `algebraMap R S r`. -/
 lemma includeLeftSubRight_algebraMap_zero (r : R) :