feat: use `rfl` proofs of `Iff` in `dsimp`

Open thorimur opened this issue 1 year ago • 7 comments

Retrying #2679 from scratch. WIP.

Apr 23 '24 00:04 thorimur

WIP

Apr 23 '24 00:04 thorimur

Mathlib CI status (docs):

❌ Mathlib branch lean-pr-testing-3973 built against this PR, but linting failed. (2024-04-23 01:08:08) View Log
❌ Mathlib branch lean-pr-testing-3973 built against this PR, but linting failed. (2024-04-23 01:28:21) View Log

Apr 23 '24 01:04 leanprover-community-mathlib4-bot