def Lean.Elab.Tactic.Do.ProofMode.transferHypNames (P P' : Expr) : MetaM Expr

If P' is a conjunction of unnamed hypotheses that are a subset of the named hypotheses of P, transfer the names of the hypotheses of P to the hypotheses of P'.

def Lean.Elab.Tactic.Do.ProofMode.mFrameCore {m : Type → Type u_1} [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (kFail : m Expr) (kSuccess : Expr → Expr → MGoal → m Expr) : m Expr

def Lean.Elab.Tactic.Do.ProofMode.mTryFrame {m : Type → Type u_1} [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (k : MGoal → m Expr) : m Expr

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