def
Lean.Elab.Tactic.Do.ProofMode.mRevertForallN
{m : Type → Type u}
[Monad m]
[MonadControlT MetaM m]
[MonadLiftT MetaM m]
(goal : MGoal)
(n : Nat)
(hypName : Name)
(k : MGoal → m Expr)
:
m Expr
Turn goal hᵢ : Hᵢ ⊢ₛ T e₁ ... eₙ into hᵢ : fun sₙ ... s₁ => Hᵢ h : fun sₙ ... s₁ => ⌜s₁ = e₁ ∧ ... ∧ sₙ = eₙ⌝ ⊢ₛ T