mathlib3
feat(tactic/rcases): transport the `cases h : e` syntax to `rcases`
#1611

Merged

feat(tactic/rcases): transport the `cases h : e` syntax to `rcases` #1611

mergify merged 8 commits into master from tagged-rcases

Update rcases.lean

338793e6

Update rcases.lean

c941beeb

cipher1024 requested a review from

robertylewis 6 years ago

Update rcases.lean

acc3d45d

Update lift.lean

9991c1c1

robertylewis added needs-documentation

Update rcases.lean

fe0e5993

Update tactics.md

b53f48d3

Update rcases.lean

69e59fa7

fpvandoorn approved these changes on 2019-10-28

fpvandoorn removed needs-documentation

fpvandoorn added ready-to-merge

Merge branch 'master' into tagged-rcases

15ca72bc

mergify merged 0ea3dfe4 into master 6 years ago

mergify deleted the tagged-rcases branch 6 years ago

Reviewers

fpvandoorn

robertylewis

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone