mathlib3

feat(tactic/simps): allow let-expressions

#1626

Merged