Explicit variable in Units.mk0

Stream: mathlib4

[Filippo A. E. Nuccio]

In the following lemma (see docs#Units.mk0)

def mk0 (a : G₀) (ha : a ≠ 0) : G₀ˣ :=
  ⟨a, a⁻¹, mul_inv_cancel ha, inv_mul_cancel ha⟩

I would suggest that (a : G₀) is left implicit. Is there a reason why it is not? I have seen that @Jireh Loreaux worked on this, perhaps he has a comment.

[Jireh Loreaux]

That's just from the port. This hasn't been touched since Mathlib3, where I assume the point was that you often may want to delay the proof obligation, and in Lean 3 it was more of an issue because you had to do @. In Lean 4 this is less of a problem.

I don't have strong feelings here.

[Filippo A. E. Nuccio]

I see your point. I would suggest to make it implicit, but will wait for some reactions here before opening a PR.

[Eric Wieser]

If you make it implicit, then you will see mk0 _ in the goal view and have no idea which unit is being talked about

[Filippo A. E. Nuccio]

In which context? I mean, if a lemma needs a unit and you have in your context an h : a ≠ 0, then you can feed your lemma with mk0 h. When would you see mk0 _ ?

[Jireh Loreaux]

Can't you change that with pp.proofs or some options?

[Jireh Loreaux]

After that, in the infoview, you will see mk0 _ in the goal, for example.

[Filippo A. E. Nuccio]

Jireh Loreaux said:

After that, in the infoview, you will see mk0 _ in the goal, for example.

Ah, I see. Well, but shall we privilege the code in function of the infoview's behaviour? This is something that changes "often"

[Jireh Loreaux]

Like I said, I think it's an option you can select.

[Jireh Loreaux]

But that behavior has long been the norm.

[Filippo A. E. Nuccio]

OK, I'll live with it (and without too much suffering :smile: )

[Jireh Loreaux]

Of course, you can always just use an underscore if you already have the proof available.

[Filippo A. E. Nuccio]

Sure, that's what I am doing and I ended up wondering if it is normal.

[Yaël Dillies]

I agree that argument should stay explicit

[Eric Rodriguez]

is proofs.withType off by default now? I would expect to see .mk0 (_ : a ≠ 0)

[Eric Wieser]

We could write a custom delaborator to print that way despite the default

[Eric Wieser]

But the result is longer than the underscore spelling

[Mario Carneiro]

Eric Rodriguez said:

is proofs.withType off by default now? I would expect to see .mk0 (_ : a ≠ 0)

Yes, it was recently disabled by default because showing the types can be quite verbose