[Merged by Bors] - feat: rcases and rintro tactics

Mathlib.lean

@@ -69,7 +69,7 @@ import Mathlib.Tactic.NormCast
 import Mathlib.Tactic.NormNum
 import Mathlib.Tactic.OpenPrivate
 import Mathlib.Tactic.PrintPrefix
-import Mathlib.Tactic.Rcases
+import Mathlib.Tactic.RCases
 import Mathlib.Tactic.Rename
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.RunCmd

Mathlib/Mathport/Syntax.lean

@@ -12,6 +12,7 @@ import Mathlib.Tactic.Find
 import Mathlib.Tactic.LibrarySearch
 import Mathlib.Tactic.NormCast
 import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.RCases
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.ShowTerm
 import Mathlib.Tactic.Simps
@@ -186,13 +187,6 @@ syntax (name := guardLHS) "guard_lhs " " =ₐ " term : conv
 
 end Conv
 
-syntax (name := rcases?) "rcases?" casesTarget,* (" : " num)? : tactic
-syntax (name := rcases) "rcases" casesTarget,* (" with " rcasesPat)? : tactic
-syntax (name := obtain) "obtain" (ppSpace rcasesPatMed)? (" : " term)? (" := " term,+)? : tactic
-
-syntax (name := rintro?) "rintro?" (" : " num)? : tactic
-syntax (name := rintro) "rintro" (ppSpace rintroPat)* (" : " term)? : tactic
-
 syntax (name := ext1) "ext1" (ppSpace rcasesPat)* : tactic
 syntax (name := ext1?) "ext1?" (ppSpace rcasesPat)* : tactic
 -- The current implementation of `ext` in mathlib4 does not support `rcasesPat`,

Mathlib/Tactic/Ext.lean

@@ -5,7 +5,7 @@ Author: Gabriel Ebner
 -/
 import Lean
 import Mathlib.Tactic.Cache
-import Mathlib.Tactic.Rcases
+import Mathlib.Tactic.RCases
 
 open Tactic