coe confusion

Stream: mathlib4

[Moritz Firsching]

In #7010, having the following lemma is useful:

lemma coe_toMonoidHom {R R' : Type} [CommMonoid R] [CommMonoidWithZero R'] (χ : MulChar R R')
(x : R) : χ.toMonoidHom x = χ x := by rfl

When looking into if it would be a good idea to add this to NumberTheory/LegendreSymbol/MulCharacter.lean, I noticed that there are many lemmas like this which are potentially useful, like

@[simp]
lemma toMonoidHom_coe (χ : MulChar R R') : χ.toMonoidHom = χ := by
  rfl

@[simp]
lemma toMonoidHom_coe' (χ : MulChar R R') (x : R) : χ.toMonoidHom x = χ x := by
  rfl

@[simp]
lemma toMonoidHom_toFun_coe (χ : MulChar R R') : χ.toMonoidHom.toFun = χ := by
  rfl

@[simp]
lemma toMonoidHom_toFun_coe' (χ : MulChar R R') (x : R) : χ.toMonoidHom.toFun x = χ x := by
  rfl

Which of them should be added and what are the good canonical names for these?

[Eric Wieser]

Doesn't the simpNF linter complain there?

[Yury G. Kudryashov]

Which function is behind the coercion?

[Yury G. Kudryashov]

In any case, you should use rfl, not by rfl to make these lemmas useful for dsimp (or did it change in Lean 4?)

[Moritz Firsching]

Eric Wieser said:

Doesn't the simpNF linter complain there?

No, #lint does not complain about that, see #7026. But does this mean all of those lemmas are useful/needed?

[Yury G. Kudryashov]

I'm surprised that lemmas No 3 and 4 have LHS in the simp normal form.

[Eric Wieser]

Are we missing docs#MonoidHom.toFun_eq_coe ?

[Eric Wieser]

Yep, looks like it lost its simp attribute during the port

[Eric Wieser]

This is pretty unpleasant:

image.png

[Yaël Dillies]

I have a PR in the works to fix this

[Eric Wieser]

How?

[Eric Wieser]

I don't understand why src#MonoidHom.toMulHom_coe is simpNF

[Eric Wieser]

(I also have a PR to fix this (the first of which is #7016), by using flat structures for morphisms so that f.toFun is not syntax for one (but only one) of f.toMulHom.toFun or f.toOneHom.toFun)

[Yaël Dillies]

I'm currently worried about lattice homs. I'll move onto algebra homs once I'm done.

[Moritz Firsching]

Yury G. Kudryashov said:

In any case, you should use rfl, not by rfl to make these lemmas useful for dsimp (or did it change in Lean 4?)

That's good to know. Is #7039 then a useful change?

[Moritz Firsching]

Yaël Dillies said:

I have a PR in the works to fix this

Did you finish the work on this PR or was this is same as @Eric Wieser's #7016? In #7026, I still don't get simpNF lint errors

[Yaël Dillies]

Not yet, but my yet-to-be PR is currently only concerned about lattice homs, which I assume are not the ones you use.

[Moritz Firsching]

Eric Wieser said:

(I also have a PR to fix this (the first of which is #7016), by using flat structures for morphisms so that f.toFun is not syntax for one (but only one) of f.toMulHom.toFun or f.toOneHom.toFun)

Did you continue making more changes in that direction? ("the first of which" sounds like you might have planned a second one?)

[Eric Wieser]

I still haven't fixed the long tail of CI failures in that PR

[Eric Wieser]

(oh, that's not the PR I thought it was)

[Eric Wieser]

#6791 is the one where I make things flat