Correct way to set up an instance with non-class parameters

Stream: general

[Paul Lezeau]

I'm currently trying to prove the following theorem

import ring_theory.adjoin_root

open polynomial localization

variables {R S : Type*} [comm_ring R] [comm_ring S] [algebra R S]
   [is_domain S] [is_integrally_closed R]

example (a : S) (ha : is_integral R a) : minpoly (fraction_ring R)  (algebra_map S
 (fraction_ring S) a)  ∣ (map_ring_hom (algebra_map R (fraction_ring R)) (minpoly R a)) :=
sorry

but for the statement to work I need the instance algebra (fraction_ring R ) (fraction_ring S). I wasn't able to find it in mathlib so I've tried to make my own, which yields the following MWE:

import ring_theory.adjoin_root

open polynomial localization


variables {R S : Type*} [comm_ring R] [comm_ring S] [algebra R S]
   [is_domain S]

noncomputable def frac_algebra_of_inj (h : function.injective (algebra_map R S)):
  algebra (fraction_ring R) (fraction_ring S) :=
ring_hom.to_algebra (is_fraction_ring.map h)

noncomputable instance problematic_instance (h : function.injective (algebra_map R S)):
  algebra (fraction_ring R) (fraction_ring S) :=
frac_algebra_of_inj h

#lint /- IMPOSSIBLE INSTANCES FOUND.
These instances have an argument that cannot be found during type-class resolution,
and therefore can never succeed. Either mark the arguments with square brackets
(if it is a class), or don't make it an instance. -/

Since this instance is wrong according to lint, what should I do?

[Eric Wieser]

Change h to a fact

[Eric Wieser]

But note that this instance might bad for reasons not found by the linter; it likely creates a diamond for the action of fraction_ring R on fraction_ring (fraction_ring R))

[Kevin Buzzard]

If anyone ever creates fraction_ring (fraction_ring R)) then they deserve the pain.

[Paul Lezeau]

Eric Wieser said:

Change h to a fact

Ok thanks, I'll try that!

[Paul Lezeau]

Eric Wieser said:

But note that this instance might bad for reasons not found by the linter; it likely creates a diamond for the action of fraction_ring R on fraction_ring (fraction_ring R))

Yeah I was planning on making it into a local attribute once I managed to get it work!