map_add times out, and AlgHom.map_* is deprecated

[jcommelin]

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)

[kbuzzard]

Trying it on current master, the slowest step is now

  [Meta.synthInstance] [2.336093] ✅️ AddHomClass (↥T₀ ⊗[A] ↥S₀ →ₐ[A] R ⊗[A] S) (↥T₀ ⊗[A] ↥S₀) (R ⊗[A] S) ▶

and over half the time spent on this synthesis is the following failures:

  [] [0.423889] ❌️ apply @Subalgebra.smulCommClass_right to SMulCommClass A ↥T₀ ↥T₀ ▶
  [] [0.106194] ❌️ apply IsScalarTower.subalgebra' to IsScalarTower A ↥T₀ ↥T₀ ▶
  [] [0.221100] ❌️ apply @Subalgebra.isScalarTower_mid to IsScalarTower A ↥T₀ ↥T₀ ▶
  [] [0.415022] ❌️ apply @Subalgebra.smulCommClass_right to SMulCommClass A ↥S₀ ↥S₀ ▶
  [] [0.104708] ❌️ apply IsScalarTower.subalgebra' to IsScalarTower A ↥S₀ ↥S₀ ▶
  [] [0.219686] ❌️ apply @Subalgebra.isScalarTower_mid to IsScalarTower A ↥S₀ ↥S₀ ▶

So this feels to me very much like the reasons integer rings were slow before they were turned into types. We have these terms-coerced-into-types and unfortunately there are many lemmas of the form "if it's true for the algebra, it's true for the subalgebra", which is a wrong turn. For example Subalgebra.smulCommClass_right says that if SMulCommClass) α A β then SMulCommClass) α (↥S) β where S is is a subalgebra of A. The problem with these lemmas is that they can lead you up the garden path, trying to find structure which isn't there. The analogous problem with integer rings was that if you wanted to prove that O_K acted on something then (because O_K was originally a subring) it would suffice to prove that K acted on the thing, but of course mathematically this is less likely to be true and was often false in practice. The same is happening here, for example trying Subalgebra.smulCommClass_right on SMulCommClass A ↥S₀ ↥S₀ takes you to

 [synthInstance] [0.409191] ❌️ SMul S ↥S₀

which fails (as it should -- the big ring doesn't act on the subring) but fails slowly because it goes on a big adventure (e.g. [] ✅️ apply @LinearOrderedCommRing.toLinearOrderedCommSemiring to LinearOrderedCommSemiring S etc etc) before giving up.