diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean
index d721b86182279..cb560fa0c3763 100644
--- a/src/algebra/algebra/basic.lean
+++ b/src/algebra/algebra/basic.lean
@@ -808,6 +808,10 @@ by rw [←(one_smul A m), ←smul_assoc, algebra.smul_def, mul_one, one_smul]
 @[simp] lemma algebra_map_smul (r : R) (m : M) : ((algebra_map R A) r) • m = r • m :=
 (algebra_compatible_smul A r m).symm
 
+-- @[simp] lemma op_algebra_map_smul [module Rᵐᵒᵖ M] [module Aᵐᵒᵖ M] (r : R) (m : M) :
+--   mul_opposite.op ((algebra_map R A) r) • m = mul_opposite.op r • m :=
+-- by rw [←(one_smul Aᵐᵒᵖ m), ←smul_assoc, smul_eq_mul, mul_one]
+
 lemma int_cast_smul {k V : Type*} [comm_ring k] [add_comm_group V] [module k V] (r : ℤ) (x : V) :
   (r : k) • x = r • x :=
 algebra_map_smul k r x
diff --git a/src/algebra/algebra/restrict_scalars.lean b/src/algebra/algebra/restrict_scalars.lean
index 39284c7145a49..a0ad66aabad74 100644
--- a/src/algebra/algebra/restrict_scalars.lean
+++ b/src/algebra/algebra/restrict_scalars.lean
@@ -172,7 +172,7 @@ lemma restrict_scalars.add_equiv_symm_map_smul_smul (r : R) (s : S) (x : M) :
   = r • (restrict_scalars.add_equiv R S M ).symm (s • x) :=
 by { rw [algebra.smul_def, mul_smul], refl, }
 
-lemma restrict_scalars.lsmul_apply_apply[module Sᵐᵒᵖ M] [is_central_scalar S M]
+lemma restrict_scalars.lsmul_apply_apply [module Sᵐᵒᵖ M] [is_central_scalar S M]
   (s : S) (x : restrict_scalars R S M) :
   restrict_scalars.lsmul R S M s x =
     (restrict_scalars.add_equiv R S M).symm (s • (restrict_scalars.add_equiv R S M x)) :=
diff --git a/src/algebra/triv_sq_zero_ext.lean b/src/algebra/triv_sq_zero_ext.lean
index 49987af59314c..efaf64720519e 100644
--- a/src/algebra/triv_sq_zero_ext.lean
+++ b/src/algebra/triv_sq_zero_ext.lean
@@ -586,21 +586,19 @@ instance algebra' : algebra S (tsze R M) :=
     show r • x.2 = algebra_map S R r • x.2 + op x.1 • 0,
       by rw [smul_zero, add_zero, algebra_map_smul],
   op_smul_def' := λ x r, ext (algebra.op_smul_def _ _) $
-    show mul_opposite.op r • x.2 = x.1 • 0 + algebra_map S R r • x.2,
-    by rw [smul_zero, zero_add, op_smul_eq_smul, algebra_map_smul],
+    show mul_opposite.op r • x.2 = x.1 • 0 + mul_opposite.op (algebra_map S R r) • x.2,
+    by rw [smul_zero, zero_add, op_smul_eq_smul]; sorry,
   .. (triv_sq_zero_ext.inl_hom R M).comp (algebra_map S R) }
 
 lemma algebra_map_eq_inl' (s : S) : algebra_map S (tsze R M) s = inl (algebra_map S R s) := rfl
 
 -- for the rest of this section we only care about the case when `R = S`
-variables [module Rᵐᵒᵖ M] [is_central_scalar R M]
 
 -- shortcut instance for the common case
 instance : algebra R' (tsze R' M) := triv_sq_zero_ext.algebra' _ _ _
 
 lemma algebra_map_eq_inl : ⇑(algebra_map R' (tsze R' M)) = inl := rfl
 lemma algebra_map_eq_inl_hom : algebra_map R' (tsze R' M) = inl_hom R' M := rfl
-lemma algebra_map_eq_inl' (s : S) : algebra_map S (tsze R M) s = inl (algebra_map S R s) := rfl
 
 /-- The canonical `R`-algebra projection `triv_sq_zero_ext R M → R`. -/
 @[simps]