How to deal with a lot of `have`

Stream: mathlib4

[Riccardo Brasca]

TL;DR
Do we want the following instance?

import Mathlib

attribute [local instance] FractionRing.liftAlgebra

instance {R S : Type*} [CommRing R] [IsDomain R] [CommRing S] [IsDomain S] [Algebra R S]
  [FaithfulSMul R (FractionRing S)] [Module.Finite R S] [IsIntegrallyClosed S] [NoZeroSMulDivisors R S] :
    FiniteDimensional (FractionRing R) (FractionRing S) :=
  Module.Finite_of_isLocalization R S _ _ (nonZeroDivisors R)

Note that docs#Module.Finite_of_isLocalization cannot be an instance.

Here is more context and a real world example. Let's suppose we want to prove something about an extension $R \to S$ of Dedekind domains (say). One standard technique is to prove the same thing after localization at any prime ideal $\mathfrak{p}$ of $R$. We get the corresponding extension $R_{\mathfrak{p}} \to S_{\mathfrak{P}}$, where $\mathfrak{P}=\mathfrak{p}S$, that satisfies a lot of "standard properties". Now, it is often convenient to introduce $K = \mathrm{Frac}(R)$ and $L = \mathrm{Frac}(S)$, and maybe also $K_\mathfrak{p} = \mathrm{Frac}(R_{\mathfrak{p}})$ and $L_\mathfrak{P} = \mathrm{Frac}(S_{\mathfrak{P}})$ (of course mathematically $K = K_\mathfrak{p}$, but not for Lean). Now, even ignoring properties of $R_\mathfrak{p}$, we already have a lot of Algebra instances, with all possible IsScalarTower.

Most of these results are already in mathlib and they are correctly stated using, for example, IsLocalization instead of the localization. The problem is that, because of this generality, they cannot be instances (since Lean has no way of guessing $\mathfrak{p}$), see for example the sequence of have here. On the other hand, the results for Localization ... can be instances, and this would eliminate (most of) the have in the above proof. This is what I am doing in #21463.

Does anyone see a better solution here?

[Andrew Yang]

I think yes but FaithfulSMul R (FractionRing S) is probably implied by NoZeroSMulDivisors R S and we probably do have that instance

[Andrew Yang]

(But I probably added that instance into flt-regular so my vote might not count)

[Riccardo Brasca]

I am doing this in #21522 (finishing it tomorrow I think). Essentially all the have in your proofs can be instances, so it seems a good idea to have them.

[Riccardo Brasca]

#21522 is ready