def Lean.Elab.Tactic.Do.findSpec (database : SpecAttr.SpecTheorems) (wp : Expr) : MetaM SpecAttr.SpecTheorem

def Lean.Elab.Tactic.Do.mSpec {n : Type → Type u_1} [Monad n] [MonadControlT MetaM n] [MonadLiftT MetaM n] (goal : ProofMode.MGoal) (elabSpecAtWP : Expr → n SpecAttr.SpecTheorem) (goalTag : Name) (tryTrivial : Bool := true) : n Expr

Returns the proof and the list of new unassigned MVars.