Commit 2025-01-01 22:55 ec10d9ba

chore: split Lean/Meta/RefinedDiscrTree (#20381) This split is intended to roughly match #11968, in order to reduce the diff there. I will take ownership of fixing any resulting merge conflicts. The declarations have been copied unchanged between files, with the exception of a single removed private on DTExpr.eqv that prevented this split. Refactors are left to #11968. The namespace of all the declarations has changed from Mathlib.Meta.FunProp.RefinedDiscrTree to Lean.Meta.RefinedDiscrTree, to match the filename.