def Lean.Elab.Tactic.Do.ProofMode.synthIsAnd (u : Level) (σs H : Expr) : OptionT MetaM (Expr × Expr × Expr)

def Lean.Elab.Tactic.Do.ProofMode.mCasesAddGoal (u : Level) (goals : IO.Ref (Array MVarId)) (σs T Q H : Expr) : MetaM (Unit × MGoal × Expr)

def Lean.Elab.Tactic.Do.ProofMode.mCasesExists {α : Type} (H : Expr) (name : TSyntax `Lean.binderIdent) (k : Expr → MetaM (α × MGoal × Expr)) : MetaM (α × MGoal × Expr)

partial def Lean.Elab.Tactic.Do.ProofMode.mCasesCore {α : Type} (u : Level) (σs H : Expr) (pat : Parser.Tactic.MCasesPat) (k : Expr → MetaM (α × MGoal × Expr)) : MetaM (α × MGoal × Expr)

def Lean.Elab.Tactic.Do.ProofMode.elabMCases : Tactic