chore: adaptations for batteries#1496 (#31437)

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.com>

Author: fgdorais

Mathlib/Data/Nat/Bits.lean

@@ -3,10 +3,10 @@ Copyright (c) 2022 Praneeth Kolichala. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Praneeth Kolichala
 -/
+import Batteries.Tactic.GeneralizeProofs
 import Mathlib.Data.Nat.BinaryRec
 import Mathlib.Data.List.Defs
 import Mathlib.Tactic.Convert
-import Mathlib.Tactic.GeneralizeProofs
 import Mathlib.Tactic.Says
 import Mathlib.Util.AssertExists
 

Mathlib/Data/PFun.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Jeremy Avigad, Simon Hudon
 -/
 import Batteries.WF
+import Batteries.Tactic.GeneralizeProofs
 import Mathlib.Data.Part
 import Mathlib.Data.Rel
-import Mathlib.Tactic.GeneralizeProofs
 
 /-!
 # Partial functions

Mathlib/Lean/Expr/Basic.lean

@@ -366,16 +366,6 @@ def mapForallBinderNames : Expr → (Name → Name) → Expr
   | .forallE n d b bi, f => .forallE (f n) d (mapForallBinderNames b f) bi
   | e, _ => e
 
-open Lean.Elab.Term
-/-- Annotates a `binderIdent` with the binder information from an `fvar`. -/
-def addLocalVarInfoForBinderIdent (fvar : Expr) (tk : TSyntax ``binderIdent) : MetaM Unit :=
-  -- the only TermElabM thing we do in `addLocalVarInfo` is check inPattern,
-  -- which we assume is always false for this function
-  discard <| TermElabM.run do
-    match tk with
-    | `(binderIdent| $n:ident) => Elab.Term.addLocalVarInfo n fvar
-    | tk => Elab.Term.addLocalVarInfo (Unhygienic.run `(_%$tk)) fvar
-
 /-- If `e` has a structure as type with field `fieldName`, `mkDirectProjection e fieldName` creates
 the projection expression `e.fieldName` -/
 def mkDirectProjection (e : Expr) (fieldName : Name) : MetaM Expr := do

Mathlib/Tactic/Cases.lean

@@ -5,8 +5,9 @@ Authors: Mario Carneiro
 -/
 import Lean.Elab.Tactic.Induction
 import Batteries.Tactic.OpenPrivate
-import Mathlib.Lean.Expr.Basic
 import Batteries.Data.List.Basic
+import Batteries.Lean.Expr
+import Mathlib.Init
 
 /-!
 # Backward compatible implementation of lean 3 `cases` tactic

Mathlib/Tactic/Common.lean

@@ -17,6 +17,7 @@ import Batteries.Tactic.Basic
 import Batteries.Tactic.Case
 import Batteries.Tactic.HelpCmd
 import Batteries.Tactic.Alias
+import Batteries.Tactic.GeneralizeProofs
 
 -- Import syntax for leansearch
 import LeanSearchClient
@@ -57,7 +58,6 @@ import Mathlib.Tactic.Find
 import Mathlib.Tactic.FunProp
 import Mathlib.Tactic.GCongr
 import Mathlib.Tactic.GRewrite
-import Mathlib.Tactic.GeneralizeProofs
 import Mathlib.Tactic.GuardGoalNums
 import Mathlib.Tactic.GuardHypNums
 import Mathlib.Tactic.HigherOrder

Mathlib/Tactic/Core.lean

@@ -8,6 +8,7 @@ import Lean.Elab.Tactic.ElabTerm
 import Lean.Meta.Tactic.Intro
 import Mathlib.Lean.Expr.Basic
 import Batteries.Tactic.OpenPrivate
+import Batteries.Lean.Expr
 
 /-!
 # Generally useful tactics.