Applying ring_equiv.to_ring_hom

Stream: Is there code for X?

[Moritz]

Hi,
for the refactoring of sesquilinear forms the following trivial lemma comes up repeatedly and I wanted to ask whether it already exists somewhere.

lemma ring_equiv.to_ring_hom_apply {J : K ≃+* K} {x : K} : J.to_ring_hom x = J x :=
  by rw [J.to_ring_hom_eq_coe, J.coe_to_ring_hom]

[Heather Macbeth]

Good find! I think perhaps the issue is that docs#ring_equiv.to_ring_hom_eq_coe should be a simp lemma. Such things usually are, it might be an accidental omission here. Then the proof can be by simp.

[Eric Wieser]

I think we didn't agree on which direction simp should apply that lemma

[Eric Wieser]

Which is why it's not @[simp]

[Heather Macbeth]

Have we discussed this before? I thought that we prefer the coercion as the simp-normal form.

[Eric Wieser]

Maybe we came to a conclusion and didn't fully implement it

[Eric Wieser]

There's a discussion thread on zulip

[Anne Baanen]

I can't find the discussion. In any case, I had the insight recently that we could declare a blanket instance of the form [ring_hom_like F R S] : has_coe F (R →+* S). I worry that this will prove too hard to infer in practice, though.

[Anne Baanen]

So the coercion would be a good choice for simp-normal form if we ever want to go down that path :)