`map_add` times out, and AlgHom.map_* is deprecated

Zulip: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Deprecation.20and.20time.20out

MWE reported by @AntoineChambert-Loir :

import Mathlib.RingTheory.TensorProduct.Basic

open TensorProduct

variable {R A : Type*} [CommRing R] [CommRing A]

lemma foo [Algebra A R] (S : Type*) [CommRing S] [Algebra A S] {S₀ : Subalgebra A S}
    {T₀ : Subalgebra A R} (x y : ↥T₀ ⊗[A] ↥S₀) :
    (Algebra.TensorProduct.map T₀.val S₀.val) x + (Algebra.TensorProduct.map T₀.val S₀.val) y =
    (Algebra.TensorProduct.map T₀.val S₀.val) (x + y) := by
  rw [AlgHom.map_add] -- But `rw [map_add]` times out.

Kevin notes:

 [synthInstance] [1.237288] ✅️ NonUnitalNonAssocSemiring ({ x // x ∈ T₀ } ⊗[A] { x // x ∈ S₀ }) ▶

is at least part of the problem.

Random hacks like attribute [-instance] Subalgebra.smulCommClass_right in fix the timeout (this is just looking at things in the instance trace which are making things go the long way around)

Start by reproducing the MWE in Mathlib/RingTheory/TensorProduct/Basic around Algebra.TensorProduct.map and AlgHom.map_add, then inspect the instance trace for the NonUnitalNonAssocSemiring search. Compare the deprecated AlgHom.map_* path with the unqualified map_add path; done means the example no longer times out and the deprecation is addressed without relying on the reported instance-removal hack.