831e8d768b
This PR provides lemmas for the tree map functions `get`, `get!` and `getD` in relation to the other operations for which lemmas already exist. Internally, the `simp_to_model` tactic was provided two new simp lemmas to eliminate some common complications that require `rw`'ing before using `simp_to_model`. However, it is still necessary to sometimes `revert` some hypotheses. --------- Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> |
||
|---|---|---|
| .. | ||
| Classes | ||
| Data | ||
| Internal | ||
| Net | ||
| Sat | ||
| Sync | ||
| Tactic | ||
| Time | ||
| Classes.lean | ||
| Data.lean | ||
| Internal.lean | ||
| Net.lean | ||
| Sat.lean | ||
| Sync.lean | ||
| Tactic.lean | ||
| Time.lean | ||