Merge master into nightly-testing

Mathlib/Lean/Meta.lean

@@ -121,24 +121,6 @@ def countLocalHypsUsed [Monad m] [MonadLCtx m] [MonadMCtx m] (e : Expr) : m Nat
   let e' ← instantiateMVars e
   return (← getLocalHyps).toList.countP fun h => h.occurs e'
 
-/--
-Given a monadic function `F` that takes a type and a term of that type and produces a new term,
-lifts this to the monadic function that opens a `∀` telescope, applies `F` to the body,
-and then builds the lambda telescope term for the new term.
--/
-def mapForallTelescope' (F : Expr → Expr → MetaM Expr) (forallTerm : Expr) : MetaM Expr := do
-  forallTelescope (← Meta.inferType forallTerm) fun xs ty => do
-    Meta.mkLambdaFVars xs (← F ty (mkAppN forallTerm xs))
-
-/--
-Given a monadic function `F` that takes a term and produces a new term,
-lifts this to the monadic function that opens a `∀` telescope, applies `F` to the body,
-and then builds the lambda telescope term for the new term.
--/
-def mapForallTelescope (F : Expr → MetaM Expr) (forallTerm : Expr) : MetaM Expr := do
-  mapForallTelescope' (fun _ e => F e) forallTerm
-
-
 /-- Get the type the given metavariable after instantiating metavariables and cleaning up
 annotations. -/
 def _root_.Lean.MVarId.getType'' (mvarId : MVarId) : MetaM Expr :=