refactor: use withImplicitBinderInfos and mkArrowN in more places (#11492)

This PR uses the the helper functions withImplicitBinderInfos and
mkArrowN in more places.

Author: nomeata

src/Lean/Elab/Tactic/Ext.lean

@@ -46,7 +46,7 @@ def withExtHyps (struct : Name) (flat : Bool)
     throwError "Internal error when constructing `ext` hypotheses: `{struct}` is not a structure"
   let structC ← mkConstWithLevelParams struct
   forallTelescope (← inferType structC) fun params _ => do
-  withNewBinderInfos (params.map (·.fvarId!, BinderInfo.implicit)) do
+  withImplicitBinderInfos params do
   withLocalDecl `x .implicit (mkAppN structC params) fun x => do
   withLocalDecl `y .implicit (mkAppN structC params) fun y => do
     let mut hyps := #[]

src/Lean/Meta/CongrTheorems.lean

@@ -339,7 +339,7 @@ where
               go (i+1) (rhss.push rhs) (eqs.push none) hyps
             | .subsingletonInst =>
               -- The `lhs` does not need to instance implicit since it can be inferred from the LHS
-              withNewBinderInfos #[(lhss[i]!.fvarId!, .implicit)] do
+              withImplicitBinderInfos #[lhss[i]!] do
                 let lhs := lhss[i]!
                 let lhsType ← inferType lhs
                 let rhsType := lhsType.replaceFVars (lhss[*...rhss.size]) rhss

src/Lean/Meta/Constructions/CtorIdx.lean

@@ -46,7 +46,7 @@ public def mkCtorIdx (indName : Name) : MetaM Unit :=
 
     let us := info.levelParams.map mkLevelParam
     forallBoundedTelescope info.type (info.numParams + info.numIndices) fun xs _ => do
-      withNewBinderInfos (xs.map (⟨·.fvarId!, .implicit⟩)) do
+    withImplicitBinderInfos xs do
       let params : Array Expr := xs[:info.numParams]
       let indices : Array Expr := xs[info.numParams:]
       let indType := mkAppN (mkConst indName us) xs

src/Lean/Meta/Injective.lean

@@ -72,8 +72,7 @@ private def mkInjectiveTheoremTypeCore? (ctorVal : ConstructorVal) (useEq : Bool
     if useEq then
       mkArgs2 0 type #[] #[]
     else
-      withNewBinderInfos (params.map fun param => (param.fvarId!, BinderInfo.implicit)) <|
-      withNewBinderInfos (args1.map fun arg1 => (arg1.fvarId!, BinderInfo.implicit)) <|
+      withImplicitBinderInfos (params ++ args1) do
         mkArgs2 0 type #[] #[]
 
 private def mkInjectiveTheoremType? (ctorVal : ConstructorVal) : MetaM (Option Expr) :=
@@ -189,9 +188,6 @@ def getCtorAppIndices? (ctorApp : Expr) : MetaM (Option (Array Expr)) := do
     if val.numIndices == 0 then return some #[]
     return some typeArgs[val.numParams...*].toArray
 
-private def mkArrows (hs : Array Expr) (type : Expr) : CoreM Expr := do
-  hs.foldrM (init := type) mkArrow
-
 private structure MkHInjTypeResult where
   thmType : Expr
   us : List Level
@@ -202,6 +198,7 @@ private def mkHInjType? (ctorVal : ConstructorVal) : MetaM (Option MkHInjTypeRes
   let type ← elimOptParam ctorVal.type
   forallBoundedTelescope type ctorVal.numParams fun params type =>
   forallTelescope type fun args1 _ => do
+  withImplicitBinderInfos (params ++ args1) do
     let k (args2 : Array Expr) : MetaM (Option MkHInjTypeResult) := do
       let lhs := mkAppN (mkAppN (mkConst ctorVal.name us) params) args1
       let rhs := mkAppN (mkAppN (mkConst ctorVal.name us) params) args2
@@ -213,7 +210,7 @@ private def mkHInjType? (ctorVal : ConstructorVal) : MetaM (Option MkHInjTypeRes
         let some idxs2 ← getCtorAppIndices? rhs | return none
         -- **Note**: We dot not skip here because the type of `noConfusion` does not.
         let idxEqs ← mkEqs idxs1 idxs2 (skipIfPropOrEq := false)
-        let result ← mkArrows idxEqs result
+        let result ← mkArrowN idxEqs result
         let thmType ← mkForallFVars params (← mkForallFVars args1 (← mkForallFVars args2 result))
         return some { thmType, us, numIndices := idxs1.size }
       else
@@ -226,9 +223,7 @@ private def mkHInjType? (ctorVal : ConstructorVal) : MetaM (Option MkHInjTypeRes
           mkArgs2 (i + 1) (b.instantiate1 arg2) (args2.push arg2)
       else
         k args2
-    withNewBinderInfos (params.map fun param => (param.fvarId!, BinderInfo.implicit)) <|
-    withNewBinderInfos (args1.map fun arg1 => (arg1.fvarId!, BinderInfo.implicit)) <|
-      mkArgs2 0 type #[]
+    mkArgs2 0 type #[]
 
 private def failedToGenHInj (ctorVal : ConstructorVal) : MetaM α :=
   throwError "failed to generate heterogeneous injectivity theorem for `{ctorVal.name}`"

src/Lean/Meta/Match/MatchEqs.lean

@@ -571,7 +571,7 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no
           let lhs := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ patterns ++ alts)
           let rhs := mkAppN alt rhsArgs
           let thmType ← mkEq lhs rhs
-          let thmType ← hs.foldrM (init := thmType) (mkArrow · ·)
+          let thmType ← mkArrowN hs thmType
           let thmType ← mkForallFVars (params ++ #[motive] ++ ys ++ alts) thmType
           let thmType ← unfoldNamedPattern thmType
           let thmVal ← proveCondEqThm matchDeclName thmType
@@ -684,7 +684,7 @@ where go baseName := withConfig (fun c => { c with etaStruct := .none }) do
           notAlt ← mkForallFVars (discrs ++ altVars) notAlt
           let lhs := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts)
           let thmType ← mkHEq lhs rhs
-          let thmType ← hs.foldrM (init := thmType) (mkArrow · ·)
+          let thmType ← mkArrowN hs thmType
           let thmType ← mkForallFVars (params ++ #[motive] ++ discrs ++ alts ++ altVars ++ heqs) thmType
           let thmType ← Match.unfoldNamedPattern thmType
           -- Here we prove the theorem from scratch. One could likely also use the (non-generalized)