Commit 2022-07-20 16:22 f9153b8a

View on Github →

feat(tactic/attribute): add expand_exists (#15498) Adds an attribute expand_exists, which takes a proof that something exists with some property, and outputs a value using classical.some, and a proof that it has that property using classical.some_spec. Closes #11682

Estimated changes

Modified src/tactic/default.lean

Created src/tactic/expand_exists.lean

Created test/expand_exists.lean

added theorem dependent_type_exists

added def dependent_type_res

added theorem dependent_type_spec_res

added theorem nat_greater_exists

added theorem nat_greater_exists₂

added theorem nat_greater_nosplit_spec_res

added theorem nat_greater_spec_res

added theorem nat_greater_split_spec_lt_res

added theorem nat_greater_split_spec_neq_res