Subalgebra to subring

Stream: Is there code for X?

[Nikolas Kuhn]

We have that coercing a subalgebra to a set factors through coercing to a subring:

@[simp] lemma coe_to_subring {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A]
  (S : subalgebra R A) : (↑S.to_subring : set A) = S := rfl

It seems like we don't have the same for coercing to sort instead of set -- would this be a good addition? And should it be marked with simp?
The same proof should work:

@[simp] lemma coe_to_subring' {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A]
  (S : subalgebra R A) : (S.to_subring : Type*) = (S : Type*) := rfl

[Kevin Buzzard]

This is an equality of types so it always makes me uneasy: my instinct would be that we should have an equiv. However @Yaël Dillies claimed the last time this came up that "this sort of thing was everywhere in category theory" or some such thing, so now I'm no longer sure.

[Eric Wieser]

Under what circumstance would this lemma be useful?

[Eric Wieser]

Kevin is right to worry; usually rewriting by an equality of types is not going to do you any favors

[Nikolas Kuhn]

Thanks for your opinions! That makes sense that one wants to be cautious about equality of types (it seems that they would in fact be "definitionally equal" here).
It also turned out not to help in the case where I thought it would.

[Eric Wieser]

It's certainly useful for types to be defined as definitionally equal

[Yaël Dillies]

The point is that defeq types can be simplified by dsimp, and this usually helps with unification. And I indeed used this trick quite a lot for my order categories stuff.

[Yaël Dillies]

For example, if you have X : BoolAlg and at some point you end up with x an element of X as a preorder, then x : X.to_BoundedDistribLattice.to_DistribLattice.to_Lattice.to_SemilatticeSup.to_Preorder. But actually x : X typechecks and this type is much easier to work with (notably for typeclass inference).