Use rcases in places where multiple cases are needed - Githubissues

spl / alpha-conversion-is-easy

Lean proof of alpha-conversion is easy

4 stars 0 forks source link

Use rcases in places where multiple cases are needed #39

Open spl opened 6 years ago

spl commented 6 years ago

See https://gitter.im/leanprover_public/Lobby?at=5a398181a2be466828c049f7

spl commented 6 years ago

rcases source: https://github.com/leanprover/mathlib/blob/902b94d3075b44601d2ee4bd74898510a0aa26ed/tactic/rcases.lean

spl commented 6 years ago

Also by_cases: