adding type annotation to `choose`

Stream: Lean for teaching

[Alex Kontorovich]

While you don't have to add type annotation when applying intro or choose, I think it has pedagogical value (perhaps @Patrick Massot showed me this?). Except that adding type annotation to choose actually doesn't work? Compare:
image.png
Lean has no problem with intro ε (hε : ε > 0). But if I try to do choose c (hc : f c = 2) using h here, I get an error:
image.png
Surely there's a way to allow choose to take a type annotation (and confirm that it's right), no? Thanks for your help!

[Kim Morrison]

@Alex Kontorovich I've implemented this feature! See https://github.com/leanprover-community/mathlib4/pull/33033

You can now write:

choose (n : ℕ) (hn : n > 0) using h

The type annotation is checked against the actual type from the existential, and an error is raised if they don't match.

[Kim Morrison]

Please try this out, and let me know if it behaves the way you want, e.g. with respect to unification of types.

[Kim Morrison]

(Just for context about what Claude can do these days:)

This was written autonomously by Claude. My only input was:

Please read
https://leanprover.zulipchat.com/#narrow/channel/187764-Lean-for-teaching/topic/adding.20type.20annotation.20to.20.60choose.60/near/564323626

Yes please.

Please branch, PR, and ping Alex in the original thread about the PR.

[Jakub Nowak]

Maybe we could also support auto-params? See #general > choose and autoparams. E.g. like this:

choose (n : ℕ) (hn : n > 0 := by grind) using @h

[Kim Morrison]

I think I'll leave that for someone else, feels niche. :-)

[Julian Berman]

Kim Morrison said:

Please branch, PR, and ping Alex in the original thread about the PR.

(Mildly offtopic, but) I am curious about this part -- was that first message written by Claude and it has API access to your Zulip? Or did it ignore this part of your request Kim? Or have you and Claude merged into a big scary productivity machine?

[Kim Morrison]

Yes, I gave it a zulip skill, which uses some Claude written wrapper scripts around the API.

[Kim Morrison]

The zulip skill is also necessary for it to be able to act on the "Please read ..." prompt, as the default Fetch tool can't cope with zulip.