Where did this instance go? Is it true by apply_instance? If so, please mention that in the PR description!

Yes, both of the following work:

instance [algebra R S] [is_scalar_tower R S A] : is_scalar_tower R S (A ⊗[R] B) := infer_instance
instance [algebra S R] [is_scalar_tower S R A] : is_scalar_tower S R (A ⊗[R] B) := infer_instance

I added it to the PR description.

Since this creates a forward-porting obligation anyway, should we add the missing results:

• is_scalar_tower S (A ⊗[R] B) (A ⊗[R] B)
• smul_comm_class S (A ⊗[R] B) (A ⊗[R] B)

for when A is a non-unital algebra? (they're inferred from left_algebra when the algebra is unital)

These are the two instances I was thinking of:

instance [monoid S] [distrib_mul_action S A] [is_scalar_tower S A A] [smul_comm_class R S A] :
  is_scalar_tower S (A ⊗[R] B) (A ⊗[R] B) :=
{ smul_assoc := λ r x y, begin
    change (r • x) * y = r • (x * y),
    apply tensor_product.induction_on y,
    { simp [smul_zero], },
    { apply tensor_product.induction_on x,
      { simp [smul_zero] },
      { intros a b a' b',
        dsimp,
        rw [tensor_product.smul_tmul', tensor_product.smul_tmul', tmul_mul_tmul, smul_mul_assoc], },
      { intros, simp [smul_add, add_mul, *], } },
    { intros, simp [smul_add, mul_add, *], },
  end }

instance [monoid S] [distrib_mul_action S A] [smul_comm_class S A A] [smul_comm_class R S A] :
  smul_comm_class S (A ⊗[R] B) (A ⊗[R] B) :=
{ smul_comm := λ r x y, begin
    change r • (x * y) = x * r • y,
    apply tensor_product.induction_on y,
    { simp [smul_zero], },
    { apply tensor_product.induction_on x,
      { simp [smul_zero] },
      { intros a b a' b',
        dsimp,
        rw [tensor_product.smul_tmul', tensor_product.smul_tmul', tmul_mul_tmul, mul_smul_comm], },
      { intros, simp [smul_add, add_mul, *], } },
    { intros, simp [smul_add, mul_add, *], },
  end }

(#19143)

S should be explicit here

You're right, and it's often painful otherwise (hence a few include_left : _ \to\_a[S] _ later in the file). However, I wonder whether one could have a variant include_left where S and R are equal, and include_left' for the more general one (with one explicit argument).

We do use that pattern elsewhere; though it means you end up duplicating lots of api

I don't understand what you mean with “duplicating lots of api”: no new lemma is created.
In the commutative case, the application suggested by @ADedecker requires less than what is done here, namely just A \to\_a A \otimes[R] B. But if A is not commutative, that does not work and one needs all intermediate linearity properties A \to\_a [S] A\otimes[R] B, for adequate S.

If we have both include_left and include_left', then every time you write a lemma about the primed one you have to duplicate it for the unprimed one. So I think we should just have only the fully-general one; I don't think making people write a single R is much of a burden.

Thank you, I see. I had imagined having include_left := include_left' R, but that would require many simp only [include_left] to access the API of include_left', or duplicating it as you say.

(I'll have to check, but it seems that one needs to do similar modifications in linear_map.tensor_product.lean)

I would suggest making this generalization in a separate PR; the typeclass change by itelf is pretty self-contained

If I understand you correctly, this PR would just change the few instances that are invoked, and adding linearity is given in a separate PR ?