Commit 2025-10-04 07:54 08f5cd2f

chore(Lean/Expr/Basic): move material about rewriting to a new file (#30156) These methods should go into Lean.Meta.Tactic.Rewrite instead, so move them to a new file. I credit Kim, Kyle and Patrick from #3801 for this; Kim's final clean-up eventually introduced these methods. With this moved, the imports for Lean.Expr.Basic can be reduced to just Lean.Expr, which we do. Noticed during work on #26221.