Def Mathlib.Tactic.Choose.choose1WithInfo

Modification history

2026-01-19 10:42

Mathlib/Tactic/Choose.lean

feat(Tactic/Choose): add type annotation support (#33033) …

Modified Mathlib.Tactic.Choose.choose1WithInfo View on Github →

2022-10-22 17:27

Mathlib/Tactic/Choose.lean

feat: port choose (#420)

Added Mathlib.Tactic.Choose.choose1WithInfo View on Github →