need `erw` due to type not being `dsimpNF`

Stream: mathlib4

[Calle Sönne]

I have noticed cases of needing erw because (d)simp has simplified the type of some expression (but not visibly the expression itself).

Basically, if my lemma is called lemma, then the following workaround avoids erw [lemma]:

have := lemma
dsimp at this
rw [this]

Have people thought how to get around this?

My first guess would just be to manually specify the type in the lemma statement so that it has dsimpNF, but I am not sure how to do this. This is from #18197, where extendScalarsComp_hom_app_one_tmul causes the need for many erws (which would be nice to avoid). The type of the LHS is: ((extendScalars f₁₂ ⋙ extendScalars f₂₃).obj M), which is not in dsimpNF, and is what is causing the issues with erw. However I can't seem to manually specify the type by restating the lemma as:

lemma extendScalarsComp_hom_app_one_tmul (M : ModuleCat R₁) (m : M) :
    ((extendScalarsComp f₁₂ f₂₃).hom.app M ((1 : R₃) ⊗ₜ m) :
      (extendScalars f₂₃).obj ((extendScalars f₁₂).obj M)) =
        (1 : R₃) ⊗ₜ[R₂,f₂₃] ((1 : R₂) ⊗ₜ[R₁,f₁₂] m) := by

In the first line of the proof, hovering over the LHS still gives the type ((extendScalars f₁₂ ⋙ extendScalars f₂₃).obj M).

I also feel that some automation should be able to get around this, and potentially save a lot of erws in the future (i.e. by automatically putting the type of the lemma in dsimpNF).

[Kim Morrison]

Yes, a cast like that doesn't actually change the type in any way, it just checks that the types agree.

[Kim Morrison]

I think a dsimp% elaborator is needed here, perhaps?

[Kim Morrison]

(relatedly, we might consider replacing by simpa using h with an elaborator simp% h??)

[Anne Baanen]

Another thread that might be relevant: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Fixing.20the.20.60erw.60.20hell.20around.20concrete.20categories

[Calle Sönne]

Kim Morrison said:

I think a dsimp% elaborator is needed here, perhaps?

Yes, this would be a good idea!