with in definitions

Stream: mathlib4

[Anatole Dedecker]

What is the status of using with (or __ :=) in definitions that are not instances? It is of course less harmful since it doesn't mess up with typeclass inference, but it still generates the same "ugly" terms, so it has to generate slower defeqs, right? Is that negligible enough that we don't care? Should we be pushing actively about using with, be neutral about it, or discourage its use?

[Eric Wieser]

I think the difference is that defeq of those terms almost never matters. someHom.toWeakerHom = someWeakerHom is a pretty rare thing to unify, and FunLike.coeFun SomeHom = someFun won't care about the with

[Eric Wieser]

In contrast, someInstance.toWeakerInstance = someWeakInstance comes up all the time

[Anatole Dedecker]

Eric Wieser said:

FunLike.coeFun SomeHom = someFun won't care about the with

Oh I see, this is the part that I didn't know about.

[Eric Wieser]

To be clear, this is somewhat speculative on my part...

[Antoine Chambert-Loir]

Probably related question : when you have to prove something about some complicated structure, it often appears in a verbose form in the goal, and some ‘simp‘ is necessary to clean it up. Is it normal? Why?

[Kevin Buzzard]

dsimp only is probably the best "tidy up" tactic

[Antoine Chambert-Loir]

But why does of show up like this, as much unfolded?

[Kevin Buzzard]

I should say that I don't think that this question is related to the "with considered harmful" topic which I think this is about, but I think the answer is simply that lean doesn't simplify things like {x := a, y := b}.x to a unless you ask it to.

[Eric Wieser]

Note that dsimp only won't help you with ↑{ toFun := f, ... } x

[Anatole Dedecker]

The right solution is definitely a clever use of @[simps]