Commit 2026-10-19 06:25 edc925ed

fix: use meta imports for metaprogramming dependencies (#43912) Prevent public import Mathlib from exposing Lean's metaprogramming APIs to public runtime declarations. Runtime use now requires an explicit ordinary import. Use meta imports for tooling dependencies, move inequality expression recognizers into Mathlib.Tactic.Ineq as meta definitions, and preserve meta imports in mk_all. Add regression tests for the boundary and explicit-import opt-in. Only two declarations change phase: Lean.Expr.ineq? and Lean.Expr.ineqOrNotIneq? move from Mathlib.Data.Ineq to Mathlib.Tactic.Ineq and become meta. Keeping them as ordinary definitions in Mathlib.Data.Ineq requires a plain import of Mathlib.Lean.Expr.Basic there, which exposes Lean.Expr through import Mathlib and fails the ImportLean test.