Commit 2026-01-19 10:42 d03d6727

feat(Tactic/Choose): add type annotation support (#33033) This PR adds support for type annotations in the choose tactic, similar to how intro supports them. This allows writing:

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

instead of just choose n hn using h. The type annotation is checked against the actual type from the existential, and an error is raised if they don't match. This is useful for pedagogical purposes and for catching mistakes early. Requested on Zulip: https://leanprover.zulipchat.com/#narrow/channel/187764-Lean-for-teaching/topic/adding.20type.20annotation.20to.20.60choose.60/near/564323626 🤖 Prepared with Claude Code