Where is `has_coe_to_sort (subalgebra R A)`?

Stream: general

[Eric Wieser]

I've found myself using subalgebra in the past, but was surprised to find that the docs don't reveal any has_coe_to_sort instance! Is there an easy way to ask lean how it found the instance?

[Kevin Buzzard]

One can start investigating this sort of thing like this:

import algebra.algebra.subalgebra

example (R : Type*) (A : Type*) [comm_semiring R]
  [semiring A] [algebra R A] : false :=
begin
  let ZZZ : has_coe_to_sort (subalgebra R A) := by apply_instance,
  sorry
end

[Kevin Buzzard]

The infoview says that ZZZ := coe_sort_trans and clicking on that tells us that submodule.has_coe_to_sort exists and etc. Is this enough clues?

[Eric Wieser]

docs#coe_sort_trans is almost certainly what I wanted to find, thanks!

[Eric Wieser]

And using let sounds like a good trick to remember.