Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-08 14:39 a9178103

View on Github →

refactor(tactic/interactive): merge rcases_hint -> rcases?

Estimated changes